← Back to feed

OpenAI on October 6 released a GitHub repository — openai/math — containing 722 mathematical manuscripts produced by an internal frontier model that has not yet shipped to customers. The results are organized into 372 related result families, with Lean formalizations attached to many of the proofs so they can be verified by a computer kernel.

The release is the latest step in an escalating sequence. OpenAI announced in September that an internal model had produced a claimed proof for the Navier-Stokes existence and smoothness problem — a result still under peer review, not yet certified by the Clay Mathematics Institute. A math advisory group was formed at the Institute for Advanced Study (IAS) to set AI disclosure standards. This release follows their recommendations.

Scale and Compute

• 722 manuscripts, organized into 372 result families
• ~4,000 problems evaluated to produce those results
• Average compute per result: roughly three hours of ChatGPT Pro thinking
• Lean formalizations for many but not all results
• 10 abridged summaries of the model’s reasoning made public
• Revision and citation protocols in place; prior versions remain accessible

The per-result compute figure is notable. Three hours of ChatGPT Pro usage is not cheap at scale, implying the model spent meaningful inference on each proof before committing it to a manuscript.

Independent Verification

Within hours of the release, community member @davegoldblatt independently re-checked one result: OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re, a proof that the Riemann zeta function ζ(s) has no zeros in the region Re(s) > 7/8. The check was run at commit adc7f12 of the public repo.

Both Lean FRO’s comparator and the independent nanoda kernel accepted the proof. #print axioms showed exactly the standard three: propext, Classical.choice, and Quot.sound. All 2,924 modules compiled with no errors. The recipe to reproduce the check is public on GitHub.

Zero-free region results for the Riemann zeta function have deep implications for the distribution of prime numbers. The Riemann Hypothesis itself would establish no zeros for Re(s) between 0 and 1 other than on the critical line Re(s) = 1/2; the verified manuscript establishes a fixed-width zero-free strip extending to Re(s) > 7/8.

What Comes Next

OpenAI stated it is “working to responsibly release the model” that produced these results and will fund a series of workshops, conferences, and special programs focused on understanding AI-generated mathematical advances. It is also exploring community-hosted alternatives to GitHub for future releases.

The IAS Advisory Group on Mathematics and Artificial Intelligence (agmai.org) provided guidance on the release format; their public recommendations from September 29 informed the citation protocols and Lean formalization requirements.

Why This Matters

Previous AI math milestones involved single results, often announced with limited verifiable artifacts. This release changes the format: 722 manuscripts at once, with formal proofs attached, in a repository structured for citation and revision. Whether the mathematical community adopts the repo as a legitimate publication venue is an open question. The verified Lean proof for the zeta function result suggests at least some of the work is machine-checkable at the level of existing formal mathematics standards.