When Proofs Become Cheap: AI and the Future of Mathematics

Editorial image generated by the author.

On 11 September 2026, twenty-five Fields Medallists were the initial signatories to an unusually blunt warning about artificial intelligence and mathematics. In A Severe Misalignment of AI in Mathematics, they argued that using famous mathematical problems as AI benchmarks risks confusing what mathematics can easily measure with what mathematics actually values.

The concern is not that AI systems cannot solve difficult problems. It is almost the opposite. Historically, solving a famous problem usually indicated that somebody had developed new ideas, techniques or understanding along the way. The solution was valuable partly because of the mathematical structure created around it. If machines can mass-produce solutions without those results being absorbed into the intellectual structure of the field, that old relationship breaks down. We can accumulate proofs without necessarily accumulating much understanding.

Much of this criticism is convincing. A million formally checked proofs would not by themselves constitute a million useful mathematical insights. But a further claim is less obvious: that the interpretation, simplification and integration of those proofs must remain fundamentally human. Understanding does not always have to precede a proof. Sometimes it is constructed afterwards. If AI makes one stage of mathematics cheap, the scarce work may simply move somewhere else.

Proof Is Not the Same as Understanding

Terence Tao develops the strongest version of the concern in Mathematics in the Age of AI, an essay based on his 2026 International Congress of Mathematicians lecture. He separates mathematical problem-solving into a chain of activities: solving a problem, verifying the solution, explaining the proof, having the mathematical community digest it, and eventually incorporating the useful parts into the accepted theory of the field.

The later stages matter enormously. A proof can establish that a formalised statement follows from its encoded assumptions without being a good explanation of the mathematics. Formal verification also does not remove every specification question: the formal statement still has to capture the theorem we intended to prove. Even when those issues are settled, a correct proof may give little indication of why the result matters, which parts of the argument are reusable or how it connects to neighbouring mathematics.

Tao therefore expects a transition from proof scarcity to proof abundance. If AI systems produce proofs faster than mathematicians can inspect, explain and absorb them, the bottleneck moves downstream. Journals, peer review and mathematical careers developed in a world where finding a difficult proof was expensive. They may behave badly in one where proofs arrive faster than anyone can read them.

I think this diagnosis is largely right. Where I am less convinced is the boundary drawn around what comes next.

There is a familiar picture of mathematical discovery in which understanding precedes the proof: problem → exploration → insight → proof → understanding. Mathematicians can spend months or years trying approaches that fail, and the failures themselves generate knowledge. Unexpected examples appear. Definitions change. Useful lemmas emerge. Eventually the mathematician sees enough of the structure to prove the theorem.

But mathematics does not always develop in that order. The first proof of an important result may be long, technical and conceptually awkward. Later mathematicians simplify it. Someone notices that several ugly steps are instances of one principle. Better notation exposes the structure. A more general theorem absorbs the original result as a special case. Eventually a textbook presents an argument quite different from the route by which the mathematics was discovered.

The chronology can therefore run another way: problem → messy search → proof → simplification → abstraction → understanding. If so, replacing some of the messy search with automated exploration does not automatically remove the later stages. It changes who, or what, performs them.

Imagine an AI system produces a formally verified proof containing fifty thousand steps. That is not yet satisfying mathematics, but it can become an object of mathematical investigation. Which lemmas carry most of the argument? Which assumptions are actually necessary? Are several technical manoeuvres manifestations of the same invariant? Can the theorem be strengthened? Is there a shorter route? What would the proof look like if written for someone trying to understand the central idea rather than merely check the conclusion?

Those are mathematical questions, and there is no principle saying that whoever answers them must also have carried out the original proof search. Mathematics already separates those roles across generations. The person who first establishes a theorem, the person who later finds the elegant proof and the textbook author who gives the result its canonical form may all be different people.

A striking recent example makes that separation unusually concrete. An internal research version of Claude produced a technically intricate proof that more than 67.25% of the non-trivial zeros of the Riemann zeta function are simple and lie on the critical line, a result subsequently verified by Levent Alpöge and Ralph Furman. Youness Lamzouri then published a shorter, conceptually simpler proof that replaces much of the finite-dimensional matrix machinery with a Hilbert-space inequality. The machine-assisted result was not made irrelevant by the later proof; establishing the result and finding a form in which its mechanism became easier to see were separate mathematical achievements.

