Perhaps you'd like to explain how you think the Incompleteness theorems affect this project?
That makes it sound like all possible mathematics past and future in all conceivable worlds. And we already know there are undecidable or unprovable statements, higher-order logics that cannot be fully formalized, concepts about axioms themselves that cannot be axiomatized, etc.
So it cannot mean "all of mathematics", strictly speaking. Just the areas in existing mathematics that have (or can have) formal proofs.
Feels like every time formalization is mentioned on hn somebody mentions incompleteness as though mathematicians in the field have never heard of it. It’s kind of annoying at this point. It’s like if every time we talked about a computer algorithm someone popped in to say “Have you heard of ‘On Computable Numbers’? Alan Turing would like a word.”
People in the field know about these things probably better than we do. They are aware of the consequences of completeness/incompleteness, decidability, computability etc. In fact Goedel’s completness and 2 incompleteness theorems have been formalized in lean as part of mathlib4 https://formalizedformallogic.org/Book/first_order/goedel1.h...
『Leanを用いたGödelの第一・第二不完全性定理の形式化』
..Oh I found a newer (more complete :) version of the proofs under the same domain.
https://formalizedformallogic.org/Catalogue/Arithmetic/G___d...
Looks like the /Book route is from an archived repo (https://github.com/FormalizedFormalLogic/book) and the content was moved to the Foundation's Catalogue. https://formalizedformallogic.org/Catalogue/
From the posted link, How to Formalize All of Mathematics, in the introduction:
> vision of how we can all work toward a world in which all, or almost all, mathematical definitions, theorems, and proofs are equipped with a formal representation
That "or almost all" feels like a wink to acknowledge the commonly misunderstood limitations of formal logic and systems. Your frustration is understandable, someone even wrote a whole book about it.
Franzén, Torkel. Gödel's Theorem: An Incomplete Guide to Its Use and Abuse