OpenAI releases AI-generated math proofs

OpenAI has released 722 manuscripts from an unreleased frontier AI model, spanning 372 families of mathematical results. The collection includes claimed solutions to major open problems such as the Navier-Stokes equations and progress on the Birch-Swinnerton-Dyer conjecture, with materials published on GitHub alongside summaries of the model’s reasoning.

Many of the proofs have been formalized in Lean, allowing them to be checked by computer. The release also includes compute estimates, problem statistics, revision guidance and citation protocols designed to support academic review and make the work easier for researchers to validate and extend.

OpenAI consulted the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study while shaping the release. The company plans to fund workshops and conferences to help mathematicians engage with the results, while keeping the frontier model itself unavailable to the public.

The effort raises practical and ethical questions around verification, exposition, attribution and the balance between openness and safety. If validated, the manuscripts could influence how mathematical research is produced, reviewed and shared.