AI could enlarge that separation dramatically. A system might explore millions of candidate routes, produce several successful proofs and then compare them for common structure. Humans could examine the landscape instead of personally walking every path through it. Other AI systems could participate in the comparison and compression. This is close to the broader question I have considered before about whether AI gives science more paths or begins to change the map itself.

None of this guarantees understanding. A final proof can discard information contained in the search that produced it. Failed attempts may reveal why particular definitions matter or why an apparently natural strategy cannot work. Tao makes a related point about the useful friction in human mathematical writing: the places where an author struggled can tell the reader where the genuine difficulty lies.

That suggests a problem in how mathematical AI is designed, however, rather than a reason to preserve human proof search as a principle. A useful system should not simply accept a conjecture, emit a certificate and discard everything else. Where possible, it could preserve failed candidate approaches, counterexamples, intermediate lemmas, alternative proofs and dependency structures. Its search history would itself become research material.

There is an obvious limit. An AI's internal process is not necessarily a tidy mathematical notebook waiting to be opened. Relevant computation may be distributed across model activations, repeated sampling, external tools and enormous numbers of discarded candidates. Producing an intelligible research record would require deliberate engineering. But the underlying distinction remains: the problem is not that a machine performed the search. The problem is if the useful information generated by the search disappears with it.

The Mathematician and the Pencil

There is a useful parallel with Leonard Read's famous essay I, Pencil. An ordinary pencil embodies a chain of knowledge no single person possesses. One person understands forestry, another graphite, others machinery, paint, glue or transportation. The pencil exists because economic organisation allows each participant to rely on expertise they do not personally reproduce.

The same principle operates throughout intellectual life. A molecular biologist does not manufacture a sequencing machine before using it. An astronomer does not build every component of a telescope. A software engineer relies on operating systems, compilers and processors whose complete construction exceeds the knowledge of any individual user. Mathematics already works this way too: mathematicians use theorems whose proofs they have not personally reconstructed, physicists apply mathematics they could not derive from first principles, and computer algebra systems perform manipulations that would contribute little if researchers had to execute them manually.

Knowledge becomes more powerful because people can build on intellectual labour they did not themselves perform.

The pencil analogy has a limit. Producing the pencil is largely the objective, whereas trying to prove a theorem can generate valuable knowledge beyond the finished result. There is another difference: the pencil's production process distributes expertise among many humans, each of whom understands some part of the chain. A sufficiently capable AI could instead concentrate several intellectual stages inside machinery that no person fully understands.

Those differences stop the analogy from proving that mathematical automation is harmless. They do not prove the opposite either. A difficult intermediate activity may have been a productive source of understanding without the difficulty itself being something mathematics needs to preserve forever.

When Twenty-Two Million Answers Are Not Enough

One of the most revealing demonstrations of the problem comes from Tao's own work. The Equational Theories Project, a large collaborative effort using Lean formalisation, automated theorem proving and human contributions, determined all 22,028,942 implications among a set of 4,694 simple equational laws for magmas. The very scale of the achievement creates an intellectual problem. Twenty-two million answers are far too many for any mathematician to absorb individually.

In March 2026, Tao and Damek Davis therefore launched the Mathematics Distillation Challenge. Its first stage asked participants to compress useful knowledge from those millions of results into a human-readable cheat sheet no larger than ten kilobytes, then test whether the compressed representation helped relatively cheap AI models answer previously unseen implication problems.

This is almost a miniature version of the future the wider debate is worried about. The expensive object had already been created: an enormous landscape of settled mathematical relationships. The interesting problem was no longer how to generate one more answer, but how to find a compact representation that captured enough structure to be useful elsewhere. Abundance had created a new scarcity.

That scarcity is distillation. Mathematics is powerful partly because it compresses enormous numbers of particular facts into comparatively small conceptual structures. We do not teach students a million examples of differentiation; we teach calculus. We do not catalogue every numerical relationship among the sides of right triangles; we use a theorem. A successful abstraction allows a mind to replace many separate statements with a structure from which those statements can be understood or reconstructed.

If AI makes individual proofs cheap, producing another theorem may gradually become less impressive. The valuable contribution could shift from establishing one isolated result to discovering the abstraction that makes thousands of results comprehensible. The achievement is no longer “Here are 5,000 true statements,” but “These 4,300 statements are consequences of the same idea.”

This is a harder target for automation than formal verification. Correctness can often be specified precisely; importance cannot. Mathematicians care about usefulness, explanatory power, elegance, surprising connections, tractability and whether an idea creates fertile new questions. Different research communities can reasonably disagree about which of those qualities matter most. Mathematical significance is partly a judgement made by a community rather than a property checked by a formal kernel.

