Sharing AI progress in mathematics
Points and comments are a snapshot, not live.
OpenAI publishes new mathematical results from an internal frontier model.
OpenAI released mathematical results produced by an internal frontier model in a GitHub repository, including formalizations in the Lean proof assistant. The release follows consultation with the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study. The repository includes 10 reasoning trace summaries, compute estimates (average equivalent of three hours of ChatGPT Pro thinking), and problem attempt statistics. OpenAI is funding workshops and conferences on AI-produced mathematical results.
What commenters are saying
Commenters are split: some criticize OpenAI for not fully meeting the mathematical community's recommendations, while others approve of the more measured approach after previous controversies over citation and plagiarism. Several note the lack of full reasoning traces, only summaries. One commenter highlights results on Riemann, Hodge, and the Unique Games Theorem, estimating 50-100 years of human math progress. Others argue that incomprehensible proofs are not progress until humans can understand them.