MATHEMATICS / PHILOSOPHY · 30 SEP 2026

What is a proof for?

Verification is one job of a proof. Understanding is another.

sk a mathematician what a proof is and you will get a clean answer: a finite chain of deductions from axioms, each step licensed by a rule of inference. Ask them what a proof is for and the answers scatter. Certainty, obviously. But also understanding, communication, discovery, and something harder to name, the thing that makes a mathematician read a correct proof and still feel they do not yet know why the theorem is true. That gap between verification and understanding is where the philosophy of proof lives, and it has become urgently practical, because machines are now very good at one side of it and still poor at the other.

Start with the official story. Proof as certification. A theorem is a claim; a proof is the audit that admits it to the canon. This view has a rigorous modern form in formal logic, and it delivers real value: mathematics is the one field where truth, once established, stays established. No replication crisis, no statistical dispute about whether the prime numbers really do thin out the way the prime number theorem says.

But certification is not why mathematicians prove things, most of the time. William Thurston, one of the great geometers of the twentieth century, made this point memorably in his 1994 essay "On Proof and Progress in Mathematics." Mathematics, he argued, is not a pile of theorems. It is a structure of understanding held by people, and proofs are one of the ways that understanding is built and transferred. A proof you have read and verified line by line can still leave you unable to say what the theorem is really about, why it had to be true, what would break if you changed an assumption. The certificate is valid; the insight is missing. Conversely, a mathematician can be convinced a result is true, correctly, from an outline that would not pass as a formal proof, because the outline transmits the idea and the idea does the convincing.

This is why mathematicians re-prove known theorems. Gauss gave multiple proofs of quadratic reciprocity and kept looking for more. Each new proof is not redundancy; it is a new route into the same territory, revealing new connections, new generalizations, new reasons. If proof were only certification, the second proof would be waste. In practice it is often where the progress is.

The tension went public in 1976, when Appel and Haken announced a proof of the four color theorem: every planar map can be colored with four colors so that no neighbors share a color. Their proof required a computer to check an enormous number of cases, far more than any human could inspect. The certification was, by the standards of the day, solid. The reaction was not celebration but unease. Was it a proof if no human could follow it? The philosophical fight that followed was really about the two jobs of proof pulling apart. The computer had delivered verification without understanding. Nobody learned from it why four colors suffice; they learned only that they do.

Fast forward fifty years and that same tension has become an industry. Interactive theorem provers like Lean let mathematicians write proofs that a small, trusted kernel checks mechanically, down to the axioms. The verification is now not just reliable but industrial-grade, and the culture is shifting: major results are being formalized, and a growing library of mathematics exists in machine-checked form. Meanwhile, AI systems have learned to find proofs, sometimes olympiad-grade ones, and to translate informal mathematics into formal code, a task called autoformalization.

Read the situation through Thurston's lens and it looks different from both the hype and the dismissal. Machines are racing ahead on the certification side. A formal proof checked by a kernel is the strongest verification mathematics has ever had, and AI assistance is making it cheaper to produce. But the understanding side does not compress the same way. A mathematician staring at a machine-found proof of an interesting statement often has exactly the 1976 problem: the result is banked, the insight is not. What the field then wants is not another verification but a proof of a different kind, one that explains. And explanation, it turns out, is not a softer or vaguer requirement. It is a specific functional demand: a structure a mind can hold, compress, and reuse on new problems.

This gives a clean way to think about what AI will and will not change in mathematics. Verification will get cheap, and that is a bigger deal than it sounds: entire categories of "we think this is right but the details are a swamp" can be settled, and large collaborations can trust each other's contributions at machine speed. Conjecture generation will accelerate too, because systems that can search proof space also stumble into statements worth proving. But the unit of progress in mathematics was never the verified statement. It was the idea that lets a person see the statement as inevitable. Until machines can produce those reliably, and the honest verdict is that they cannot yet, the mathematician's job changes shape more than it shrinks: less clerk, more reader, more judge of which routes into the territory are worth building roads along.

There is a tempting analogy to chess, where the engines won and the humans kept playing, diminished. Mathematics looks more like chess's opposite. The point of a game is to win it, and the engine does. The point of a proof was never only to win the theorem. It was to make the theorem yours. A field that can verify everything and understand nothing would be a kind of epistemic bankruptcy with perfect paperwork.

So what is a proof for? Three things, and the order matters. It verifies, and machines now verify better than we do. It explains, and explanation is still ours to demand, from ourselves and from any system that claims to do mathematics. And it teaches the next person who has to go further, which is the quiet reason proofs are written in words at all. The axioms are the floor. The understanding is the house. Machines are pouring excellent concrete. Someone still has to know what the building is for.