The field of mathematics is in turmoil, thanks to AI.
As the field advanced, one of the techniques mathematicians leveraged to be certain that a proof is correct is to have a machine check it. But it did not come for free. Hales and Ferguson announced the Kepler proof in 1998 but the machine-checked proof arrived in 2014. Hales, in a guest post on Terrence Tao’s blog, shared his estimate of the human effort that went it:
the formal proof of the Kepler conjecture on sphere packings in three dimensions took about 20 human work-years.
Early September, OpenAI announced what it called a solution to one of the seven Millennium Prize problems, the Navier-Stokes. It shared that the agents took about 88 hours to arrive at it. The verification that it was valid using Lean formalization took an additional 17 hours and an AI model, GPT-6 Astra, did it. Lean is a computer program and a language that allows mathematicians to verify and guarantee that a proof has no errors, akin to a spell-checker that can help a writer make sure there are no spelling errors.
And on October 6th, OpenAI shared 722 more manuscripts in a single release. On average, it reported that each result used three hours of ChatGPT Pro compute.
Doing got cheap, and now checking did too. What happens when both are cheap, and who pays for it?
What is already settled
Others have already made the case that what it means to be a correct proof has diverged from what it means to be understandable. In the words of De Toffoli and Duede,
We can end up with formal proofs that float free from any intelligible proof.
Sanderson captured the essence when he wrote
… every AI-generated proof is born an unsolved exposition problem.
Tao summed it up in a lecture at Caltech that we are entering a new era
we are now entering an era of proof abundance in mathematics.
In my earlier post on the topic, I wrote that the machine check does not remove trust from the picture but moves it. In this post, I want to address where it moved to.
The accounting
OpenAI has committed to preserve the public release history. There are 719 manuscripts across 372 families, resulting from approximately 4000 problems that were posed to the model. We have to be careful to not read this as a success rate. OpenAI has not shared how the problems were chosen or what happened to the rest but said selection was by “requiring an appropriate level of significance.” 300 of them, about 42%, have been shared with a machine check and OpenAI warns that “some of the unformalized results could have issues.” A spokesperson told Retraction Watch that “roughly 50% of the results were released unconfirmed.”
Some had issues. The log for October 7 records three papers withdrawn. One contained “a sign error” that “invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.” The company found it. “A spokesperson for OpenAI told us the company identified the errors during an audit,” Retraction Watch reported. The same day, fourteen more manuscripts were revised, with “proof repairs, corrected statements, clearer hypotheses and dependencies,” and thirteen more were updated to cite the revised versions. Thirty manuscripts changed in a day.
The gap between claimed and accepted is older than this release. MIT FutureTech tracks the 457 problems on Wikipedia’s list of unsolved problems as it stood in January 2024. By late September, 30 had been resolved, and “only 9 have been formally accepted; the rest are claimed but not yet verified.” The author adds that AI agents compiled the statuses, and that “the individual proofs have not been hand-reviewed by any expert mathematicians.”
What the cheap check bought
In the book I use mathematics as the cleanest case for letting machines attempt everything. Three conditions make that safe. You can say in advance what success is. You can detect failure promptly. You can reverse a failure before it spreads. In mathematics, I wrote, “verification is cheap and failure is free.” October tested each condition in the one field where they hold best.
Saying what success is
A theorem statement looks like the sharpest success criterion there is. In July I named two places the trust goes when a machine does the checking: you have to trust “that the formal statement fed to the checker is the statement anyone cared about, and that the checker itself is sound.” October showed a third.
First, the statement. OpenAI describes its Navier-Stokes result this way: “The fluid has a smooth force applied to it.” Two specialists in singularity formation, Diego Córdoba and Luis Martínez-Zoroa, note that the claim, if verified, would meet one of the alternatives in the prize statement, and that it differs from blow-up without forcing. Hales states the rule:
a proof in Lean should not be accepted until a human audit is performed to ensure statement fidelity.
He is fair to the other side. “This task is generally massively easier than checking the proof itself,” and the Navier-Stokes formalization “has already been confirmed by more than a dozen proof-checkers.” Easier per result still means a specialist per result. There are 300 of them.
Second, the translation. On the day of the release, Alexander Bastounis, Fabian Circelli and Anders Hansen posted a paper comparing OpenAI’s Lean proof of the Navier-Stokes result with its written proof. Their finding:
the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.
NL is natural language. In one estimate, the written proof needs four derivatives of a quantity and the Lean version assumes five, which makes the Lean statement weaker. The authors take no position on whether the written proof is correct. Their point is about the method. A model translates the paper into Lean and revises until Lean accepts. Lean then confirms that the Lean proof establishes the Lean statement. Whether either one matches the paper is a separate question, and Lean does not ask it.
Third, the checker. Hales reports that Lean’s kernel had soundness bugs this summer. “One Lean bug led to an illicit disproof of the Collatz conjecture.” He learned of another when “it produced a short illicit proof of the Kepler conjecture in Lean.” That is the theorem from my opening paragraph, proved falsely in a few lines. The bugs were repaired. His conclusion stands: “we absolutely cannot put blind trust in systems such as Lean.”
The three have something in common. Whatever makes the proof can keep adjusting until the check passes. Tao’s lecture asks the same question of a clinical trial:
Could the AI solution be somehow misaligned by exploiting a weakness in the trial process or its math models?
I think this adds a fourth condition to the three in the book. The check has to be independent of the maker. I take that up in this week’s newsletter, because it amends what I wrote in July about medicine.
Detecting failure promptly
Lean detects a broken proof at once, within the limits above, for the 42 percent it covers. That share had not moved a week later. Six formalizations were added on October 7, and the log has no later entry as I write.
For the rest, detection means a specialist reading a paper. The one failure we know of was caught by the producer’s own audit. Outside readers describe their capacity plainly. Asaf Karagila, a set theorist, called the release “the equivalent of a Denial of Service” and declined to read the paper in his own field. Bryna Kra, a former president of the American Mathematical Society, told the New York Times: “Peer review is gone in this process.” On the one result she most wanted to read: “The writing, however, makes it impossible to understand.” Scott Aaronson’s summary, the day after the release: “it also appears that no human has understood just about any of these proofs yet.”
We see only the errors that were found. The MIT post asks how many problems the models failed on. The same question applies to checking. I found no public count of how many of the 719 manuscripts a person has read.
Reversing a failure before it spreads
The README says: “Some outputs build upon earlier results produced by the models.” The sign error shows what that means. One mistake took three papers, because two had been built on the first before it was checked. I wrote about this shape in Nothing to Declare: outputs consumed by other systems without a contract, and nobody owning the pair.
A failed attempt costs tokens and spreads nothing. An unchecked success gets cited. This time the withdrawal worked, because a public log existed to record it.
Tao raised a harder case the same day. Some of this cannot be reversed at all. “A problem that has been ‘solved’ cannot be somehow reverted to become ‘unsolved’,” he wrote, and knowing a solution exists “contaminates” the search for other routes that might teach more.
The bill
That leaves understanding. Amit Sahai, a computer scientist, described the unit of work: research groups “each spending a term or a year trying to understand an extraordinary set of ideas produced by an AI system.”
Models will help write the explanations, and the MIT post expects the human edge there to be “short lived.” I grant that. Writing an explanation gets cheap. Absorbing one does not. Sahai again: “Depth of understanding needs time and a pace of life that humans can sustain.”
Tao describes what used to pay this bill. A breakthrough brought talks, workshops and newcomers, and through that activity proofs “become digested, streamlined, placed in context.” For machine results he reports the opposite: “Many fewer seminars, workshops, collaborations, or other activities are being generated from these results compared to traditional breakthroughs.” Solutions, he says, are being “harvested at large scale in an unsustainable fashion.” Kra says the same from the other side. “By releasing this trove of material in this manner, the companies are in the process of destroying the ecosystem that made it possible for this work.” A mathematician who uses the tools, she adds, “risks giving their ideas away.”
That is the vocabulary of a commons. I have used it for enterprises: “The deploying team enjoys the benefit and the enterprise absorbs the cost. That is the textbook definition of an externality.” The mathematicians advising OpenAI use the same word. Their guidelines warn of “substantial negative externalities that this practice inflicts on the mathematical community.”
Two ways of paying the bill are now apparent. The first is to release everything and let the field digest it. Aaronson calls the resulting work “thankless, barely-credited, competitive, and unfun.” The second is for the producer to pay experts to digest a result before release. Aaronson reports that Anthropic gave Virginia Williams and Josh Alman a model’s result to write up and announce, and compensated them. He names the cost of that route too. It “puts a private company in the position of picking and choosing which human mathematicians” speak for the machine.
The advisory group’s answer is that the producer pays and the community leads. Labs “must take responsibility for ensuring that human understanding will follow” and “should provide significant support, including funding,” while understanding “must remain organic and community led.” The group also asks for disclosure: “how many other problems of comparable difficulty the models tried and failed to solve, as well as how the problems were chosen.” OpenAI supplied part of this. The formalization status, the change log, the compute, the count of problems posed, and a promise to fund “workshops, conferences, and special programs” with no amount stated. The README is silent on failures and on selection.
The best case
Mathematics is as well equipped for machine output as any field. It has a proof checker, specialists, an advisory group, and a habit of labeling what has been checked. In this release it also had a public log. With all of that, here is the record so far. Under half of the output was machine-checked a day after release. A paper disputes what the September check certified. One error traveled through three papers. Funding for understanding is promised and unspecified.
Most companies have none of that machinery for what their agents produce. Meta’s numbers, which I wrote about last month, show where that leads: “Review load rises with the volume and not with value.” That post ended with three questions for a board. Here are four more.
- When a check passes, who confirmed that it checked the right thing?
- What share of the AI output shipped last quarter was checked by a machine, by a person, or by nobody?
- Does unchecked output feed other output, and could you withdraw it?
- Who pays to absorb it: the team that generated it, or everyone downstream?
Then ask for one artifact. OpenAI’s change log is public and dated, and it says what was withdrawn and why. Ask to see yours.
I ended the July post by saying that somebody “still has to be able to tell whether the answer is any good.” October showed what that sentence contains. Doing got cheap. Checking got cheap. Checking the check has not. And the title of this post leaves out a third job that has not either: absorbing the result.
Hales wrote of the review of his one proof: “A panel of twelve referees was assigned the review. Review dragged on for years, until the referees became exhausted and quit.” OpenAI’s catalogue lists 719 manuscripts.