OpenAI released mathematical results from an internal model alongside Lean formalizations, process details and plans for community workshops and programs.
OpenAI published a collection of mathematical results produced by an internal frontier model on October 6, 2026, and is making the material available through a GitHub repository. The release includes formalizations of many proofs in Lean, a language that lets mathematical proofs be checked by computer. OpenAI says it plans to add more formalizations as they are obtained.
The company also disclosed information about how the results were generated. The repository includes ten summaries of the model’s reasoning, estimates of the compute used expressed in equivalent ChatGPT Pro usage, and statistics on attempted problems. OpenAI says an average result used compute equivalent to roughly three hours of ChatGPT Pro thinking. The post does not present that estimate as a measure of the model’s total training or operating costs.
OpenAI said it consulted the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study while developing its approach to sharing results. For this release, the company is using GitHub and providing protocols for paper revisions and citations. It said it is also exploring other community-hosted options that would meet the advisory group’s guidelines.
The release is intended to make AI-produced mathematical work more open to scrutiny and follow-up. Lean formalizations can provide a computer-checkable representation of proofs, while the published process information offers context about attempts and compute behind the results. OpenAI also acknowledged that its papers need improvement in areas including citations, exposition and presentation, and said it intends to use community feedback to refine future disclosures.
The company said it will fund workshops, conferences and special programs focused on understanding major results produced by AI, with further details to come. It also said it is working toward a responsible release of the model behind the results; the announcement does not provide a release date or promise that the model is currently available.