OpenAI’s 719 AI-Generated Math Manuscripts Face Ongoing Verification
The collection includes 372 result families, while 300 top-line results have been formalized in Lean and the rest remain under review.

OpenAI has released 719 manuscripts generated by an unreleased internal frontier model, leaving mathematicians with a large body of work to examine for correctness and significance.
The collection is organized into 372 result families. A family can contain a main result, related arguments, consequences or alternative proofs, so the total does not represent 719 separate problems solved independently.
The repository initially listed 722 manuscripts after the Oct. 6 release. Three were withdrawn on Oct. 7 after a sign error was found in one argument and constructions used by two dependent papers were affected. Fourteen additional manuscripts were revised to repair proofs, correct statements, clarify hypotheses or change dependencies.
About 42% of the 719 top-line results, or 300 results, have been formalized in Lean. The programming language and proof assistant checks whether a formalized statement follows from a formalized proof. That process does not by itself show that the formal statement fully captures the broader claim in a manuscript.
The collection includes work produced after the model was asked approximately 4,000 problems. The average result used computing equivalent to roughly three hours of ChatGPT Pro thinking. The release also contains 10 shortened summaries of the model’s reasoning for selected results.
The repository warns that some results without formalizations may contain issues. The current collection therefore represents work at different stages of verification rather than a completed body of established mathematical research.
The Advisory Group on Mathematics and Artificial Intelligence, an independent group associated with the Institute for Advanced Study, called the release an important event but did not endorse OpenAI’s process or assess the impact of the work.
The collection is presented as a catalog of manuscripts and related result families. OpenAI plans to add more formalizations as they become available.
The release follows TokenPost’s earlier coverage of the initial 722-manuscript release, which described the company’s first public disclosure of the research.