The Pulse
OpenAI Publishes 722 Math Manuscripts From an Unreleased Model
OpenAI published 722 mathematical manuscripts on GitHub on October 6, saying an unreleased internal model produced the results. The collection includes some Lean proof formalizations, while the repository says not all manuscripts have them.
AI.info Team · Written with AI ·
“Making this work public is a first step. This release is the beginning, not the completion, of the process of human understanding and the incorporation of the work into mathematical knowledge.”
The Advisory Group on Mathematics and Artificial Intelligence
OpenAI published 722 mathematical manuscripts on GitHub on October 6, saying an unreleased internal model produced the results. The company organized the manuscripts into 372 families of related work and released some proof formalizations in Lean, a programming language that lets computers check mathematical proofs.
The release offers a large batch of AI-generated research for mathematicians to inspect, but OpenAI’s own repository stresses that the work is at different stages of verification. The repository says not all manuscripts have accompanying Lean formalizations, and the company warns that some unformalized results could contain problems. The model itself is not included in the release.
From about 4,000 problems to 722 manuscripts
OpenAI says it posed approximately 4,000 problems to the internal model during its evaluation. The resulting manuscripts span 372 families, each of which can contain a main result, related arguments, consequences or alternative proofs. The company says the average result used compute equivalent to roughly three hours of ChatGPT Pro thinking with the internal model.
That compute figure describes an average, not a uniform budget for every result. OpenAI identifies two exceptions to its general procedure: work on a zero-free region for the Riemann zeta function and a proof of the Hodge Conjecture for CM abelian varieties. It also says a write-up concerning the zeta function was edited by people for readability.
The repository includes 10 abridged summaries of the model’s reasoning, alongside information about attempted problems and compute estimates. OpenAI says it will preserve the release history and record revisions as new versions, leaving earlier versions accessible.
Lean formalizations cover only part of the collection
Lean artifacts can let readers check a formalized proof against a computer-verifiable system. OpenAI says many of the proofs have been formalized and promises to add more as they become available. The repository’s qualification matters: a manuscript without a formalization has not received that particular kind of check, and a formalization does not by itself tell readers how significant or understandable a result is.
The GitHub collection says its papers represent results at different verification stages and acknowledges that unformalized work may have issues. OpenAI says it will try to fix such issues quickly. The company has not named the model in the release or announced a date for making it available; it says it is working toward a responsible release.
Advisers say publication starts the human review
The independent Advisory Group on Mathematics and Artificial Intelligence, which OpenAI says it consulted, said the release should not be read as an endorsement of the results or the process that produced them. The group said only the mathematical community can assess the work and emphasized that publication begins, rather than finishes, the effort to understand and incorporate it into mathematics.
The group’s September recommendations called on AI companies to release significant mathematical results responsibly, provide details about how they were generated, formalize proofs where possible and support work that helps people understand them. Its October 6 statement said it had discussed those recommendations with OpenAI, but left it to mathematicians to judge how successfully the company followed them.
OpenAI says it will fund workshops, conferences and other programs focused on understanding major AI-produced results. It has not yet announced those programs’ details. For now, the collection’s 722 manuscripts are available for examination, with the company’s own repository warning that not all manuscripts have Lean formalizations and some unformalized results may be flawed.