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…
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…
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…
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…