After Math

On September 8th, 2026, OpenAI claimed to have produced an AI-generated solution to the Navier–Stokes existence and smoothness problem, one of the seven Millennium Prize Problems. This announcement sparked debate over the roles of humans and machines in the discovery, and intensified comparisons to earlier AI successes in fields traditionally seen as human domains.

Tristan Buckmaster, a mathematician involved in the Navier–Stokes saga, likened the achievement to Deep Blue's victory over Garry Kasparov in chess, raising existential questions for the field.

Should mathematicians simply continue their work, adapting to new practices? The comparison is apt, as in games like chess or Go, the process—playing the game—is as crucial as the outcome. However, in the realm of mathematics, this seems unnecessary. Instead of accepting mathematics as a game that necessitates such a retreat, we can challenge the characterization of mathematics as a game that demands this retreat.

The narrative that AI has "solved" mathematics is based on two assumptions: first, that AI has indeed solved a mathematical problem; second, that mathematics is solely about problem-solving. The first assumption is flawed because a mere answer, even one formally certified, does not constitute a true solution. A genuine solution requires an intelligible proof that human mathematicians can understand and utilize to advance the field.

Even if AI provided such a proof, the second assumption—the view that mathematics is solely about problem-solving—would also be incorrect, as mathematics encompasses much more than that. Mathematicians also aim to develop new concepts and theories, ask and answer new questions, unify disparate areas, educate and sustain scholarly communities, and produce beautiful and deep work.

OpenAI's AI provided an answer: yes, the Navier–Stokes problem has a solution. However, the solution provided by OpenAI—two artifacts that appear to be proofs—leaves much to be desired. While the first artifact is a Lean formalization that meets the logical standards for proof, the second artifact is an informal proof. The issue lies with the definition of proof itself, which consists of two notions: the logical notion (which can be checked mechanically) and the intelligible notion (which requires understanding and insight).

The AI's proof meets the logical standards but lacks the intelligible aspect, which is crucial for mathematicians who seek to grasp the underlying ideas and use them to make further progress. Thus, OpenAI's AI solution falls short of providing the comprehensive, intelligible proofs mathematicians desire.