On October 6, OpenAI released 719 mathematical manuscripts produced by an internal AI model that the public cannot use. They are organized into 372 families of related results, and some of the claims are startling.
Among the manuscripts are claimed proofs of the Unique Games Conjecture, a major open problem in theoretical computer science, and L = RL = BPL, a result that would show certain forms of randomness add no computational power when memory is severely limited.
The collection also includes claimed progress on longstanding mathematical problems involving the Riemann zeta function and the Hodge Conjecture.
Computer scientist Scott Aaronson described the release as a potentially historic turning point for mathematics.
But there is an important distinction between producing a proof and establishing that it is correct.
For now, this is an extraordinary collection of mathematical claims, and independent scrutiny is still underway.
OpenAI released 719 manuscripts from about 4 000 problems
OpenAI says its model was presented with approximately 4 000 mathematical problems.
The resulting collection contains 719 manuscripts organized into 372 families, which group related results, alternative proofs and supporting arguments.
On average, each result required approximately three hours of ChatGPT Pro thinking compute using the unreleased model.
The figures do not establish a straightforward success rate. The manuscripts represent different kinds of mathematical contributions, and multiple papers can belong to the same family.
Some of the claims concern problems that mathematicians have investigated for decades.
For example, one manuscript, titled The Unique Games Theorem, presents a claimed proof of the Unique Games Conjecture.
Another, Exact Derandomization of Logarithmic Space: L = RL = BPL, claims to resolve a longstanding question about randomness and memory-limited computation.
The repository also includes a claimed zero-free region for the Riemann zeta function, specifically where the real part exceeds 11/12. This is not a proof of the Riemann Hypothesis.
Another result concerns the Hodge Conjecture for a particular class of mathematical objects known as CM abelian varieties, rather than the general conjecture.
The significance of these results would be substantial if they survive mathematical scrutiny.
About 42% of the top results have machine-checked proofs
According to OpenAI, approximately 42% of the collection’s top-line results have been formalized in Lean, a programming language and proof assistant used to verify mathematical arguments.
That matters.
Unlike an ordinary mathematical manuscript, a formal proof can be checked by software to determine whether its logical steps follow from precisely stated assumptions.
A successfully checked Lean proof provides strong assurance that the formalized statement follows from those assumptions.
But there is a catch.
A computer can verify a proof without establishing that the statement being proved is exactly the one mathematicians intended.
If the formalized statement differs subtly from the original mathematical problem, the verification may be correct while the intended question remains unanswered.
Human experts must still examine whether the formalization accurately captures the original claim.
The remaining results lack accompanying Lean formalizations, and OpenAI acknowledges that some may contain errors.
Even the formally verified results therefore require careful interpretation.
Some proofs are hard even for experts to follow
There is another problem beyond correctness: understanding.
Aaronson described how mathematicians were beginning to examine the newly released results, including the claimed Unique Games proof.
Dana Moshkovitz, a researcher with expertise in the conjecture, reportedly found parts of the AI-generated manuscript difficult to follow, including confusing citations, and was using AI tools to help interpret it.
For centuries, mathematical proofs have served two purposes.
They establish that a statement is true, but they also help explain why it is true.
A good proof can reveal connections between seemingly unrelated ideas, introduce new techniques and inspire further discoveries.
AI-generated mathematics may begin separating those functions.
A computer could establish the formal correctness of a theorem while the human mathematical community struggles to understand the argument or recognize its broader significance.
That raises an unusual possibility: mathematicians could become convinced that a result is correct before anyone has developed an intuitive explanation for it.
Mathematicians may become auditors of machine proofs
If many of these results survive scrutiny, the way mathematical research is conducted could change substantially.
AI systems might generate candidate proofs at a scale that human mathematicians cannot match.
Researchers would increasingly become auditors, interpreters and question-setters, deciding which results deserve attention and what they reveal about mathematics.
OpenAI says it consulted an independent advisory group at the Institute for Advanced Study about releasing the collection.
The group’s involvement should not be interpreted as an endorsement of OpenAI’s publication process or an independent validation of the mathematical claims.
The release also raises questions about scientific institutions.
Who receives credit for a theorem produced by an AI model? How should researchers cite it? And how should academic journals evaluate hundreds of manuscripts arriving simultaneously?
There are implications beyond mathematics.
Aaronson noted the relative absence of cryptography from the released collection and reported hearing that AI laboratories were investigating whether advanced models could break important cryptographic systems.
That is not evidence that any particular cryptographic system has been broken.
Nevertheless, cryptography depends heavily on mathematical problems being difficult to solve. Major advances in automated mathematical reasoning could eventually have consequences far beyond academic research.
The coming months will test the claims
The coming months should provide a clearer picture of the collection’s significance.
Some results may be independently confirmed. Others may require corrections, and some could turn out to be incorrect.
Particularly important will be expert assessments of the most consequential claims, including the Unique Games proof and the proposed derandomization result.
Another useful measure will be how many currently unformalized results acquire machine-checkable proofs.
OpenAI has said it intends to update the repository as additional formalizations become available and preserve a public record of corrections.
For now, the appropriate response is serious attention without assuming that every claim is correct.
Something important has happened, but how important remains uncertain.
The deeper question may not be whether AI can produce mathematical proofs.
It is what happens when machines can produce them faster than humans can understand them.