OpenAI's 722-manuscript math release reopens the fight over unverified AI proofs

OpenAI on October 7 published 722 mathematical manuscripts spanning 372 open problem families to a public GitHub repository, attributing the work to an unnamed internal frontier model and reigniting a dispute over how AI labs disclose results the research community has not yet had time to check.

The scale of the release is the story as much as any single result. OpenAI says the model was posed roughly 4,000 open problems, with the average published result costing about three hours of ChatGPT Pro Thinking-equivalent compute. According to a detailed account from The Decoder, nearly every result came from a single prompt to a single agent, with some requiring multiple attempts. Many, but not all, of the manuscripts include Lean formalizations that allow a proof checker to verify logical validity; unformalized results carry an explicit caveat from OpenAI that some may contain errors.

What the model actually produced

The repository's ten published reasoning summaries cover a mix of narrow and significant claims: progress on multiplicative-function correlations, the irrationality exponent of pi, the symmetric and general Mahler conjectures, NP-hardness results at the basic semidefinite threshold, quasipolynomial bounds for arithmetic progressions, Kaplansky's direct-finiteness conjecture in characteristic two, the Mezard-Parisi formula for diluted spin glasses, spontaneous magnetization in the quantum Heisenberg ferromagnet, the isomorphism of free group factors, and the 3D relativistic Vlasov-Maxwell system. Two results stand out for their proximity to marquee open problems: a zero-free region for the Riemann zeta function restricted to Re(s) greater than 11/12, and a proof of the Hodge Conjecture for CM abelian varieties. OpenAI has not claimed the Riemann Hypothesis itself, and the repository frames both as incremental advances rather than full resolutions of century-old problems.

The release builds directly on a more contested claim from a month earlier. On September 8, OpenAI said the same model line had produced a Lean-formalized proof that smooth three-dimensional Navier-Stokes flow can develop a finite-time singularity, using a swarm of roughly 10,000 agents and, per OpenAI's own account, millions of dollars of compute. The company said it would not pursue the Clay Mathematics Institute's $1 million prize for the underlying Millennium Problem, and whether the institute accepts the proof remains unresolved.

A credit dispute becomes a field-wide revolt

The Navier-Stokes announcement triggered a backlash that has shaped every OpenAI math release since. NYU's Tristan Buckmaster said OpenAI offered him authorship terms on related work that excluded Levent Alpoge, an Anthropic mathematician pursuing the same proof route; OpenAI's Sebastien Bubeck denied trying to cut Alpoge from credit, but the dispute became the flashpoint for wider objections about speed and attribution.

On September 11, twenty-five Fields Medal winners, including Terence Tao and Peter Scholze, published a declaration titled 'A Severe Misalignment of AI in Mathematics,' arguing that AI labs' use of famous open problems as capability benchmarks works against the field's actual goal of building conceptual understanding that other mathematicians can learn from and extend.

Solving problems is a tool and proxy for the field's real aim, and rushed announcements leave too little time for writeups and citation, raising severe attribution and plagiarism questions, the Fields Medalists wrote in their declaration.

A separate, broader letter signed by 771 mathematicians targeted a specific event: Caltech's student-run Mathathon, where 100 teams each receive roughly $20,000 in AI credits and 40 hours to attack an open problem, with top entries advancing to a six-month round requiring an arXiv preprint and an auto-formalized solution. The letter labeled this approach 'slop mathematics,' arguing that it produces results quickly and leaves other researchers to verify, correct, and credit them without pay. OpenAI withdrew its $1 million sponsorship on September 10; Anthropic kept its own $1 million commitment, and the event is proceeding as planned for October 30 through November 1.

We don't have the luxury of waiting around to find out, said Caiman Moreno-Earle, the Caltech sophomore who founded the Mathathon, defending the event's pace against critics.

OpenAI's compliance is partial

In response to the controversy, the Institute for Advanced Study's Advisory Group on Mathematics and Artificial Intelligence published responsible-release recommendations on September 29 after soliciting more than 600 responses from the field. The group's guidance includes depositing results in repositories no single lab controls, disclosing model names, exact prompts, reasoning summaries, time spent, and cost per problem, formalizing proofs wherever possible, and publishing records of failed attempts rather than only successes.

OpenAI's October 7 release follows some of that guidance and departs from the rest. The GitHub repository includes revision logs and citation protocols, and the company says it consulted the advisory group directly. But OpenAI did not publish any prompts, gave only an average compute cost across all results rather than a per-problem figure, left the originating model unnamed, and kept the repository on its own infrastructure rather than moving to a lab-independent host, saying it is still 'exploring other community-hosted options.'

We recognize that the rapid progress of AI in mathematics is disruptive, OpenAI research lead Dan Roberts said, adding that the company wants to work with the mathematics community on how to integrate the technology.

OpenAI's own announcement frames the release as a step toward wanting this progress 'to push the frontier of human knowledge' and, eventually, to 'directly empower scientists with state-of-the-art capabilities' through a responsible release of the underlying model, though no timeline or name has been given.

Why practitioners should care

For AI researchers, the more durable signal in this episode is not the raw count of solved problems but the widening gap between what formal verification can confirm and what the research community is willing to accept. Lean and similar proof assistants can check that a derivation is logically valid; they cannot judge whether a result is original, relevant, or worth the field's attention, and OpenAI's own repository acknowledges that unformalized submissions may still contain errors. With roughly 4,000 problems posed to generate 722 publishable results, the attempt-to-success ratio implies a high rate of silent failures that are not being surfaced for the same scrutiny as the wins. As frontier labs push mathematics as a visible proving ground for autonomous research capability, the unresolved question is whether formal correctness alone is sufficient grounds for a claim to stand, or whether community vetting at human speed remains a precondition the industry has not yet priced in.