5 ms·

I'm a mathematician, but I don't really understand Gödel's incompleteness. I've recently been reading everything I can about proof assistants such as Coq and Le

I'm a mathematician, but I don't really understand Gödel's incompleteness. I've recently been reading everything I can about proof assistants such as Coq and Lean, and Homotopy Type Theory and such. My lay understanding is that Gödel's incompleteness put a dagger through Hilbert's vision of automating mathematics. And now we're automating mathematics. I of course oversimplify, but what gives? You'd think all popular accounts of Gödel or proof assistants would name-check Hilbert (as this article does just before the paywall) then reconcile this apparent conflict. Someone here understands this well. Can you explain?

tim_hutton 5y ago
Gödel's incompleteness isn't a practical obstacle to proof assistants - it will never stop us formalizing proofs and searching for new theorems. It's irrelevant to their operation and will continue to be for all time. If Gödel's incompleteness applies to the theorem you are trying to prove then it means that the theorem has been very carefully set up with reference to the axioms that you are using in order to be unprovable. It's not something you will stumble across otherwise. Think of it like this: imagine knowing that maths will stop working if a certain very specific enormous number appears in your calculation. This would keep mathematicians up at night with worry but it would have no practical effect on anyone else because the enormous number simply never appears.
- sva_ 5y ago
  But as I also understand it, Goedel's incompleteness theorem also implies that for any given axiomatic system, if you have any finite number of theorems/proofs, you can never know if these are all theorems/proofs possible in that system. Hence it isn't possible to "finish" any axiomatic system, in the sense that no number of theorems/proofs will ever "complete" it. I might be wrong though. But if I understand it correctly, that's not a bad thing at all. It means that there might always be more out there to discover. Some dub Goedel's incompleteness a 'bug' of mathematics, I think it's actually a feature.

tim_hutton 5y ago

Gödel's incompleteness isn't a practical obstacle to proof assistants - it will never stop us formalizing proofs and searching for new theorems. It's irrelevant to their operation and will continue to be for all time. If Gödel's incompleteness applies to the theorem you are trying to prove then it means that the theorem has been very carefully set up with reference to the axioms that you are using in order to be unprovable. It's not something you will stumble across otherwise. Think of it like this: imagine knowing that maths will stop working if a certain very specific enormous number appears in your calculation. This would keep mathematicians up at night with worry but it would have no practical effect on anyone else because the enormous number simply never appears.

sva_ 5y ago
But as I also understand it, Goedel's incompleteness theorem also implies that for any given axiomatic system, if you have any finite number of theorems/proofs, you can never know if these are all theorems/proofs possible in that system. Hence it isn't possible to "finish" any axiomatic system, in the sense that no number of theorems/proofs will ever "complete" it. I might be wrong though. But if I understand it correctly, that's not a bad thing at all. It means that there might always be more out there to discover. Some dub Goedel's incompleteness a 'bug' of mathematics, I think it's actually a feature.