AGMAI withholds endorsement of OpenAI math release process

The Advisory Group on Mathematics and Artificial Intelligence withheld endorsement of OpenAI’s process for releasing hundreds of AI-generated mathematics manuscripts. Researchers are now left to assess both the results and whether the release followed the group’s recommendations.

That decision puts the collection’s verification status at the center of the dispute. OpenAI’s repository lists 719 manuscripts across 372 families and says the results are at different stages of verification. It also says not every result has been formalized in Lean and some unformalized results could contain issues.

When OpenAI announced the release on Oct. 6, it said an internal frontier model had produced a broad range of mathematical results. AGMAI described the collection as reporting solutions to hundreds of open questions. According to OpenAI, the model was given approximately 4,000 problems, and an average result used compute equivalent to roughly three hours of ChatGPT Pro thinking. The repository includes 10 abridged summaries of the model’s reasoning.

The standards dispute follows OpenAI’s initial publication of 722 AI-generated math manuscripts with partial Lean formalizations. An Oct. 7 repository history update recorded the withdrawal of three manuscripts after a sign error invalidated one argument and two constructions that depended on it. The update also recorded revisions to 14 other manuscripts and citation changes to 13 more.

OpenAI reported that 300 of the remaining 719 top-line results, about 42%, had Lean formalizations after six more were added. A Lean formalization expresses a proof in a form that the Lean theorem prover can mechanically check. The reported coverage does not extend to every manuscript in the collection.

The company said it published the materials on GitHub with protocols for revisions and citations, preserved previous versions, released some formalizations and process information, and was exploring repository options hosted by the mathematical community.

AGMAI’s responsible-release recommendations distinguish between papers fully understood by a responsible mathematician and output that people do not yet understand. For understood work, the group recommends established practices including preprints, journal peer review and explanatory talks.

For output that is not yet understood, AGMAI calls for literature and citation work, conventional exposition, disclosure of the model and production process, formalization where possible with its status clearly labeled, records of problem selection and failed attempts, and a repository outside an AI lab’s control with persistent identifiers and revision histories.

AGMAI said its advisory role should not be interpreted as an endorsement of OpenAI’s process or as a judgment about the results’ impact. It described public release as a first step toward human understanding and said the mathematical community must assess both the work and how closely the release followed its recommendations.