Sharing AI progress in mathematics

OpenAI is releasing a broad range of new mathematical results produced by an internal frontier model. In collaboration with the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, OpenAI has developed best practices for sharing these results. The release includes a GitHub repository with protocols for paper revisions and citations, along with formalizations of many proofs in Lean, a programming language for computer-checked mathematical proofs. Additional details about the model's reasoning, compute usage, and problem statistics are provided. The average result used compute equivalent to roughly three hours of ChatGPT Pro thinking. OpenAI plans to fund workshops and conferences to understand major AI-produced results and is working to responsibly release the model that produced them.

(Source：OpenAI)