OpenAI publishes AI-generated math proofs, many machine-checkable in Lean

Key Points

1. OpenAI released new mathematical results from an internal frontier model in a public GitHub repository.
2. Many proofs are formalized in Lean, a language that lets computers verify mathematical arguments.
3. Machine-checkable output lets researchers audit AI math results instead of trusting model claims.

The latest:

A broad set of new mathematical results produced by an internal frontier AI model is now public, OpenAI said on October 6, 2026, posted to a new repository at github.com/openai/math. Many of the proofs are formalized in Lean, the proof-checking language, with the company saying further formalizations will be added as they become available.

Details:

• The release: OpenAI said the results came from an internal frontier model and were published in a dedicated GitHub repository rather than a journal or preprint server. The company said it is working to responsibly release the model that generated the results, without naming the model or setting a release date.
• Verification layer: Many of the proofs are formalized in Lean, a language that allows a computer to check a mathematical proof step by step. OpenAI said more formalizations will be added as they become available, indicating the initial release is not fully machine-verified across every result.
• Outside consultation: The company said it consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study and drew on the group’s public recommendations in preparing the release. OpenAI did not detail which specific recommendations shaped the repository’s contents.
• What is included: Beyond the proofs themselves, the repository carries summaries of the model’s reasoning, compute estimates, and statistics on the number of problems the model attempted — material that lets outside researchers see failure rates and cost, not only successful outputs.
• The compute figure: OpenAI expressed compute in an unusual unit: ChatGPT Pro usage. The average result consumed the equivalent of roughly 3 hours of ChatGPT Pro thinking time, a framing that measures the work in consumer-product terms rather than GPU hours or training cost.
• Funding commitment: OpenAI said it plans to fund workshops, conferences and special programs focused on understanding major AI-produced results. The company promised more details later and did not specify budgets, partner institutions, or a timeline for the first program.
• The attempt data: Publishing statistics on problems attempted alongside the results is a departure from typical model-capability announcements, which usually surface benchmark scores. The repository structure allows mathematicians to assess how often the model succeeded relative to how often it tried.

Background:

Lean is a proof assistant used by mathematicians to encode arguments in a form a computer can check exhaustively. A formalized proof either compiles or fails, removing reliance on human review alone — the central reason formalization is treated as a credibility test for AI-generated mathematics.

Between the lines:

The release’s design points at a trust problem rather than a capability one. Publishing Lean formalizations, attempt statistics and per-result compute lets reviewers check claims independently instead of taking a benchmark score on faith. The choice to consult an outside academic advisory group before publishing, and to fund programs on interpreting AI-produced results, suggests OpenAI expects the mathematical community’s acceptance to be the binding constraint on this work.

What’s next

Watch for the promised release of the model behind the results, the pace at which remaining proofs are formalized in Lean, and the first funded workshop or conference OpenAI names.