OpenAI releases 719 math manuscripts from an internal model, with Lean proofs for 42 percent

On October 6, 2026, OpenAI published “Sharing AI progress in mathematics” and opened a public GitHub repository, openai/math, holding mathematical manuscripts produced by an unreleased internal frontier model. The repository README says the catalogue contains 719 manuscripts organized into 372 families, each family grouping a principal result with companion arguments, consequences or alternative proofs.

According to the README, the model was posed about 4,000 problems as part of evaluating it on open research problems, an effort OpenAI expanded after its existing math evaluations saturated. On average each result used the equivalent of about three hours of ChatGPT Pro thinking. Roughly 42 percent of top-line results (300 of 719) have Lean formalizations that a computer can check. OpenAI also released ten abridged reasoning summaries, covering topics such as the irrationality exponent of pi, the Mahler conjectures, Kaplansky’s direct-finiteness conjecture in characteristic two and the isomorphism of free group factors. OpenAI said it consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study on how to release the work, and on October 15 added a $5 million contribution to a new Simons Foundation program to help mathematicians examine and build on AI-produced results.

The repository’s own history shows the risk. On October 7 OpenAI withdrew three manuscripts, including one on the Hodge conjecture for products of K3 surfaces, because a sign error invalidated an argument they shared, and revised 14 others with proof repairs and corrected statements.

Why it matters: this is a release of AI mathematics at a volume no human group produces, published with versioning, retractions and machine-checked proofs rather than as a handful of headline claims. It moves the question from whether models can do research mathematics to how the community verifies and absorbs it.

What it does not show: most results are not formally verified and the README warns unformalized ones “could have issues”. Significance was judged by OpenAI, the producing model is unreleased, and a few results (the Riemann zeta zero-free region and a Hodge conjecture case) were exceptions to the standard procedure, one with human-edited writeup.