Comment by lioeters

Great link, wonderful, Formalized Formal Logic. I'll enjoy reading through it. I see, a Japanese person worked on the formalization of Gödel's Incompleteness Theorems.

『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