Comment by seanhunter
3 days ago
Well since one of the authors of TFA is literally the person who was asked by the association of symbolic logic to give the memorial lecture for Goedel’s centenary the comment could scarcely have been wider of the mark.
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...
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