fpvandoorn

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).

They actually used Lean statements that were carefully human-written and human-reviewed, from here https://github.com/google-deepmind/formal-conjectures/blob/m...

This doesn't guarantee that the statement is correct (Lean cannot do that), but makes it highly likely.