What a Proof Is Now
For twenty-three centuries a proof was something a person could read and be convinced by. In 1976 that stopped being true, and the question of what mathematics is has quietly turned into a question about who — or what — is doing the knowing.
In 1929 G. H. Hardy, the most fastidious pure mathematician of his generation, wrote an essay called “Mathematical Proof” and said something in it that he presumably did not want his students to hear. There is, strictly, no such thing as mathematical proof, he wrote; proofs are what he and Littlewood called gas — rhetorical flourishes designed to affect psychology, pictures on the board in the lecture, devices to stimulate the imagination of pupils.[1] What a mathematician actually does, on Hardy's account, is see something, and then point at it until other people see it too.
That is a strange thing for a Platonist to say, and Hardy was a Platonist. But it makes the point that this essay is about. A proof does two jobs. It certifies: this statement follows from those premises, with no gap. And it explains: here is why, in a form that a trained mind can hold and be moved by. From Euclid to about 1976 both jobs were done by the same object, a written argument, and both were done by the same act, a human being reading it. The two jobs have since come apart, and the object that certifies is increasingly one that no human has read.
The first two essays in this series argued that we invent the rules and discover the consequences, and that the rules run out. This one is about the machinery in between — proof, the thing that turns rules into consequences — and what has happened to it. The short version is that the machinery has become something we build rather than something we do, and that changes what “knowing a theorem” means.
The theorem that kept changing its subject
Before the machines, the best evidence that mathematics is made came from watching mathematicians argue. In 1750 Euler wrote to Goldbach with an observation that had somehow escaped the Greeks: for any polyhedron, the number of vertices minus the number of edges plus the number of faces is two.[2]
A cube has 8, 12 and 6: two. A tetrahedron has 4, 6 and 4: two. Cauchy gave a proof in 1813 by flattening the polyhedron onto a plane and collapsing it triangle by triangle.[3] And then the counterexamples began. Simon Lhuilier pointed out in 1812 that a polyhedron with a tunnel through it — a picture frame — gives zero, and one with a hollow cavity inside gives four.[3] Two tetrahedra glued along an edge give three. Kepler's star polyhedra, if you count their self-intersecting faces honestly, give negative numbers.
Imre Lakatos told the story in Proofs and Refutations, first published as a series of papers in 1963 and 1964, as a classroom dialogue, and the interesting part is not the counterexamples but what mathematicians did with them.[4] First they refused to admit that the offending objects were polyhedra at all — Lakatos calls this monster-barring. Then they narrowed the theorem to exclude the monsters — exception-barring. Then, more honestly, they went back to Cauchy's proof, found the step that silently assumed the polyhedron could be flattened without tearing, and built that assumption into the statement. The theorem ended up true, but of a class of objects — the simply connected polyhedra — that had been carved out precisely so that it would be. Poincaré finished the job by showing that V − E + F is a topological invariant, equal to 2 minus twice the number of holes, at which point the original theorem was less a discovery about polyhedra than a definition of what it means to have none.
Lakatos's phrase for this was proof-generated concepts. The objects of mathematics, on his account, are not given in advance and then reasoned about; they are refined in the course of the reasoning, and the refinements are chosen to save the theorems people care about. This is the constructivist's strongest evidence, and it comes not from philosophy but from the archive. The realist's reply is that Euler saw something real — that the Euler characteristic was there to be found — and that the century of argument was the slow process of finding out what it was a characteristic of. Both are right, and the division of labour from the first essay covers it: the concept of “polyhedron” was negotiated, and the invariant was not.
Four colours, twelve hundred hours
In 1852 Francis Guthrie, colouring a map of the English counties, noticed that four colours seemed to suffice to keep any two neighbouring regions distinct, and asked whether that was always true. Alfred Kempe published a proof in 1879 that was accepted for eleven years, until Percy Heawood found the hole in it in 1890 — though Kempe's argument, repaired, does prove that five colours suffice.[5] Then nothing, for eighty-six years.
In June 1976 Kenneth Appel and Wolfgang Haken at the University of Illinois announced a proof.[6] Its strategy was old: show that every map must contain one of a finite list of configurations, and show that each configuration can be reduced — that a colouring of the rest of the map can always be extended across it. The list had 1,936 entries. Checking that every one of them was reducible took about twelve hundred hours on an IBM mainframe, and the checking was not something a person could repeat, or even in any meaningful sense read. The University of Illinois mathematics department changed its postmark to Four colors suffice. A substantial number of mathematicians declined to consider the theorem proved.
The philosopher Thomas Tymoczko put the objection precisely in 1979.[7] A proof, on the traditional account, is surveyable: a competent mathematician can, in principle, go through every step and be convinced by each one. The Appel–Haken proof was not. Its correctness depended on the correctness of a computer program and on the hardware it ran on, and belief in it therefore rested on empirical grounds — the reliability of a physical machine — of exactly the kind that mathematics had always claimed to be free of. If we accept it, Tymoczko argued, we have changed what the word “proof” means.
What happened next is the instructive part. In 1996 Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas gave a cleaner proof, with 633 configurations instead of 1,936; it still needed a computer.[8] Then in 2005 Georges Gonthier, at Microsoft Research, did something no one had done with a major theorem before: he wrote the entire proof — the human parts and the machine parts, the topology and the combinatorics and the case-checking — in a formal language called Coq, and had the Coq kernel verify every step against the axioms.[9] The proof that had been doubted because a machine had done part of it became, after a machine had checked all of it, the most thoroughly certified theorem in mathematics. The objection had not been answered. It had been inverted.
Ninety-nine per cent
Thomas Hales announced a proof of the Kepler conjecture in 1998 — the claim, made by Kepler in 1611 and believed by every grocer since, that no way of stacking spheres is denser than the obvious one. The proof was about 250 pages of mathematics plus some 40,000 lines of code and three gigabytes of data, and Hales submitted it to the Annals of Mathematics.[10] The journal assembled a panel of twelve referees, led by Gábor Fejes Tóth, and they worked on it for four years. Their conclusion, relayed by the editor Robert MacPherson, was that they were ninety-nine per cent certain the proof was correct, and that they could not certify the computer calculations. The Annals published it in 2005.
Hales found the ninety-nine per cent unacceptable, and in 2003 he began a project, Flyspeck, to remove the one per cent.[10] It took eleven years and around twenty collaborators. In August 2014 the complete proof of the Kepler conjecture — every lemma, every inequality, every case — had been checked by the proof assistants HOL Light and Isabelle. The verified proof is not a document a mathematician reads. It is an artefact: a body of code whose acceptance by a small, heavily scrutinised kernel program constitutes the certification. Nobody has surveyed it and nobody will. It is, by any reasonable standard, the most certain theorem Kepler's name is attached to, and it is certain in a way that has nothing to do with anyone understanding it.
The tensor experiment and the working mathematician
Until about 2020 formal verification was something that happened to famous theorems long after they were proved, by specialists, at great cost. Then it started happening to new mathematics, done by the people who were doing the mathematics.
Lean is a proof assistant developed at Microsoft Research by Leonardo de Moura from 2013; mathlib is the community library of mathematics written in it, driven from Imperial College by Kevin Buzzard, which by the mid-2020s had grown to well over a million lines and covered most of an undergraduate degree and a good deal beyond. In December 2020 Peter Scholze — a Fields Medallist, and about as far from the formal-methods world as a mathematician can be — posted a challenge.[11] He and Dustin Clausen had built a theory they called condensed mathematics, and a central result in it rested on a long and delicate proof that Scholze admitted he was not entirely sure of. Would the Lean community check it?
Johan Commelin led the effort.[11] The key theorem was verified in June 2021 and the whole result, the Liquid Tensor Experiment, in July 2022. Two things came out of it that mattered more than the verdict. First, Scholze said that the formalisation had given him confidence in a proof he had not fully trusted; the machine had done for him what the referees had done for Hales, but in eighteen months rather than four years and to a standard of certainty the referees could not reach. Second, and less expected, the process of formalising had clarified the argument: the parts that were hard to formalise turned out to be the parts that were genuinely subtle, and the effort of stating them precisely produced a better proof than the one Scholze had started with.
The pace has since become the story. In November 2023 Tim Gowers, Ben Green, Freddie Manners and Terence Tao proved a conjecture in additive combinatorics; the paper was formalised in Lean, by around twenty volunteers coordinating online, in about three weeks.[12] In 2024 Tao launched a project to determine, among 4,694 possible equational laws for a binary operation, which imply which — some twenty-two million questions — and a mixed crowd of mathematicians, programmers and automated provers settled essentially all of them within a year.[13] No single participant understands the result. In October 2024 Buzzard began a five-year project to formalise Wiles's proof of Fermat's Last Theorem in full. And in July 2024 a DeepMind system called AlphaProof, working inside Lean, solved four of the six problems on that year's International Mathematical Olympiad, which put it at the level of a silver medal; a year later, systems from DeepMind and OpenAI reached gold-medal level working in plain language, within the competition's time limit.[14]
This is where the series meets another one on this blog. How We Know Software Works is about the ladder that runs from “we tested it” to “we proved it”, and about how far up that ladder the software industry has been willing to climb. The tools are the same — Coq, Isabelle, Lean — and the two disciplines are approaching the same rung from opposite directions: engineers climbing up toward proof because testing is not enough, mathematicians climbing down toward mechanical checking because reading is no longer enough. The rung is the same in both cases: a certificate a machine can verify and a human can, with effort, still follow.
What certifies and what explains
William Thurston, who did as much as anyone in the twentieth century to reshape geometry, wrote an essay in 1994 called “On proof and progress in mathematics” in reply to colleagues who had proposed dividing the field into rigorous and speculative wings.[15] Mathematics, he said, is not the production of theorems. It is the advancement of human understanding of mathematics; theorems are how the understanding is stored and transmitted, but a result that has been proved and not understood has not yet done its job. He gave his own experience as evidence. When he had proved things quickly and well in the 1970s, other people stopped working on them — the certificate was in, and the explaining was left undone — and the field went quiet in a way that helped nobody.
The two jobs do not only come apart at the machine end. Grigori Perelman posted his proof of the Poincaré conjecture in three preprints in 2002 and 2003, written by a human in ordinary mathematical prose, and it took three separate teams three years to confirm that the argument was complete.[16] Shinichi Mochizuki posted a claimed proof of the abc conjecture in 2012, some 500 pages built on a theory he alone had developed; Scholze and Jakob Stix travelled to Kyoto in 2018 and reported that they could not follow a crucial step; the papers were nonetheless published in 2021, in a journal of which Mochizuki was editor-in-chief; and as of this writing the mathematical community does not accept the proof, without anyone being able to demonstrate that it is wrong.[17] That is the surveyability problem with no computer anywhere in sight, and it is the case the Lean community points to when asked what formalisation is for.
The interface
For the question this series is about, the computer proofs push in a surprisingly clear direction. The four colour theorem is true. It was true in 1852 and it is true now, and it is true whether or not any mind has ever seen why, because no mind has, and yet the certification is complete. If truth in mathematics required human understanding, the four colour theorem would be in some odd limbo; it is not. That is a realist's point, and it has been made stronger by every formalisation since — the theorems stand independently of anyone's grasp of them.
But Lakatos's point stands alongside it, untouched. The concepts the theorems are about — polyhedron, continuity, the specific class of objects the four colour theorem quantifies over — were built, argued over, revised, and revised again, and the theorems were preserved partly by changing what they were about. The formal proof of the four colour theorem is a proof about planar graphs, and “planar graph” is a made thing, a definition tuned over a century to make a class of arguments go through.
Structuralism, again, is where this lands. The structures are found; the vocabulary for them is made; and proof is the interface between the two — the place where the made vocabulary is shown to fit the found structure. What has changed since 1976 is that the interface now has two faces that no longer coincide. One is a certificate that a machine produces and a machine checks. The other is an explanation that a mind produces and a community absorbs. Hales got the first and waited eleven years for it; Scholze got both, and said the second was worth more.
The risk Thurston named is a mathematics of certificates that nobody understands — a library of verified theorems that advances nothing, because the understanding that would let anyone build on them was never produced. The opportunity is a division of labour inside proof itself: machines certify, people explain, and each is freed to do the thing it is good at. Which of these we get is not a philosophical question. It is a question about what mathematicians choose to reward, and it will be settled, like the choice of axioms, by what the practice converges on.
The last essay in the series leaves the machines and goes the other way: into the brain, to ask where the capacity for any of this comes from, and why an organ that evolved to estimate should have produced a science that does not.
Where this could go
Who checks the checker. Every formal proof rests on a kernel — a few thousand lines of code that is trusted because it is small and has been audited. The de Bruijn criterion, verified kernels, and the question of what a bug in Lean's type checker would and would not undermine are the same problem this blog's software series faces from the other side. A joint piece would be the natural bridge between The Shape of the Problem and this one.
The machines, dated. Claims about AI and mathematics go stale in months and are routinely overstated on the way through the press. A running, dated record — what was solved, at what level, with how much human translation, and which announced results were later found to be rediscoveries — would be more useful than any single essay, and would let the third-essay argument be re-run every year.
Polymath and the crowd. Gowers's Polymath projects from 2009 onward, and Tao's equational theories project, are a third mode of proof: neither a mind nor a machine but a crowd, with the understanding distributed and no participant holding the whole. Whether that counts as explanation, in Thurston's sense, is a real question, and the participants have written about it.
Explanation, made precise. Philosophers have tried to say what makes one proof explanatory and another merely valid — Mark Steiner in 1978, Marc Lange more recently. If the distinction can be formalised even roughly, it could be tested against which proofs mathematicians actually prefer, and against what the machines produce.
abc, resolved. The Mochizuki case will end one way or another: with a formalisation, a located error, or a generation of Kyoto students who can explain it to the rest of the world. Whichever it is will be the best available case study in how the community decides a proof is a proof, and it is worth watching with the essay's two-jobs distinction in hand.
This piece was written collaboratively with Claude Fable 5.1 (Anthropic): human specification, editorial direction and critical review; machine synthesis, drafting and figure generation. It is Part III of Found or Made.
The timeline figure uses the dates of the cited papers. The Euler-characteristic counterexamples — the picture frame at 0, the hollow cube at 4, two tetrahedra on an edge at 3 — were recounted by hand from vertices, edges and faces.
Two kinds of claim here go stale or are secondhand, and are marked. The state of machine-assisted mathematics is dated to July 2025 and will be wrong within a year; the open thread proposes a running record for exactly that reason. The Hales–Annals “ninety-nine per cent” episode and Scholze's remarks on the Liquid Tensor Experiment are retold from published accounts and blog posts, paraphrased rather than quoted. The Mochizuki paragraph states the community's position as of this writing and will need revisiting.
The distinction the essay rests on — proof as certificate, proof as explanation — is Thurston's and Lakatos's, not the authors'. What is ours is the claim that the two have come apart, and the worry about which one gets rewarded.
Authored by: Luis Matos Ferreira — Physicist, Developer, Writer
- Invented, Then Unavoidable — imaginary numbers, rigidity, and why physicists trust beauty.
- The Limits of the Rules — Gödel, Goodstein, the continuum, and what happens when the axioms run out.
- What a Proof Is Now — Lakatos, the four colour theorem, Lean, and proofs no one has read. This essay.
- Where Number Comes From — the number sense, cultures without counting, and whether aliens would share our arithmetic.
- The Bus at Coutances — how mathematicians and physicists actually think: images, incubation, birds and frogs, and minds without pictures.
- Chance, Necessity and Convention — afterword: Monod's pair, and the third term the sciences need.
See also, on this blog: The Cheap End of Rigour and The Shape of the Problem, on formal methods in software.
- Hardy, “Mathematical Proof”, Mind, 1929.
- Euler, letter to Goldbach, 1750; “Elementa doctrinae solidorum”, 1758.
- Cauchy, “Recherches sur les polyèdres”, 1813; Lhuilier, “Mémoire sur la polyédrométrie”, 1812–13.
- Lakatos, “Proofs and Refutations”, British Journal for the Philosophy of Science, 1963–64; book edition, 1976.
- Kempe, “On the geographical problem of the four colours”, 1879; Heawood, “Map-colour theorem”, 1890.
- Appel & Haken, “Every planar map is four colorable”, Illinois Journal of Mathematics, 1977 (Part II with Koch).
- Tymoczko, “The four-color problem and its philosophical significance”, Journal of Philosophy, 1979.
- Robertson, Sanders, Seymour & Thomas, “The four-colour theorem”, Journal of Combinatorial Theory B, 1997.
- Gonthier, “Formal proof — the four-color theorem”, Notices of the AMS, 2008.
- Hales, “A proof of the Kepler conjecture”, Annals of Mathematics, 2005; Hales et al., “A formal proof of the Kepler conjecture”, Forum of Mathematics, Pi, 2017.
- Scholze, “Liquid tensor experiment”, Xena blog, December 2020; Commelin et al., completion announced July 2022; Scholze, “Liquid tensor experiment”, Experimental Mathematics, 2022.
- Gowers, Green, Manners & Tao, “On a conjecture of Marton”, 2023; Lean formalisation, December 2023.
- Tao et al., Equational Theories Project, 2024–25.
- DeepMind, “AI achieves silver-medal standard solving International Mathematical Olympiad problems”, July 2024; gold-medal results announced by DeepMind and OpenAI, July 2025.
- Jaffe & Quinn, “Theoretical mathematics”, 1993; Thurston, “On proof and progress in mathematics”, Bulletin of the AMS, 1994.
- Perelman, arXiv preprints, 2002–03; Kleiner & Lott, Morgan & Tian, Cao & Zhu, 2006.
- Scholze & Stix, “Why abc is still a conjecture”, 2018; Mochizuki, Publications of the RIMS, 2021.
Comentários
Enviar um comentário