What happened?
On October 6, 2026, OpenAI released a broad range of new mathematical results produced by an internal model it has not released OpenAI post ↗. The repository first listed 722 manuscripts in 372 result families; after three withdrawals it now lists 719 GitHub repository ↗ History log ↗. A family groups a main result with companion papers, consequences or alternative proofs GitHub repository ↗.
The results cover many areas, from number theory to quantum physics. Two examples are a claimed zero free region for the Riemann zeta function, sometimes called the quasi Riemann result, and a claimed area law for two dimensional quantum systems Catalogue ↗. These are claims in the collection, not results confirmed by the wider mathematical community.
OpenAI says it consulted an independent Advisory Group on Mathematics and Artificial Intelligence hosted at the Institute for Advanced Study on how to release the work OpenAI post ↗. That group said its role is not an endorsement of how the results were obtained and that only the mathematical community can assess them AGMAI statement ↗. One day after release, OpenAI withdrew three manuscripts because a sign error broke a key argument, and revised 14 others History log ↗.
What is in the collection?
The manuscripts
Written papers with proofs, grouped into 372 families by topic GitHub repository ↗. Corrections are recorded as new versions, and older versions stay available GitHub repository ↗.
The Lean proofs
Lean is a programming language in which a computer can check every step of a proof. About 42 percent of top line results, 300 of 719, have Lean formalisations History log ↗.
The reasoning summaries
Shortened summaries of the model's reasoning for 10 families GitHub repository ↗. OpenAI also gave compute estimates and statistics on how many problems were attempted OpenAI post ↗.
The scale is new: one release asks mathematicians to check more claimed results than a typical research group could read in years. The interesting test now is how many survive.
Leapscope interpretation of the reported result.How did AI help?
OpenAI says the vast majority of results came from one fixed procedure using the unreleased model, which was posed about 4,000 problems over the evaluation GitHub repository ↗. The outputs were then grouped into families and filtered for significance, a selection made by OpenAI GitHub repository ↗ RuntimeWire ↗. Two pieces of work did not follow the fixed procedure: the zeta function zero free region and a Hodge conjecture case, and the 11/12 zeta write up was edited by humans for readability GitHub repository ↗.
Counts from the OpenAI repository README and history log as of October 7, 2026 GitHub repository ↗ History log ↗.
The main limit is checking. OpenAI warns that some results without Lean proofs could have issues GitHub repository ↗, and three papers were already withdrawn for an error History log ↗. A Lean proof checks the formal statement, but a person still has to confirm that the statement matches the claim in the paper. Because the model is not public, outsiders cannot rerun the process RuntimeWire ↗.
Which fields could this affect?
The immediate value is a large pool of proposed results for experts to inspect; most other uses depend on verification, and these connections are our assessment.
Pure mathematics
Specialists can read, test and build on individual claims, and the Lean files let them check some proofs by computer GitHub repository ↗. Each claim still needs review in its own field.
Explore scienceFormal verification
Hundreds of new Lean formalisations give proof checking tools a large real test set History log ↗. Results without Lean proofs remain candidates for future formalisation GitHub repository ↗.
Explore softwareTheoretical physics
Some families concern quantum systems and fluid equations. If validated, they could sharpen mathematical understanding behind physics models.
Explore scienceEveryday technology
Results in number theory or quantum theory sometimes feed into cryptography or computing over many years. This release demonstrates no new product or device.
What has been checked?
The evidence is a company release of preprints with partial computer checked proofs, not peer reviewed papers. Leapscope reviewed these sources; we did not repeat the experiments.
Shown so far
- OpenAI published the manuscripts, reasoning summaries for 10 families and compute estimates OpenAI post ↗ GitHub repository ↗.
- Around 300 of 719 top line results have Lean formalisations that anyone can run History log ↗.
- Errors are being found and logged: three manuscripts were withdrawn and 14 revised within a day History log ↗.
Still unknown
- How many unformalised results are correct; OpenAI says some could have issues GitHub repository ↗.
- Whether each Lean statement matches what its paper claims, which needs human review.
- Which model produced the work and how much human selection shaped the final set GitHub repository ↗ RuntimeWire ↗.
Evidence status: Mixed verification. Stage: Claim. Verification is ongoing and uneven across the collection.
From release to accepted mathematics
This is our suggested way to follow the collection, not a promised timetable.
Can I use it today?
Anyone can read the manuscripts and run the Lean checks from the public repository GitHub repository ↗. The model that produced them is internal and not available, so the process cannot be reproduced by outsiders yet OpenAI post ↗ RuntimeWire ↗.
A few things you might be wondering
Did AI just solve 722 math problems?
No. 722 is the original count of manuscripts, many of which are companion papers inside 372 families, and three have since been withdrawn GitHub repository ↗ History log ↗. A manuscript is a claim until experts confirm it.
Does a Lean proof mean a result is definitely right?
It means a computer checked the formal statement. People still need to confirm the formal statement says what the paper claims. About 42 percent of top line results have Lean proofs History log ↗.
What do mathematicians think?
Views are mixed. The advisory group OpenAI consulted said its role is not an endorsement and that only the mathematical community can assess the results AGMAI statement ↗.
Go straight to the sources
Checked Oct 8, 2026. The first source is the original announcement or research. Later sources add independent context; background pages do not validate the result on their own.
01OpenAI's announcement of the collection, its release process and its caveats.
Counts, how results were produced, verification notes and the list of reasoning summaries.
Log of withdrawals, fixes and new Lean formalisations.
Descriptions of every result family with links to manuscripts and Lean notes.
The independent advisory group's members, guidelines and statement on the release.
News report noting the selection was OpenAI's own and that Lean files do not verify every paper.