On October 6, the mathematics community received an unsolicited delivery: OpenAI published 722 mathematical preprints at once, on its own site and GitHub, covering 372 previously unresolved results—some accompanied by formalized versions machine-verified with the Lean proof assistant. All in one day. The New York Times later described mathematicians' mood in two phrases: awestruck and staggered. Science put it more coolly, and more accurately—OpenAI has permanently changed mathematics; how, nobody yet knows.
Three weeks on, the second act is more interesting than the first. The first act was shock; the second is the math community collectively answering a question: machine-written proofs now exist—how do humans plan to accept them?
Production is automated; acceptance is not
First, the accounting. The 722 manuscripts correspond to 372 distinct results, produced by an internal frontier model. The officially disclosed average cost: roughly 3 hours of ChatGPT Pro thinking-mode compute per result. A professional mathematician typically spends years on a single open problem. The ratio between those two timelines is the entire impact of this release.
But production speed was never mathematics' bottleneck—verification is. For a proof to become accepted knowledge, other mathematicians must read it, check it, hunt for counterexamples, and eventually someone must be willing to put it in a textbook. At the human pace, that's months to years per paper. 722 papers arriving together would overwhelm every mathematician on earth, even working in parallel.
The community had a contingency plan ready, and its name is Lean. Once a proof is translated into this formal language, correctness can be adjudicated by a compiler—machines deliver a verdict in seconds, independent of anyone's reputation. That is why the subset of the 722 papers with Lean formalizations drew the most attention—around 300, per third-party tallies. The majority have only one realistic near-term path: human reading.
Three retractions and one crack
The retractions came fast. Around October 8, OpenAI pulled three preprints. The chain: one proof contained a symbolic error; two others depended on it—one error, two casualties. The Hacker News discussion thread was bluntly titled "OpenAI retracts three mathematical results."
What's worth remembering is where the crack sits. New Scientist flagged the detail: the problem arose in translating mathematics into Lean code—the correctness of the mathematics and the correctness of the translation are two different things. If the translation layer errs, even the strictest machine verification will flawlessly verify something wrong. It echoes an old software maxim: tests passing doesn't mean the requirements were right.
Ten days of events clarify what this release really was: less a victory declaration of "AI solved 372 problems" than an imperfect public beta. OpenAI's own actions confirm the framing. An October 15 update announced a $5 million donation to a new Simons Foundation initiative funding mathematicians to verify AI results, plus model and compute access for grantees. The producer of AI is paying for acceptance too—an admission that without verification, production is worthless. There was institutional scaffolding as well: an advisory group with the Institute for Advanced Study helped shape the release protocol, and the company committed to responsibly releasing the model that produced the results.
Verification is the new scarcity
In the bigger picture, this event marks a change in the division of labor. Of a mathematician's two traditional legs—devising proofs and checking proofs—machines have now taken over one. The cost of producing candidate proofs is collapsing, from person-years to machine-hours. Lean can absorb part of verification, but the hardest part still needs humans: judging whether a result is worth verifying, translating physical intuition into formal language, and catching misalignment when the translation layer errs.
Three weeks in, the vast majority of the 372 results remain unverified by humans; the true quality of the 719 survivors will become clear over months or even years. Only one thing is settled: on the assembly line of mathematical knowledge, the most expensive step has changed hands.
Sources and caveats: Release scale (722 papers, 372 results), compute figures (~3 hours ChatGPT Pro thinking per result), the Simons donation, and the IAS advisory group and model-release commitments come from OpenAI's official blog post *Sharing AI Progress in Mathematics* (Oct 6, updated Oct 15). Retraction details come from a Hacker News thread (Oct 8) and media reports; the translation-layer issue is based on New Scientist's headline and summary. The ~300 Lean formalizations figure is a third-party tally, not verified paper-by-paper. NYT and Science headlines are paraphrased. Tao's statement is confirmed only as to existence and date; its full text was not reviewed.