722 AI-generated math manuscripts, with proofs to examine

A collection of 722 mathematical manuscripts from an internal OpenAI model is public, with formal proofs available and varying levels of verification.

Hundreds of mathematical papers produced by a model that remains unavailable to the public can now be accessed through OpenAI’s research repository. The collection contains 722 manuscripts organized into 372 families, each potentially bringing together a main result, supporting arguments, consequences, or alternative proofs. That count therefore does not represent an equal number of distinct problems solved. According to the company, the research extends its standard evaluations, which had become insufficient to measure its models’ mathematical capabilities.

Verification varies across the collection. Some papers include proofs formalized in Lean, a language in which mathematical arguments can be written for computer checking. Others have no accompanying formalization, and the company acknowledges that some of those results could contain errors. The repository is expected to gain additional formal proofs and retain earlier manuscript versions when corrections are made.

Approximately 4,000 problems were posed to the model during the evaluation. Outputs were then selected for significance and grouped into the published collection. Each result used an average amount of computation equivalent to roughly three hours of ChatGPT Pro thinking, an estimate of the resources consumed by this internal model. To document the process, ten reasoning summaries are available, covering subjects including the irrationality exponent of π and the Mahler conjectures. There were exceptions to the standard procedure; one manuscript on the Riemann zeta function was also edited by a human for readability.

According to the company, the release draws on recommendations from the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study. Its public guidance calls for understandable papers, accurate citations, and financial support for studying the results. It also explicitly asks labs to stop testing advanced mathematical problems on proprietary models that the scientific community cannot access. The company plans to fund workshops, conferences, and programs dedicated to understanding these results. Its research post also says it is working toward releasing the model involved, without specifying a timeline.