3 ms·

ctrl+F Gödel ctrl+w

tom_mellior 7y ago
Lovely poem. One reading of it is something like "if computers can't prove that computer proofs are always correct, then we can't be sure of anything", but that is true of human proofs as well, so we might as well Ctrl-W mathematics itself. Another reading is something like "this very introductory article didn't mention whether we can formalize Gödel's incompleteness results in the computer, so it's too introductory for me". Fair enough.
black_knight 7y ago
Gödel’s incompleteness theorems are actually not very relevant to computer formalisation of mathematics. They crushed the naïve hopes of some classical logicians in the beginning of the 20th century. But they do not pose any further restrictions on what computer can do, as opposed to what a human can do, with any specific set of axioms.
fnrslvr 7y ago
If the headline question were something more like "can computers prove all theorems reliably?" this response would be more understandable. But a fairer interpretation would be "do automated theorem proving techniques stand a chance of making novel contributions to the mathematical literature?", to which I think it's pretty unfairly dismissive to rule out the possibility at this point. Considering it's still pretty early days for automated theorem proving, there's already some promising progress: an automated prover resolved the Robbins conjecture. If you think Gödel's incompleteness theorems are hard evidence that computers can never consistently perform on the same level as humans at theorem proving, take it from someone who understands Gödel's results well: you're mistaken. --- I think one sense in which the headline seems a little misleading, though, is that on a skim it looks like it's more about formalizing mathematical knowledge so that computers can verify theorems proven largely by people, than it is about computers themselves proving the theorems. (Which is also a fine topic, I'm not complaining.)
ColinWright 7y ago
That's a short and pithy response, but I'd like to know more. Imagine, if you will, that you are addressing an audience that knows what Gödel's results are. In particular, assume that we know Gödel's proof that any formal system that's sufficiently complex to hold a model of arithmetic has statements that are true, but unprovable within the system. Now, can you explain to us why this result makes it pointless to read the article?

ctrl+F Gödel ctrl+w

Lovely poem. One reading of it is something like "if computers can't prove that computer proofs are always correct, then we can't be sure of anything", but that is true of human proofs as well, so we might as well Ctrl-W mathematics itself. Another reading is something like "this very introductory article didn't mention whether we can formalize Gödel's incompleteness results in the computer, so it's too introductory for me". Fair enough.

black_knight 7y ago

Gödel’s incompleteness theorems are actually not very relevant to computer formalisation of mathematics. They crushed the naïve hopes of some classical logicians in the beginning of the 20th century. But they do not pose any further restrictions on what computer can do, as opposed to what a human can do, with any specific set of axioms.

fnrslvr 7y ago

If the headline question were something more like "can computers prove all theorems reliably?" this response would be more understandable. But a fairer interpretation would be "do automated theorem proving techniques stand a chance of making novel contributions to the mathematical literature?", to which I think it's pretty unfairly dismissive to rule out the possibility at this point. Considering it's still pretty early days for automated theorem proving, there's already some promising progress: an automated prover resolved the Robbins conjecture. If you think Gödel's incompleteness theorems are hard evidence that computers can never consistently perform on the same level as humans at theorem proving, take it from someone who understands Gödel's results well: you're mistaken. --- I think one sense in which the headline seems a little misleading, though, is that on a skim it looks like it's more about formalizing mathematical knowledge so that computers can verify theorems proven largely by people, than it is about computers themselves proving the theorems. (Which is also a fine topic, I'm not complaining.)

ColinWright 7y ago

That's a short and pithy response, but I'd like to know more. Imagine, if you will, that you are addressing an audience that knows what Gödel's results are. In particular, assume that we know Gödel's proof that any formal system that's sufficiently complex to hold a model of arithmetic has statements that are true, but unprovable within the system. Now, can you explain to us why this result makes it pointless to read the article?