Interviews published October 19, 2026, captured contrasting views from UC Berkeley mathematicians Richard Borcherds and Robin Huang about AI’s place in mathematics. Their debate follows OpenAI’s claimed Navier–Stokes result and an October 6 paper that identifies mismatches between parts of the written proof and its Lean formalization. The paper’s authors do not claim that the written proof is incorrect.
Berkeley mathematicians differ on AI’s role
Borcherds expects AI’s mathematical abilities to advance rapidly and believes the technology could surpass human researchers. Huang, a final-year mathematics Ph.D. candidate at UC Berkeley, is less convinced by current systems’ research usefulness. She has used AI in her own research and described it as inefficient; she also expressed concern about the effects of AI companies’ work on the mathematics community. Those are their individual views, not a shared verdict among mathematicians.
What OpenAI claimed about Navier–Stokes
On September 8, 2026, OpenAI announced a claimed result for the three-dimensional incompressible Navier–Stokes equations. The company says a smooth external force can produce a finite-time singularity, and that its result addresses statements C and D in the Clay Mathematics Institute’s problem formulation.
OpenAI reported that roughly 10,000 agents worked concurrently on the result, generating about 2.7 million messages and 130 billion output tokens. The company said the agents reached their result about 88 hours after launch, with another 17 hours spent on Lean formalization and verification. NeoTeo previously covered OpenAI’s release of mathematical results from an internal model.
What the Lean critique identifies
Lean is a proof assistant: software that checks whether a formal proof establishes a specific, computer-readable mathematical statement. A. Bastounis, F. Circelli, and A. C. Hansen’s October 6 paper examines whether OpenAI’s Lean formalization faithfully represents parts of the company’s written argument. Their paper on the formalization points to differences in particular estimates.
One example concerns the number of input derivatives needed to bound the same torus derivatives of the output. In the natural-language paper, the estimate uses four additional derivatives; the cited Lean estimate uses five.
| Estimate version | Additional input derivatives |
| Natural-language paper | 4 |
| Cited Lean estimate | 5 |
The authors also describe differences between the written and formalized versions of a pressure-flux estimate, whose bounds they say are difficult to compare. These examples concern how the formalization corresponds to the written argument.
Why passing Lean checks is not the same as faithful translation
When Lean accepts a proof, it has checked that the encoded proof establishes the encoded statement under the system’s rules. That check does not, by itself, establish that the statement and reasoning in the code faithfully match the natural-language paper. A formal proof can be valid for what it encodes while differing from the intended written argument.
Bastounis, Circelli, and Hansen limit their claim to mismatches in the formalization they examine. They explicitly do not assess whether OpenAI’s natural-language proof is correct. The distinction at issue is between checking a formal proof and establishing that its formalization preserves the meaning of the written proof.
