No. This is not how this works.

As the silliest example of this: the Calculus of Inductive Constructions (the core calculus implemented in Lean) has a published proof of its soundness (that you cannot derive False in it). That proof can (probably, thanks to Gödel) not be formalized in Lean or any formal system of axioms weaker than Lean.

If what you were trying to do was define what it means for something to be a correct proof, then you must equally admit that there can't be a correct proof of the fact that Lean can't prove False. And if you find that world a happy world to live in while we delegate all concerns about truth to Lean, then I have an infinite hierarchy of monotonically growing bridges to sell you.

Yes. This is how this works.

Any proof which is correct can be formalized. That is what is means for a proof to be correct.

I’m not sure why you are restricting the scope of our discussion to what _Lean_ can(not) formalize. Even if we do choose to do that for some reason, Lean is not a formal system of fixed axioms; it supports optional additional axioms.

There is no unconditional proof that CIC is sound. Thanks to Gödel, the best you can do is relative consistency proofs, something like "in ZFC with omega (i.e. infinitely) many inaccessible cardinals, you can prove that the theory of Lean is consistent". Such a relatively consistency proof can be fully formalized in Lean (and in fact, in much weaker systems than Lean).

In principle, a computer can check a nonconstructive proof. I don't know if that's possible in Lean. The interpretation of proofs still assumes the consistency of their axioms.

[dead]