Has the concept of using a hand checked simple theorem prover to validate more complex theorem provers been explored before?

More specifically, has anyone used a chain of theorem provers to validate a highly evolved theorem prover, starting with a very simple hand checked prover such that each new theorem prover is used to validate a somewhat more complex theorem prover, rinse repeat?

This would be something along the lines of induction, I guess. In that you'd have just as much confidence in the complex prover at the end as the hand checked prover you started with.

If it has been explored (wouldn't be surprised), a pointer towards more resources would be welcome.

Not that I know of. A more typical architecture is to decompose the theorem prover into a prover plus a proof checker. Then only the proof checker needs to be validated. If proofs are expressed in a simple enough language, then the proof checker might be extremely simple. All of the smarts can go into the prover (which tries various strategies to try to find a valid proof), but it doesn't need to be validated, since its output will always be checked by the proof checker.

StackExchange Computer Science Q#93792, answer score: 3