FoxTPNL / Wikimedia Commons (CC BY 4.0)
OpenAI releases new mathematical results from internal frontier model
The release includes computer checked proofs and details on reasoning and compute usage.
OpenAI is releasing a broad range of new mathematical results produced by an internal frontier AI model, publishing papers and supporting materials in a public GitHub repository.
The release includes formalizations of many proofs in Lean, a programming language that allows computers to check mathematical proofs. OpenAI said it will add more formalizations as they become available.
The company is also publishing 10 summaries of the model’s reasoning, estimates of compute usage and statistics on the number of problems attempted. According to OpenAI, the average result required compute equivalent to roughly three hours of ChatGPT Pro thinking.
The disclosure follows consultation with the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study. OpenAI said the group’s advice and public recommendations informed how it is releasing the results.
AI, tech, and the markets they move—in one daily briefing.
Daily. Free. Join 34,000+ readers across crypto, finance, and policy.
The repository includes protocols for paper revisions and citations. OpenAI is also exploring alternatives hosted by the community that meet the advisory group’s guidelines. For future releases, it said it plans to improve citations, mathematical explanations and presentation.
OpenAI will fund workshops, conferences and special programs focused on understanding major mathematical results produced by AI. Further details will be announced later.
The company said it is working toward responsibly releasing the model behind the results, but did not provide a timeline. It plans to continue evaluating internal frontier models in mathematics and other sciences and to update its disclosure standards based on community feedback.