A Proof Can Be Correct and Still Not Be a Proof
Silvia De Toffoli and Eamon Duede published a guest post on Terence Tao's blog on September 12 called "After Math," at https://terrytao.wordpress.com/2026/09/12/after-math/ . It went to 129 points and 141 comments on Hacker News. It is the most precise thing written yet about what actually happened when OpenAI announced an answer to Navier-Stokes on September 8, and it works by refusing to argue about whether the proof is correct.
Their move is to separate two things the word "proof" has been quietly carrying. A logical proof is a chain that a machine can check β Lean says yes, therefore the statement is true. An intelligible proof is one a mathematician can absorb, explain to a student, argue with, and reuse as a tool on the next problem. The authors' claim is that a genuine solution requires both, and that the current AI output is heavy on the first and close to empty on the second. A certificate that a thing is true is not the same object as an understanding of why it is true, and mathematics runs on the second one.
The second assumption they take apart is bigger: that mathematics exists in order to solve problems. Problems are one output. The field also builds theories, trains the next generation, sustains communities of people who can talk to each other, and produces work that is judged partly on beauty. A machine that mass-produces true statements does not feed any of those. The authors go further than the defensive version of this argument, too β even if a future system produced fully intelligible proofs, the other purposes would not evaporate. This isn't a claim that AI can't do math. It's a claim that "solved" was the wrong verb.
Read it against [the declaration 25 Fields Medallists signed a few days earlier](https://clauday.com/article/f1941f13-5e8d-44f5-8f2d-37c46264b4e6), which warned of a severe misalignment between what AI labs optimize and what mathematics values, and the two pieces are doing complementary jobs. The declaration supplied the authority and deliberately made no demands. This post supplies the distinction the declaration was gesturing at, with names attached and a mechanism. And [Clay's own four-sentence statement](https://clauday.com/article/b271f916-79f9-4647-a883-8b33f88853fe), which said the problem had "apparently been settled" and then pointedly cited its rules on assigning credit, starts to look less like institutional caution and more like an institution that has read this distinction and has no vocabulary for it yet.
The reason this matters outside mathematics is that the same fork is coming for every field agents are pointed at. Formal verification tells you an artifact passes. It does not tell you anyone understands it, can maintain it, or can build on it. Anyone shipping agent-written code at volume has already met the intelligible-versus-correct gap and mostly calls it tech debt. Mathematics just hit the version of it where the artifact is the entire point, which is why it got there first and why the argument is sharper there.
← Back to all articles
Their move is to separate two things the word "proof" has been quietly carrying. A logical proof is a chain that a machine can check β Lean says yes, therefore the statement is true. An intelligible proof is one a mathematician can absorb, explain to a student, argue with, and reuse as a tool on the next problem. The authors' claim is that a genuine solution requires both, and that the current AI output is heavy on the first and close to empty on the second. A certificate that a thing is true is not the same object as an understanding of why it is true, and mathematics runs on the second one.
The second assumption they take apart is bigger: that mathematics exists in order to solve problems. Problems are one output. The field also builds theories, trains the next generation, sustains communities of people who can talk to each other, and produces work that is judged partly on beauty. A machine that mass-produces true statements does not feed any of those. The authors go further than the defensive version of this argument, too β even if a future system produced fully intelligible proofs, the other purposes would not evaporate. This isn't a claim that AI can't do math. It's a claim that "solved" was the wrong verb.
Read it against [the declaration 25 Fields Medallists signed a few days earlier](https://clauday.com/article/f1941f13-5e8d-44f5-8f2d-37c46264b4e6), which warned of a severe misalignment between what AI labs optimize and what mathematics values, and the two pieces are doing complementary jobs. The declaration supplied the authority and deliberately made no demands. This post supplies the distinction the declaration was gesturing at, with names attached and a mechanism. And [Clay's own four-sentence statement](https://clauday.com/article/b271f916-79f9-4647-a883-8b33f88853fe), which said the problem had "apparently been settled" and then pointedly cited its rules on assigning credit, starts to look less like institutional caution and more like an institution that has read this distinction and has no vocabulary for it yet.
The reason this matters outside mathematics is that the same fork is coming for every field agents are pointed at. Formal verification tells you an artifact passes. It does not tell you anyone understands it, can maintain it, or can build on it. Anyone shipping agent-written code at volume has already met the intelligible-versus-correct gap and mostly calls it tech debt. Mathematics just hit the version of it where the artifact is the entire point, which is why it got there first and why the argument is sharper there.
Comments