| ▲ | N_Lens 2 hours ago |
| Godel would like to talk to you about his “Incompleteness Theorem” |
|
| ▲ | dwohnitmok 2 hours ago | parent | next [-] |
| This is irrelevant. The theorems Avigard, Buzzard, et al. are talking about all have natural language proofs already that in theory should be formalizable. They are not claiming all possible theorems are formalizable. They are claiming to try to formalize all already proven theorems in the mathematics canon. To the extent the theorems in question are impossible to formalize this means the original proof must be in error. |
| |
| ▲ | Maxatar an hour ago | parent | next [-] | | >To the extent the theorems in question are impossible to formalize this means the original proof must be in error. Theorems by definition must be formalizable. A theorem is not simply a true proposition, it's a provable proposition and a proof is necessarily a formal/syntactic property of a proposition. That said, I agree with the sentiment that dismissing the entire article on the basis of the incompleteness theorems is shallow and the article is not about formalizing "all" of mathematics in the strict sense. It's mostly about introducing formal tools to the everyday mathematics. | |
| ▲ | netdevphoenix an hour ago | parent | prev [-] | | Then, "All of Mathematics" is being used as clickbait. |
|
|
| ▲ | epgui an hour ago | parent | prev | next [-] |
| The incompleteness theorem doesn’t mean it’s impossible to formalize all of mathematics. It just means you’ll need to build out “various” mathematics from a landscape of axioms that are not necessarily all compatible with each other. A bit like a multiverse of mathematics. |
|
| ▲ | LPisGood 2 hours ago | parent | prev | next [-] |
| If a theorem has a published proof, it is either formalizable or incorrect. |
| |
| ▲ | fdupress an hour ago | parent [-] | | No. This is not how this works. As the silliest example of this: the Calculus of Inductive Constructions (the core calculus implemented in Lean) has a published proof of its soundness (that you cannot derive False in it). That proof can (probably, thanks to Gödel) not be formalized in Lean or any formal system of axioms weaker than Lean. If what you were trying to do was define what it means for something to be a correct proof, then you must equally admit that there can't be a correct proof of the fact that Lean can't prove False. And if you find that world a happy world to live in while we delegate all concerns about truth to Lean, then I have an infinite hierarchy of monotonically growing bridges to sell you. | | |
| ▲ | LPisGood an hour ago | parent | next [-] | | Yes. This is how this works. Any proof which is correct can be formalized. That is what is means for a proof to be correct. I’m not sure why you are restricting the scope of our discussion to what _Lean_ can(not) formalize. Even if we do choose to do that for some reason, Lean is not a formal system of fixed axioms; it supports optional additional axioms. | |
| ▲ | fpvandoorn an hour ago | parent | prev | next [-] | | 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). | |
| ▲ | whatshisface an hour ago | parent | prev | next [-] | | In principle, a computer can check a nonconstructive proof. I don't know if that's possible in Lean. The interpretation of proofs still assumes the consistency of their axioms. | |
| ▲ | Maxatar an hour ago | parent | prev [-] | | [dead] |
|
|
|
| ▲ | seanhunter 2 hours ago | parent | prev | next [-] |
| Do you honestly Jeremy Avigad (to pick one of the authors) isn't intimately familiar with the Incompleteness Theorems? For starters, Jeremy is chair in logic and philosophy of maths at CMU. https://www.andrew.cmu.edu/user/avigad/ Perhaps you'd like to explain how you think the Incompleteness theorems affect this project? |
| |
| ▲ | lioeters an hour ago | parent [-] | | I think the comment was poking fun at the phrase, "to formalize all of mathematics". 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. | | |
| ▲ | seanhunter 18 minutes ago | parent [-] | | 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... |
|
|
|
| ▲ | wslh 2 hours ago | parent | prev | next [-] |
| I understand that, even taking Gödel's results into account, formalization helps us analyze mathematics and can lead to new (non-mechanical) ideas and results. |
|
| ▲ | fedeb95 2 hours ago | parent | prev | next [-] |
| Also Chaitin would like a few words. |
| |
|
| ▲ | bubbluppugus 2 hours ago | parent | prev [-] |
| Yeah which is why I don't have much sympathy for folks like Tao either The ability to conjure math is practically as endless as time At some point the outcome is just generation of new visual art in the form of syntax We can't physically observe the past or future so we can only theorize and simulate; IMO that's the physical phenomena that belies Incompleteness Theorem; from Earth in the relative year of 2026 my view of the universe is fundamentally incomplete. As such all language describing too far either is incomplete always. It makes any kind of longtermism, religious or agnostic framework espoused by kids of rich academics, empty. We all gonna stick around 10 more generations just to make sure? Whole lot of educated people are just peddling euphemism for religious conviction they steeped in as kids but hid behind atheist semantics like "Intelligent Design." |
| |
