I've had discussions around this with theorem prover types (OPLSS, highly recommend for people who can take the two weeks off)

The sort of head canon for any of the automated proof systems is that lean saying a proof is correct is "if lean is correct then the proof is correct".

One can get the temptation to try and prove lean correctness with lean but I believe _that_ is impossible due to the incompleteness theory.

_But_ the discussions I had, everyone was kind of in agreement with the idea that you could continue to shrink down the "kernel" of lean with lean (or whatever proof system really) so that in the end the thing you have to trust is pretty small.