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.)

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.

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.

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?