New comment by fpvandoorn in "How to Formalize All of Mathematics"

fpvandoorn — Fri, 16 Oct 2026 16:37:09 +0000

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

New comment by fpvandoorn in "How An AI math breakthrough ignited a controversy"

fpvandoorn — Wed, 09 Sep 2026 13:21:00 +0000

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.

Hacker News: fpvandoorn

New comment by fpvandoorn in "How to Formalize All of Mathematics"

New comment by fpvandoorn in "How An AI math breakthrough ignited a controversy"