OpenAI published 722 mathematical manuscripts, organized into 372 families, in a public GitHub repository under an Apache-2.0 license on October 6. The company says they were produced by an unreleased internal frontier model given roughly 4,000 open problems; each result consumed compute equivalent to about three hours of ChatGPT Pro thinking.

Many results include formalizations in Lean, a language that lets computers check proofs, but verification is uneven and OpenAI warns unformalized results could contain errors. The release follows the September 29 recommendations of the Advisory Group on Mathematics and AI at the Institute for Advanced Study, which asked labs to stop testing advanced math in secret.

Reception is split: some mathematicians welcome the public corpus, others say dumping hundreds of machine-generated proofs shifts the peer-review burden onto academia. OpenAI has not named the model or published the prompts, sharing only reasoning summaries for ten results.

Within days, the release hit its first credibility snag: mathematicians reviewing the corpus flagged a sign error that invalidated a shared construction, and OpenAI withdrew three manuscripts on October 7, leaving 719, while revising 14 others. Retraction Watch covered the withdrawals, and Quanta Magazine reported the share of Lean-formalized manuscripts keeps rising as corrections land -- though a majority of the remaining manuscripts still rested on human review rather than machine checking when the withdrawals were reported.