OpenAI Math Proofs Face Backlash Over Lean Formalization Gaps

A Flood of Proofs, and a Cold Reception

OpenAI has published 722 mathematical manuscripts covering 372 families of results, which the company says include solutions to hundreds of open questions 4. The papers are on GitHub alongside summaries of the reasoning produced by an unreleased internal frontier model, compute estimates, and statistics on how many problems the system attempted 4. OpenAI says the average result took compute roughly equivalent to three hours of ChatGPT Pro thinking, and it released many of the proofs in Lean, a programming language whose proofs can be checked by a computer 4.

The release follows OpenAI's September claim that the same unreleased model had solved the Navier-Stokes problem, a question nearly 90 years old and one of mathematics' million-dollar prize problems 42. Many working mathematicians reacted with hostility rather than celebration 1. A group called the Association for Human Mathematics issued a statement rejecting OpenAI's assertion that the release advances the field and calling on fellow mathematicians to respond 1. Fields Medal winner Terence Tao reshared the statement, which effectively endorsed it 1.

The Lean Mismatch

The most concrete technical objection concerns the Navier-Stokes proof. A team of mathematicians says OpenAI made a subtle error when it published the work 3. OpenAI's GitHub repository says it contains Lean 4 formalizations of the results in its paper, which implies the human-readable proof and the machine-checked proof are the same 3. The critics say they are not identical. In Lemma 8.6, the natural-language version requires a certain value to stay below m + 4, where m is a whole number. The critics say the Lean version does not express exactly the same condition 3.

The critics are careful about what they are claiming. Anders Hansen of the University of Cambridge says the discrepancy does not show the proof is wrong, and also that his team is not saying it is correct 3. The point is about trust. If the formal code does not faithfully encode the paper, then a successful Lean check certifies something slightly different from what the paper states. Hansen says every LLM-generated proof will therefore have to be read by humans, and that this places an enormous extra burden on mathematicians 3.

A Dispute Over Who Gets Credit

A second controversy concerns how the Navier-Stokes proof was described. Early accounts, including OpenAI's own, said the 166-page proof followed a strategy developed by Spanish mathematicians Diego Córdoba and Luis Martínez-Zoroa 2. That framing led to a public clash with Tristan Buckmaster of New York University. Buckmaster had spent much of the past year using LLMs to pursue that same "Spanish program" with Levent Alpöge, who works at Anthropic, OpenAI's rival 2.

Experts working through the paper now say the proof does not follow that program at all 2. Gonzalo Cao-Labora of EPFL says the approach turns out to be different once you look at the details 2. This is partly a question of credit. It also shows how hard it is to understand what a long, opaque machine-generated argument is actually doing, even for specialists in the area.

Where the Accounts Agree and Differ

The four reports do not contradict one another on the facts, but they emphasize different things. The business-oriented coverage presents the release mainly as a scale and transparency story: numbers of papers, compute figures, and formal verification 4. The science outlets focus on whether the work can be verified and how it was characterized 23. Futurism focuses on the community's anger, especially the resentment that the models may draw on mathematicians' own work while leaving humans to untangle sometimes nearly incomprehensible output 1.

Why It Matters

The central issue is not whether AI can produce valid mathematics. It is who pays the cost of confirming that it has. Lean formalization was supposed to answer exactly this objection, because machine checking would remove the need to trust the model. The Lemma 8.6 dispute shows a weakness in that promise. A formal proof is only as reliable as the translation from the claim people care about into code, and checking that translation still takes expert human attention 3.

By releasing hundreds of results at once, OpenAI has in effect shifted the verification work onto a community that did not ask for it and is not paid for it. The strong reaction from mathematicians looks less like resistance to new tools and more like a refusal to absorb that cost. Until AI labs show that formal statements faithfully match the theorems they claim, high proof counts will not buy much credibility with mathematicians. The Navier-Stokes episode suggests that credibility now matters more than speed.