OpenAI Released 722 AI-Written Maths Manuscripts. Verification Is Now the Story

What happened

OpenAI has released a collection of 722 mathematical manuscripts generated by an unreleased internal model. The papers are organized into 372 families spanning multiple mathematical disciplines, with some families containing a principal result, companion arguments, consequences or alternative proofs.

The company announcement dated 6 October describes the release as a broad range of new mathematical results. The manuscripts, source files, proof artifacts and selected reasoning summaries are available in a public GitHub repository.

The release details and verification status described below come from OpenAI's public materials and the independent advisory group's public statement. Haivian has not independently checked the 722 manuscripts or their proof artifacts.

OpenAI says the model was presented with approximately 4,000 problems. After grouping related outputs and applying a significance threshold, the company produced the current catalogue. It estimates that an average result used compute equivalent to roughly three hours of ChatGPT Pro thinking.

The scale is the headline. A single release now asks mathematicians to evaluate hundreds of proposed results distributed across fields in which expertise is highly specialised. But the manuscripts do not become established mathematics merely because they are numerous, public or written in theorem-proof form.

The verification burden is now part of the scientific event.

What the evidence shows

The repository provides more than a press release. Readers can inspect individual manuscripts, an overview of result families, source material, revision instructions and a catalogue of formal proofs. OpenAI has also published ten abridged reasoning summaries for selected results.

Many of the manuscripts have associated Lean formalizations. Lean is a proof assistant: when a theorem and its dependencies are represented correctly, a checked proof can offer strong assurance that the formal steps follow. Formalization is valuable evidence, but it does not automatically settle whether the formal theorem precisely matches the informal headline, whether assumptions capture the intended problem, or whether the result is novel and significant.

OpenAI says the overwhelming majority of results came from a common procedure using the same unreleased model. It identifies exceptions, including work related to a zero-free region for the Riemann zeta function and the Hodge conjecture for CM abelian varieties. The repository also says the company will preserve release history and record corrections as new versions.

These are useful transparency measures. They make the work inspectable and create a path for errors to be found and revisions tracked.

What remains uncertain

The repository carries its own essential warning: the collection contains results at different stages of verification, not all have formalizations, and “some of the unformalized results could have issues.” That caveat should accompany any report about the release.

Neither OpenAI's announcement nor its repository presents the 722 manuscripts as independently certified in full. Even where a formal proof exists, specialists still need to check the statement being formalized, the imported assumptions, the relationship to prior literature and the significance claimed for the result. Where no formalization exists, conventional line-by-line mathematical review remains necessary.

The model itself has not been released, so outside researchers cannot independently reproduce the generation process. OpenAI provides selected reasoning summaries and aggregate compute information, but not a complete reproducible record for every manuscript.

There is also a structural question: who performs the review? Haivian's analysis is that hundreds of manuscripts could impose a substantial unpaid workload on a mathematical community that did not choose the problems, control the release schedule or share equal access to the system that produced them.

The independent Advisory Group on Mathematics and Artificial Intelligence calls the release an important event, but stresses that its advisory role is not an endorsement of either the results or the process. Its 6 October statement says public release is “the beginning, not the completion” of human understanding and incorporation into mathematical knowledge. It also argues that mathematicians must remain able to formulate their own questions and pursue directions not selected as demonstrations of an AI system's capabilities.

Why independent scrutiny matters

The old bottleneck in mathematics was often discovery: finding a conjecture, proof strategy or missing connection. This release suggests a world in which candidate results can be generated at enormous speed. In that world, review, interpretation, prioritization and correction become scarce resources.

Verification needs layers. A first pass can confirm that files build, references resolve and formal artifacts correspond to named results. A mathematical audit can reconstruct the dependency chain, identify hidden assumptions and test fragile lemmas. Subject specialists can assess novelty against the literature. The wider community can then decide which results are important enough to absorb, teach and extend.

Those stages answer different questions. Machine checking can establish formal consistency within a specified system. It cannot by itself establish historical novelty, explanatory value or the social legitimacy of directing a field's attention toward hundreds of machine-selected problems.

The responsible headline is therefore not that OpenAI has independently proven 722 breakthroughs. OpenAI has released 722 manuscripts containing mathematical results that it attributes to an internal frontier model, with verification status varying across the collection. Their eventual place in mathematics will depend on examination outside the system that generated them.

Haivian provides bounded independent audits for mathematical and scientific claims that need a clear verification record. With a collection this large, the first useful product may not be one verdict, but a transparent triage: what is formalized, what is reproducible, what is novel, what remains unverified and where expert attention is most valuable.