OpenAI releases 722 AI-generated math manuscripts with Lean proof files

OpenAI has released 722 AI-generated mathematics manuscripts from an internal frontier model in a public repository, grouping them into 372 families and providing formal-proof artifacts for researchers to inspect part of the collection.

The release gives outside mathematicians more than finished papers to examine. The repository includes a Lean library, a machine-readable catalog that maps manuscript sources to named Lean declarations and files, and Comparator challenge configurations with public checking instructions. Lean is a proof assistant: its checker can verify that encoded proof steps follow from specified definitions and assumptions. That auditability is narrower than independent mathematical validation of the manuscripts.

OpenAI says the collection is at different stages of verification and that not every manuscript has a Lean formalization. The repository also cautions that some unformalized results could contain issues. The formalization catalog describes its scope as partial progress. The opened materials did not establish how many of the 722 manuscripts had corresponding Lean files.

The company also released 10 abridged reasoning summaries, compute estimates and statistics about attempted problems. OpenAI reports that each result used roughly three hours of ChatGPT Pro thinking compute on average and that about 4,000 problems were posed during the evaluation. It says the vast majority of results followed the same procedure, while identifying exceptions involving a Riemann-zeta zero-free region and a Hodge-conjecture result. One zeta-function manuscript was human-edited for readability, according to the repository.

For corrections, OpenAI says it will preserve the public release history, record revisions as new versions, keep earlier versions accessible and provide manuscript-level BibTeX citation blocks. It also says more Lean formalizations will be added as they become available. Those measures create a revision trail, but they do not establish manuscript-by-manuscript peer review, human comprehension or correctness.

The Advisory Group on Mathematics and Artificial Intelligence said its advisory role was not a judgment of the results’ impact or an endorsement of OpenAI’s process. The group said the mathematical community must assess the work and whether its recommendations were followed. That distinction between publication and independent validation of OpenAI mathematics work is central to assessing the new collection. The group’s responsible-release guidelines recommend timely deposit in a scholarly repository outside an AI lab’s control, persistent identifiers and a record of modifications. OpenAI says it is still exploring community-hosted alternatives.

OpenAI says it plans to add further formalizations and fund workshops, conferences and special programs focused on understanding major AI-produced results.