OpenAI releases 722 mathematics manuscripts from an unreleased frontier model

The Apache-2.0 corpus includes papers, reasoning summaries and partial Lean formalizations, but the underlying model remains private and many results still need independent review.

2 min read

A blackboard filled with mathematical formulas and symbols, illustrating AI-assisted mathematical research.

OpenAI released a large collection of mathematical manuscripts and proof artifacts on October 6, produced by an unreleased internal frontier model. The public repository contains 722 manuscripts grouped into 372 result families across multiple mathematical disciplines.

The release is evidence about a model-development evaluation, not a new model launch. OpenAI has not published the model’s name, weights, API access, pricing, architecture or license, and says it is still working toward a responsible release. The company reports that it posed roughly 4,000 open research problems to the model. Each retained result used, on average, compute equivalent to about three hours of ChatGPT Pro thinking.

For reproducibility and review, the repository includes manuscript PDFs and source files, a catalogue of result families, ten abridged reasoning summaries and a growing Lean library. Lean can mechanically check formalized proofs against stated definitions and assumptions. However, OpenAI says many—but not all—manuscripts have formalizations, and explicitly warns that some unformalized results may contain errors. The collection therefore should not be read as 722 independently validated mathematical discoveries.

The project is published under Apache 2.0 and preserves revision history, but the underlying model remains proprietary and unavailable. OpenAI says it consulted the Institute for Advanced Study’s independent Advisory Group on Mathematics and Artificial Intelligence. That group’s public recommendations call for prompt release, careful citation and exposition, community-led review, and sustained support for human understanding; it also objects to testing advanced mathematics on inaccessible proprietary models.

The practical significance is the scale and auditability of the release rather than a single benchmark score. Researchers can inspect, formalize, challenge and revise the artifacts, while important questions remain about novelty, correctness and how performance would generalize beyond OpenAI’s selected problems.

A blackboard filled with mathematical formulas and symbols, illustrating AI-assisted mathematical research.

Sources: OpenAI announcement · OpenAI mathematics repository · AGMathAI responsible-release recommendations · Unsplash image license

mathematicsfrontier modelsOpenAIformal verification