On October 6, 2026, OpenAI announced a GitHub release of mathematical results generated by an internal frontier model. The company says the release includes supporting materials and Lean formalizations for many proofs. OpenAI’s announcement also puts average compute per result at roughly the equivalent of three hours of ChatGPT Pro thinking.
OpenAI’s internal model produced the results
OpenAI described the generator as an internal frontier model. ChatGPT Pro appears in the announcement as a reference for the compute estimate, not as the model that generated the mathematical work.
The repository materials include protocols for revisions and citations, ten summaries of the model’s reasoning, estimates of compute use, and statistics on attempted problems. Those details give readers and mathematicians more context about how the results were presented.
What Lean formalizations cover
OpenAI says it is sharing Lean formalizations for many proofs and plans to add more. Lean is a proof assistant: a system that lets a computer check the logic of a proof once it has been written in a formal structure. The formalizations therefore provide a way to check some of the proof work, while the announced scope is many proofs rather than every result.
A visual walkthrough uses mathematical diagrams and Lean code to show a creator-run proof-checking demonstration.
What the three-hour estimate measures
OpenAI’s figure is an average compute estimate per result, expressed as roughly three hours of ChatGPT Pro thinking. It is a compute-equivalence measure, with ChatGPT Pro serving as the reference; the results themselves came from the internal frontier model.
AGMAI’s recommendations for AI-generated mathematics
On September 29, 2026, the Advisory Group on Mathematics and Artificial Intelligence (AGMAI) published recommendations asking AI labs to stop testing advanced mathematical problems on proprietary models inaccessible to the research community. The group also called for disclosures such as a model’s name, prompts, summarized reasoning, time and estimated compute cost, along with information about formalization and how AI was used. It recommended community-led support to help people understand AI-generated mathematics.
OpenAI said it consulted AGMAI and used the group’s advice in shaping the release. In its October 6 announcement, the company also said it was working toward a responsible release of the model that produced the results and planned to fund workshops and related programs.
