OpenAI's internal model produces new mathematical results, shared with Lean proofs

Sharing AI Progress in Mathematics

OpenAI is releasing a broad range of new mathematical results generated by an internal frontier model. The average result used roughly three hours of ChatGPT Pro thinking. The company consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study to develop best practices. Results are published in a GitHub repository with protocols for revisions and citations, including Lean formalizations of many proofs, ten summaries of the model's reasoning, compute estimates, and problem attempt statistics. OpenAI will fund workshops and conferences on understanding AI-produced major results.