That is one of the strongest arguments for an enduring human role. But “harder to optimise” is not the same thing as “uniquely human.” An AI able to inspect millions of proofs may have unusual advantages when searching for recurring structures. It could test alternative abstractions against unseen problems, compare competing formulations by how much mathematical territory they compress, or discover that techniques treated as unrelated in the existing literature repeatedly instantiate the same pattern.

Some of those activities already sound uncomfortably close to what mathematicians call understanding. Whether machines will become good at them is an empirical question. It should not be settled in advance by defining understanding as whatever humans continue to do after machines have taken over the previous task.

Research Is Not Education

The needs of mathematical research also have to be separated from the needs of mathematical training. A professional researcher may benefit enormously from having a machine eliminate a week of routine proof search. A student may need exactly that week of struggle because the objective of the exercise is not merely to obtain the answer. It is to develop the ability to reason about the problem.

Calculators did not make arithmetic useless to teach. They changed which arithmetic deserves repeated manual practice and at what stage. Computer algebra did not eliminate the need to understand algebra; it made it less sensible to spend professional research time performing certain manipulations by hand. Proofs may acquire the same distinction.

There may therefore be excellent educational reasons for students to prove theorems themselves even in a world where machines can produce those proofs instantly. The September declaration is right to worry about a training process that produces answers without developing mathematical judgement. But that does not imply that research mathematics should deliberately preserve proof scarcity. Difficulty can be instrumentally valuable without being intrinsically valuable.

Does Distillation Have to Be Human?

The September declaration goes further than warning about bad benchmarks. It argues that AI-generated ideas need mathematicians to develop them, connect them with previous work and integrate them into the mathematical canon; without that process, the profession's human transmission chain would be lost.

The cultural concern is persuasive. Mathematics is not merely a database of true statements. It is a community in which people teach one another ways of seeing structures and problems. A world in which machines generated millions of results that no person could follow might preserve mathematical truth while hollowing out mathematics as a human practice.

But this combines two different questions. One is whether human beings should continue to practise mathematics. I hope they do. Mathematics provides intellectual pleasure, education, aesthetic experience and a distinctive way of understanding the world. None of those values disappears merely because another intelligence becomes better at producing proofs.

The other question is whether human participation is necessary for mathematics itself to continue advancing. That is much harder to establish. If machines can eventually generate conjectures, prove them, compare alternative arguments, identify useful intermediate structures, connect results with previous literature, test generalisations and compress large bodies of results into simpler theories, then insisting that the final act of understanding must belong exclusively to humans begins to look less like a property of mathematics than a preference about who we want mathematics to be for.

That preference is legitimate and may be worth defending institutionally. It should simply be named accurately.

Chess remains worth playing even though computers play it better than humans. We value the human activity because thinking, competing and improving were part of what we wanted from chess in the first place. Mathematics may eventually develop a similar distinction between the frontier of what can be discovered and the frontier of what humans choose to understand for themselves. That would be a profound cultural change, but not necessarily a failure of mathematical progress.

When Proof Becomes Infrastructure

For most of mathematical history, difficult proofs have been scarce. Institutions, prestige and research practices grew around that scarcity. A mathematician who could solve a problem other mathematicians could not had produced something genuinely difficult to replace.

If AI changes the economics of proof, mathematics may reorganise around different scarce resources. Verification could become increasingly infrastructural. Proof generation might happen continuously in the background. More attention could move toward deciding which results deserve attention and finding representations that make enormous bodies of machine-generated mathematics intelligible.

There is no guarantee that such a transition would go well. Mathematical communities could be overwhelmed by low-value results. Attribution could become harder. Students could avoid precisely the work needed to develop judgement. Proprietary systems could generate mathematics faster than independent researchers can scrutinise it. A flood of technically correct results could make the literature less usable rather than more.

Those are reasons to build institutions and tools around the new abundance. They are not, by themselves, reasons to preserve scarcity.

The strongest achievement of the recent criticism from Tao and the other Fields Medallists is that it rejects the crude equation of more solved problems with more mathematical progress. They are right that mathematics ultimately needs ideas that can be explained, reused, connected and absorbed into what comes next.

Once that is accepted, however, a more uncomfortable question follows: why assume that the machinery capable of making proofs abundant must stop at the proof?

The future problem may not be how to stop machines from producing too much mathematics. It may be how to turn an abundance of proofs into a small number of ideas worth knowing—and whether we should assume, before the experiment has even begun, that only humans can do that.