Hundreds of claimed solutions to some of the hardest open problems in mathematics landed in a single week, and the experts OpenAI consulted say the work is far from finished. The short answer: OpenAI’s newest batch of AI math proofs follows some recommended guidelines but misses others, especially on human understanding, formal verification, and transparency, so the results are best treated as claims awaiting peer review rather than settled mathematics.
This guide covers what was released, what mathematicians asked for, where the gaps are, and how to judge the next announcement yourself. It draws on TechCrunch’s October 8, 2026 reporting, plus general background on how proof checking works.
Key Takeaways
- OpenAI released 719 manuscripts containing claimed solutions to hard mathematical problems.
- An advisory group of nine mathematicians had published guidelines for frontier labs just days earlier.
- Only 10 of the 719 manuscripts included the model’s chain of thought.
- No machine-readable metadata linked the natural-language proofs to their formal versions.
- A new paper found at least two mismatches between an English-language proof and its Lean code for a Navier-Stokes-derived problem.
- Mismatches don’t prove the solutions wrong, but they show a compiled formal proof can’t be trusted blindly.
- Mathematicians say a result isn’t truly useful until humans understand it and can build on it.
What Happened in OpenAI’s Math Release?
OpenAI published hundreds of claimed solutions to difficult math problems and said it had consulted mathematicians to avoid repeating an earlier controversy. According to TechCrunch, the lab released the material this week on GitHub. It said it had sought advice from an elite group of researchers because its previous attempt, when a model solved a long-standing problem, set off a public dispute.
TechCrunch’s reporting suggests the consultation didn’t fully translate into compliance. The gap is sharpest where the mathematicians stressed that people, not just machines, must understand a result. The concern is heightened by a fresh paper showing disagreements between the plain-language and formally expressed solutions to a million-dollar problem that OpenAI’s models had ostensibly solved.
These OpenAI math solutions matter beyond one company. They are an early test of how the research community, AI labs, and the press will handle machine-generated discoveries.
What Are AI Math Proofs, and How Are They Checked?
AI math proofs are logical arguments, produced largely or entirely by an AI model, that claim to establish a mathematical statement is true. Like human proofs, they are only as valuable as the community’s ability to verify them, understand them, and reuse their ideas.
Checking happens in two layers, and the distinction explains much of the current dispute.
The Natural-Language Proof
The model first writes an explanation in ordinary mathematical prose, much like a journal article. Human experts can read it, probe it, and argue about it. This is the traditional route, and it depends on reviewers understanding every step.
The Formal Proof in Lean
The model then tries to express the same argument in Lean, a programming language built for proof checking. In theory, if the code compiles, the logic is airtight. This translation step is called autoformalization, and it is where the newest criticism lands.
| Feature | Natural-Language Proof | Formal Lean Proof |
|---|---|---|
| Format | Prose with mathematical notation | Code in a proof assistant |
| Who checks it | Human reviewers and peers | A computer, plus human review of the statement |
| Main strength | Readable, conveys ideas | Mechanically verifiable |
| Main weakness | Errors can hide in gaps | May not match the intended claim |
| Role in community | Builds understanding and reuse | Adds confidence in correctness |
The key insight is that Lean formal verification only guarantees that the code is internally consistent. It does not guarantee the code says what the English proof says.
Who Is AGMAI and What Did It Ask For?
AGMAI is the Advisory Group on Mathematics and Artificial Intelligence, a nine-member panel of prominent researchers hosted by Princeton’s Institute for Advanced Study. Its members work at institutions around the world.
At the end of September, the group published guidelines for frontier labs that solve math problems. Several of the AGMAI guidelines are relevant here:
- Stop testing advanced mathematical problems on proprietary models.
- Release results as soon as possible.
- Include information on how the models reached their conclusions.
- Formalize proofs that people don’t yet understand.
- Include machine-readable metadata that connects natural-language and formal versions.
- Take responsibility for ensuring that human understanding follows, including helping fund the human mathematicians whose work will be needed.
In its statement on the latest release, the group said the mathematical community will ultimately decide how well its recommendations were followed. That is a careful, diplomatic framing, but the underlying facts reported by TechCrunch point to mixed compliance.
How Did OpenAI’s Release Measure Up? A Scorecard
OpenAI met a few of the recommendations, partly met several, and clearly missed at least two. The table below summarizes what TechCrunch reported. It reflects the reporting, not an independent audit, and the advisory group did not respond to TechCrunch’s request for a fuller evaluation.
| AGMAI Recommendation | What Was Reported | Assessment |
|---|---|---|
| Stop testing hard problems on proprietary models | OpenAI’s release says it is evaluating proprietary models on open research problems | Not followed |
| Release results quickly | Results were released promptly | Followed |
| Share how models reached conclusions | Only 10 of 719 manuscripts included chain of thought | Partly followed |
| Formalize hard-to-understand proofs | A 42% figure was reported, but its wording is ambiguous | Unclear |
| Add machine-readable links between English and Lean | Not included | Not followed |
| Take responsibility for human understanding | Reporting says this remains unclear | Unclear |
One caution on the 42% figure: TechCrunch says “just 42%” of the proofs “had not undergone” formalization, a phrasing that can be read two ways. Check the original before quoting it.
What OpenAI Did Well
Releasing quickly and publishing the material openly are both consistent with the advisory group’s principles. Open release lets the community begin scrutiny immediately, which is how mathematics is supposed to work. Including at least some reasoning traces also gives reviewers more to examine than a bare answer would.
Where OpenAI Fell Short
The most significant gap is the first recommendation. The advisory group’s opening request was to stop using advanced open problems as tests for proprietary models, and OpenAI’s release explicitly describes doing exactly that. The second gap is traceability: with chain of thought shared for just 10 of 719 manuscripts, most reviewers cannot see how a conclusion was reached. The third is missing metadata, which makes it harder to check whether an English proof and its Lean counterpart say the same thing.
Why Does Human Understanding Matter in Mathematics?
Because a proof is not just a certificate of truth; it is a tool that other people use. When human mathematicians discover something, they take responsibility for it. They write papers, give talks, and answer questions at seminars. That engagement spreads understanding, reveals techniques that apply to other problems, and eventually allows the knowledge to be used in practical fields.
When a model produces a solution on request, that chain of responsibility can break. Harvard mathematics professor Melanie Wood told TechCrunch that “there is not human understanding of them at the point of release,” and that the real work begins afterward.
This is why the advisory group suggested labs help fund human mathematicians. If AI math proofs arrive faster than people can digest them, someone has to do the digesting, and that labor has a cost.
What Did the “Lost in Translation” Paper Find?
It found at least two discrepancies between the natural-language proof and the Lean code for OpenAI’s solution to a problem derived from the Navier-Stokes equations. Those equations describe the complex behavior of fluids. The paper, from mathematicians at the University of Cambridge and King’s College London, was released the same week as OpenAI’s batch.
Importantly, the discrepancies do not necessarily disprove either version. What they show is a process risk: when a model writes the English argument and also writes the formal version, errors can creep in during translation, and the formal artifact may not capture the original claim.
The authors concluded that OpenAI’s natural-language proof and other autoformalized Lean proofs shouldn’t be trusted at face value. Their view is that these proofs deserve the same peer review and scrutiny as any other mathematical work.
Is a Compiled Lean Proof Enough to Trust a Result?
No. A compiled Lean proof confirms the code is logically consistent, not that it faithfully represents the intended theorem. Think of it like a spell-checker approving a document: it can confirm every word is spelled correctly without confirming the document says what you meant.
The risk areas in autoformalization include:
- Statement mismatch: the formal theorem differs subtly from the claimed one.
- Definition drift: a concept is defined differently in the code than in the prose.
- Hidden assumptions: a condition added to make the code compile quietly weakens the result.
- Missing traceability: without links between prose and code, checking requires redoing the translation by hand.
This is why the advisory group asked for machine-readable metadata. Such metadata would map each claim in the English proof to the corresponding piece of Lean code, letting reviewers spot mismatches far faster. Because it wasn’t included, verifying the Lean formal verification step still demands human effort.
What Are Experts Saying About the Release?
Prominent mathematician Terence Tao has criticized the approach, arguing that problems are being “solved” by prompters who lose interest afterward. In a social media post following the release, he said these operators often don’t understand the output well enough to answer questions, give talks, or otherwise engage with the wider field.
Tao’s concern is about incentives and culture rather than any single proof. If solving a headline problem is the only goal, nobody is left to explain the result, connect it to other work, or maintain the knowledge.
Wood’s remarks echo this from a different angle: release is the start of the work, not the end. And the Cambridge and King’s College authors add a procedural point, that machine-formalized proofs still need ordinary peer review. Together, these views form a consistent message from the field: speed and volume are not substitutes for comprehension.
What Does This Mean for Readers, Researchers, and Journalists?
It means treating headlines about AI math proofs as the beginning of a verification process, not the end of one. Several practical implications follow.
For researchers: expect a surge of material that needs expert attention. Funding and credit systems may need to change so the people who verify and explain machine-generated results are recognized for that work.
For AI labs: the guidelines offer a roadmap. Releasing reasoning traces, linking prose to formal code, and supporting human mathematicians would address the main criticisms reported so far.
For journalists and general readers: announcements that a model “solved” a famous problem deserve skepticism until independent experts weigh in. The question to ask is not just “Does it compile?” but “Do people understand it?”
For the broader AI community: math is a unusually clean testing ground, because correctness can in principle be checked. If standards of verification and transparency can’t be met here, it raises hard questions for messier domains.
How Can You Evaluate Claims About AI Math Proofs?
Use a short checklist. When a new announcement appears, look for these signals:
- Independent review: have outside mathematicians examined the argument?
- Formal version: does a Lean (or similar) proof exist, and is it linked to the prose?
- Statement fidelity: does the formal theorem match the claimed result exactly?
- Reasoning transparency: are the model’s intermediate steps shared?
- Human ownership: is a named person or team prepared to explain and defend the result?
- Community response: are respected researchers engaging, or staying silent?
No single item settles the question, but a result that scores well on most is far more credible than one that scores well on none.
Frequently Asked Questions
Did OpenAI actually solve famous open problems?
Not conclusively. OpenAI claims solutions, but the mathematical community has not finished assessing them, and the advisory group said it is up to that community to judge. A recent paper also found mismatches in one high-profile case that don’t disprove the solution but warrant scrutiny.
What is Lean, and why does it matter?
Lean is a programming language designed for writing proofs that a computer can check. It matters because compiled code offers strong evidence of internal logical consistency, which is much harder to guarantee with prose alone.
Why can’t the model just verify itself?
When the same system writes both the English proof and the Lean code, translation errors can slip through. The “lost in translation” authors argue that such proofs should face normal peer review rather than being trusted automatically.
Are AI math proofs reliable?
They can be, but reliability depends on verification, transparency, and human understanding. The current evidence suggests that some are promising and others need much closer examination, so each result should be judged individually.
What should labs do differently?
According to the guidelines reported by TechCrunch: avoid testing on proprietary models with open research problems, share reasoning traces, formalize proofs people don’t understand, provide metadata linking English and formal versions, and help fund the human work needed to make results meaningful.
Conclusion
The latest wave of AI math proofs shows how fast machine reasoning is moving and how slowly the surrounding norms are catching up. OpenAI followed some of the advisory group’s principles, such as quick release and some reasoning disclosure, but fell short on others, including the request to avoid proprietary-model testing, the sharing of reasoning for most manuscripts, and metadata linking prose to code.
The central lesson is simple: a solution isn’t finished when it’s produced. It’s finished when people understand it, check it, and can build on it. Until then, the responsible way to read any announcement of machine-generated mathematics is as a claim to be tested, not a conclusion to be celebrated.