In his September 12, 2026 interview, Steven Strogatz described how AI is changing mathematical understanding and researchers’ professional identity. On September 8, 2026, OpenAI reported an analytical proof and Lean formalization concerning a finite-time singularity in forced, three-dimensional, incompressible Navier–Stokes equations. That claim remains independently unverified and is not an accepted solution to the Navier–Stokes Millennium Prize problem. On September 4, Anthropic reported a different kind of achievement: Claude had formalized an existing proof of Fermat’s Last Theorem, using about 29,500 intermediate theorems.
That distinction is the real story. AI is already helping produce and check serious mathematical work, but a company announcement, a machine-checked formalization and an accepted theorem are not interchangeable labels.
AI can move mathematics forward without settling what counts as a breakthrough
OpenAI’s announcement concerns a reported construction for a specific version of the Navier–Stokes equations. Anthropic’s project concerns the formal encoding of mathematics that was already proved by humans. Neither development supports the simple headline that AI has independently solved every problem it touches.
The Navier–Stokes existence and smoothness problem is one of the Clay Mathematics Institute’s seven Millennium Prize Problems, each associated with a $1 million prize. OpenAI’s reported result addresses forced, three-dimensional, incompressible equations and describes a finite-time singularity with unbounded velocity under those conditions. The mathematical question is whether that construction matches the intended problem and survives expert scrutiny—not merely whether software can check a file of formal statements.
Anthropic’s Fermat project has a different profile. It did not discover Fermat’s Last Theorem. It formalized an existing proof associated with Andrew Wiles and Richard Taylor, with Claude agents proving approximately 29,500 intermediate theorems in Lean.
| Project | Mathematical objective | What was reported | What experts still assess | Human contribution at issue |
| OpenAI’s Navier–Stokes work | A finite-time singularity for forced, three-dimensional, incompressible equations | An analytical proof and Lean formalization | Whether the construction addresses the intended mathematical problem and withstands scrutiny | Interpretation, validation, significance and credit |
| Anthropic’s Claude project | Formalization of an existing proof of Fermat’s Last Theorem | About 29,500 intermediate theorems proved in Lean | Whether the formal development faithfully represents the established proof and its assumptions | Translating established mathematics into a machine-checkable form and understanding it |
What OpenAI reported about Navier–Stokes
OpenAI’s September 8 announcement described a finite-time singularity in forced, three-dimensional, incompressible Navier–Stokes equations with finite energy. In plain language, the claim concerns a mathematical evolution in which velocity becomes unbounded in finite time under the stated conditions.
That is a substantial claim—but it is still a claim by OpenAI. A Lean artifact can make the formalized steps mechanically checkable; it does not, by itself, prove that the formalized system captures the exact problem mathematicians intended to solve or that the wider mathematical community accepts the result.
So, does the announcement mean that the Millennium Prize problem is solved? No. OpenAI reported a result and a formalization, but the accepted mathematical status of the problem requires more than a corporate announcement or a machine-readable proof.
Why Claude’s Fermat result is a different kind of achievement
Claude did not discover Fermat’s Last Theorem. Anthropic reported that its agents formalized an existing proof in Lean and proved approximately 29,500 intermediate theorems. The result is important as a large formalization effort, not as a new solution to a theorem already proved by human mathematicians.
That distinction matters because formalization can be laborious even when the underlying mathematics is established. A proof assistant requires definitions, assumptions and individual steps to be expressed in a form that a computer can check. Turning a human-readable proof into that structure can expose gaps, clarify dependencies and create a durable machine-checkable record.
Why Lean checks more—and less—than readers may think
Lean is a proof assistant: software that mechanically checks whether formalized steps follow from encoded definitions, axioms and assumptions. If the formal system accepts the development, the chain of encoded inferences satisfies those rules.
But Lean does not independently decide whether the right problem was formalized. It does not replace the mathematician who determines whether the assumptions match the intended question, whether the result has the claimed scope or whether the argument carries mathematical significance beyond its formal shell.
That is why “machine-checked” and “accepted mathematical solution” describe different milestones. The first concerns the consistency of an encoded development under its rules. The second also involves interpretation, scope, scrutiny and community judgment.
The mathematician’s changing role
Steven Strogatz described the moment as both exciting and unsettling. He argued that mathematicians may need to provide “proof digestion”: explaining machine-generated arguments in terms that people can understand and appreciate. His point is practical. A proof can be formally valid and still be difficult for humans to interpret, connect to existing ideas or evaluate for importance.
Strogatz also warned that mathematical researchers may not be able to compete in breakthrough work without AI in the future. That is a forecast and a concern, not a settled labor-market outcome. The immediate change is more concrete: researchers are confronting tools that can accelerate tasks once limited by human time and attention.
Alex Townsend described that pressure in personal terms after 15 years devoted to research mathematics. He said that an AI system appeared able to surpass his peak research ability, leaving him feeling threatened. His account captures the uncomfortable trade-off: the same tools that can make difficult work feasible can also challenge the status, motivation and sense of mastery built around doing that work unaided.
The next test is understanding
The useful question is not simply whether AI “solved” a famous problem. Ask instead which task the system performed: proposing a new construction, formalizing an existing proof, checking encoded steps or helping a human researcher explore an idea.
Those tasks carry different claims about novelty and mathematical value. OpenAI’s reported Navier–Stokes result still needs the scrutiny required for an accepted mathematical resolution. Anthropic’s Fermat project shows the scale at which AI-assisted formalization can operate, but it does not turn established mathematics into a new discovery.
For now, human mathematicians remain responsible for connecting formal steps to meaning. That role may change as the tools improve, but the decisive standard remains the same: a result must be understood, examined and accepted for the exact problem it claims to address.
