OpenAI releases machine-produced math results with Lean proofs and compute figures

OpenAI published “Sharing AI progress in mathematics” on 6 October 2026. The post describes a broad range of new mathematical results produced by an internal frontier model and released in a GitHub repository, with protocols for paper revisions and citations.

Many of the proofs are formalized in Lean, a language that lets a computer check a proof. OpenAI says it will add more formalizations as it obtains them.

The repository discloses how the results were obtained: ten summaries of the model’s reasoning, statistics on the number of problems attempted, and estimates of compute. The average result used the equivalent of roughly three hours of ChatGPT Pro thinking.

OpenAI says it consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study on how to release results of this kind.

The post does not say how many results are in the release or how many have been checked by mathematicians outside the company. The model is not public. OpenAI says it is working to release it responsibly and commits to better citations, exposition and presentation in future releases. It also says it will fund workshops and conferences on major results produced by AI.