Notes
The Verification Bill for Mathematics
A month ago, I wrote that AI could produce real mathematics, but could also churn out mathematical texts that look complete and fall apart under scrutiny. Humans, meanwhile, would have to withstand a DDoS attack delivered at silicon bandwidth, in bodies made of carbon. That essay focused on changes in mathematical ability and how research gets done. I left another question largely unexplored: who should pay for verifying all this output?
On October 6, OpenAI released a collection of mathematical results produced by an internal model, along with Lean formalizations of some of the proofs. Such a release may bring important mathematical advances. It also puts a verification bill in front of the mathematical community. I don’t think frustration with this approach to research can simply be dismissed as mathematicians disliking AI or fearing for their jobs. There is a more direct question: Of the work you claim to have completed, how much is actually finished, and how much is waiting for someone else to finish it for you?
Who Finishes the Work
People who build software should recognize the feeling. In late 2025 and early 2026, a common complaint about AI coding was that code arrived at astonishing speed, while checking it, finding the mistakes, and doing it over still fell to the programmer. It looked plausible. Then you took responsibility for it and discovered that the time saved on writing had gone into understanding and repair. In the 2025 Stack Overflow survey, 66% of respondents to the relevant question had encountered AI output that was “almost right, but not quite.” In a Sonar survey released in January 2026, 38% of developers said reviewing AI code took more effort than reviewing code written by a colleague. “AI writes the code; humans clean up” isn’t a scenario invented to make a point about mathematics. Software has already paid that bill.
So programmers’ resistance at the time cannot all be written off as an unwillingness to accept better tools. Some of it addressed a specific problem: You demonstrate the speed of generation. I take responsibility for delivery. When a mistake is explained away as “the model still has room to improve,” but work that humans have reviewed and repaired is then presented as proof that “AI can already do the whole job independently,” the people finishing that work have every reason to object. You cannot call the generation step automation, leave the rest to someone else, and announce that the whole job has been automated.
Mathematics faces the same bill, only a harder one to settle. AI will make mistakes, and humans will take part in review. The trouble is that a producer can lower its own costs without lowering the cost of completing the work. If failure means “AI got it wrong” and success means “AI solved the problem,” the people who spent their time understanding, verifying, and even repairing crucial arguments can easily disappear from the story of the achievement. Verification hasn’t disappeared. It has merely been left off the bill for work supposedly completed “independently.”
There is another difference: how independently verification can be done. Suppose the software task is to improve performance. We can agree on the hardware, workload, and metrics in advance, run the same benchmarks repeatedly after the changes, and check for functional regressions. The person accepting the work needn’t reinvent the optimization or take the developer’s explanation of the code on trust. They can obtain evidence that, under these conditions, it really is faster and the behaviors checked haven’t regressed. That isn’t a guarantee covering every environment and every input, but it can already justify a controlled release. How developers find an answer and how reviewers judge the result can be quite separate processes.
A proof written in natural language at the research frontier is a less tidy affair. A reviewer can follow the argument without having to discover the route from scratch. But judging whether each step holds often still requires going deep into the same mathematics. Are the assumptions sufficient? Does that consequence really follow? Can the step waved away as “obvious” actually be filled in? Running a few more examples won’t settle those questions. If a crucial step is missing, the reviewer may have to supply that part of the proof themselves. Checking a proof is not the same as rediscovering it. But checking an unfinished research manuscript is also a long way from running tests on a finished product.
Software engineering also has some relatively forgiving ways to handle failure. For many everyday tasks, we can restrict where a program is used, retain human confirmation, degrade a faulty feature, or roll back when something goes wrong. A program needn’t first prove itself correct on every possible input before it can produce value in a controlled setting. Compared with the standard a mathematical proof must meet, that margin for error is positively luxurious. Mathematics can of course study approximation, probability, and error. But the error must be part of the proposition, not a debt quietly left unpaid by the proof. A defective program may still be useful. A proof missing a crucial argument isn’t complete just because most of its steps are right.
After Formalization
Formal tools offer an enormously important way forward. For fully encoded statements and proofs, systems such as Lean really can separate constructing a proof from checking it. The checker needn’t retrace the process of discovering the proof. So a blanket claim that mathematics has no independent verification would be wrong. But we still need to be clear about what passing that check establishes. Lean checks the statements and proofs entered into its formal system. It does not automatically ensure that they faithfully express what the paper originally claimed. The recent preprint Navier–Stokes lost in translation identifies substantive differences between OpenAI’s written Navier–Stokes proof and its accompanying Lean materials in the assumptions and conclusions of some estimates. That alone doesn’t refute the original mathematical result. It does show that “the formal proof passed” and “the original claim was verified” are separated by another layer of work that deserves careful scrutiny.
Nor can we currently count on AI to handle that entire layer reliably on its own. Proof search within a formal system can already use machine checking to obtain clear training feedback; work such as AlphaProof demonstrates the value of this approach. A manuscript at the research frontier presents another set of difficulties: understanding the original problem, making implicit assumptions explicit, checking the full chain of dependencies, and confirming that formalization hasn’t changed the meaning of the claim. Research updated as recently as this October still identifies reliable proof verification as a bottleneck in training and evaluating difficult mathematical reasoning.
That’s why I don’t think “a few more rounds of training and the next model will fix it” is a basis for calling today’s work finished. Researchers are training verifiers. But improvements on individual metrics don’t establish that the whole review process is reliable. If the judgments used to reward a model themselves come from an unreliable model, training may reinforce what looks like a correct proof rather than mathematical correctness. One study found that, on the models and datasets it tested, verifier training improved some metrics for judging proofs without significantly improving the verifier’s precision on final-answer tasks. The authors suggested that these gains might owe more to recognizing proof style and the form of an argument than to understanding its mathematical content. We can hope that verification catches up. We cannot use a capability that may exist tomorrow to sign off on verification left unfinished today.
Who Pays
The remaining work still demands precious effort from the mathematical community. This may involve far more than a quick read and a few corrected typos: sorting out definitions, tracking down references, reconstructing omitted arguments, or first working out what the authors meant to prove. The recommendations from the mathematics and AI advisory group AGMAI specifically address support for the work of understanding, organizing, and absorbing these results. The cost goes beyond hours worked. A researcher cleaning up someone else’s manuscript cannot spend those same hours advancing their own questions. We can add computing capacity. Expert judgment, research attention, and human lives don’t scale that way.
I can therefore understand mathematicians’ frustration with this model of research. A potentially important result doesn’t oblige anyone to stop their own work for it. Peer review is part of collaboration, but collaboration is not a standing agreement to take whatever work arrives. Independent scrutiny should not be an excuse for a lab to skip its own checks. When research output accelerates while verification remains stuck at human speed, what gets crowded out is the community’s capacity to keep doing research. You cannot count everything the machines have produced and ignore all the people who had to stop what they were doing to get that work across the finish line.
That cost belongs in the research budget, not in optional after-sales service once the publicity is over. AGMAI calls on labs to support the subsequent work of human understanding, including financially. OpenAI has also said it will fund workshops, conferences, and targeted programs around AI-generated mathematics. These commitments deserve credit. Funding, however, doesn’t buy the mathematical community’s attention, let alone purchase its approval in advance. Substantial contributions to understanding, verification, and repair should be recorded as contributions. Nor should a lab omit its own screening, organization, and checks because “someone will look at it later.”
Admission and Immunity
Understanding these objections doesn’t make every demand attached to them valid. The same AGMAI recommendations also call on labs to stop testing advanced mathematics problems on proprietary models that have not been made available to the wider scientific community. That is not a blanket rejection of AI doing mathematics. It does, however, move from how research should be released responsibly to the conditions under which research should be conducted. There are reasons to demand fairer access to tools. Demanding that a category of exploration stop requires a separate argument. A heavy verification burden alone doesn’t get you there.
Likewise, “I reject the way you are promoting this result” and “I reject AI as a participant in mathematical research” are different positions. The first can address evidence, responsibility, and research practices. The second begins drawing boundaries around the identity of the participant. Mathematical problems are no community’s private property. Exploring the unknown shouldn’t require a particular group’s permission. Other people, in turn, are entitled to decide where their limited energies go. The right to do research is not the right to commandeer someone else’s time. The right to refuse a review is not the right to deny someone else a place in research.
There is no need to swing to the other extreme and demand that AI verify everything with absolute certainty before anything can be made public. Conjectures, partial results, and failed approaches can all have research value. What matters is being clear about what is being delivered. A candidate result that identifies its gaps and invites others to help move it forward is a different offering from an announced “breakthrough” waiting for someone else to supply the crucial arguments. One seeks collaborators. The other may be packaging unfinished work as a completed achievement.
I don’t think this checkpoint must forever be staffed by humans, either. Using AI to search for counterexamples, check dependencies, examine the correspondence between a paper and its formalization, or overturn an earlier model’s judgments with a stronger one are all directions worth pursuing. The question is not which steps must be reserved for carbon. It is whether, before those capabilities are reliable, we erase from the accounts the work humans are already doing. AI can take on a growing share of research. “AI did it” should not become a release from responsibility for the people publishing it.
Just Go Create?
On October 8, LeCun responded on X to the lament that “a part of mathematics is dead” with a different vision: as formal proof becomes largely automated, mathematics will shift toward new concepts, abstractions, definitions, and conjectures. His analogy was the boat: it made swimming less important, but enabled the discovery of new lands.
This discussion has been around for some time. In an essay published in March, Commelin and his coauthors considered how, if machines could carry out well-defined tasks at scale, mathematical expertise might shift toward choosing tasks, connecting them to larger questions, and exercising judgment and insight. In his October 5 guest post on Tao’s blog, The Future of Mathematics, Jeremy Avigad also discussed creating new concepts and frameworks. He acknowledged that such advice offered little comfort to young researchers facing upheaval, and that it did not make the difficulties easy to resolve.
These are worthwhile directions. But what I called Lv4—creating worlds—in the previous essay isn’t a task you can hand out with “just go create.” Anyone can say the words. An abstract framework that opens up vast new sets of questions for others to keep working on is extraordinarily rare.
When you’re creating such a world, even the direction may be unclear. What objects should you introduce? Which distinctions are worth preserving? How do you tell whether a definition has opened up a problem or merely given it new wording? There may be no ready answers. You might spend a long time before realizing you’ve been going in circles. AI can help with derivation, search, and trial and error. Making those operations faster doesn’t automatically provide a worthwhile direction or a yardstick for judging it. Calculation, proof, and years of hitting walls are not low-grade labor you can casually discard on the way to creation. Many new concepts and judgments grow out of precisely that work.
Now software has Wish Coding. Say what you wish for, and a product grows out of it. Sounds even easier than Vibe Coding. Yet at least in the demonstrations I’ve seen, most of it is still combination and imitation: fitting existing features together, giving an existing product a new look, smoothing out a familiar workflow. These things can be very useful, and new creations can grow out of combinations. But making implementation cheaper doesn’t automatically make creation easier. Someone who didn’t know what to create may still have no answer, however fast the generator runs.
What I have no patience for is compressing these discussions of future directions into “just go create,” then using that line to belittle people working on specific research problems. If you haven’t managed that kind of creation yourself, what gives you the right to look down on others? And even if you have, what gives you that right? The four kinds of ability in the previous essay were never ranked by worth. You don’t get to turn one of them into a license to ridicule everyone else. If a result needs these people’s understanding, verification, and repairs before it can stand, there is even less reason to talk as if their work were worthless.
In the previous essay, I looked forward to humanity taking AI along to batter at walls we couldn’t break through before. I still do. I don’t want the mathematical community to turn reasonable demands for scrutiny into grounds for excluding new participants. Nor do I want AI companies to treat the speed of generation as the speed of completion, then leave others to pay for the missing stretch of work. Progress worth looking forward to includes more than the number of manuscripts delivered in a day. It includes how many errors can be worked through before delivery, so that those who follow can more easily understand the work, test it, and build on it.
Mathematics has no admission ticket reserved for carbon. It should have no liability waiver reserved for silicon.