Before discussing the importance of the result, what exactly did OpenAI claim?
Taras: OpenAI claims that its system constructed a solution of the three-dimensional incompressible Navier–Stokes equations that starts from rest, uses a smooth external force, maintains bounded kinetic energy, but develops unbounded velocity in finite time.
The result is presented as an analytical proof rather than a numerical experiment. The authors also published a formalised version in Lean. It is important to say "OpenAI claims" because the proof still requires independent mathematical checking. The paper is publicly available, but publication by OpenAI and Lean formalisation do not automatically mean that the result has already been universally accepted by the mathematical community.
Is this just a numerical simulation that appears to blow up?
Taras: No. A numerical simulation could show very large velocities, but it would not prove that the velocity becomes infinite in finite time. Numerical results are also affected by discretisation, resolution, and numerical instability.
OpenAI's paper describes an explicit analytical construction. The authors define velocity and pressure fields with carefully selected scaling properties and then prove estimates for the remaining errors. The purpose is to show mathematically that the velocity becomes unbounded while the relevant energy remains bounded.
As a mathematician with a PhD in mathematics, what was your first reaction?
Taras: My first reaction would be cautious interest. A claimed resolution of a long-standing PDE problem deserves attention, but it also deserves a very precise reading.
There are three separate questions:
- First, is the construction mathematically correct?
- Second, does it satisfy the exact conditions in the Clay formulation?
- Third, maybe the most interesting for me, how significant is the underlying method beyond this particular example?
These questions should not be merged. A proof can be technically correct but apply to a narrower formulation than people assume. Conversely, a result can use familiar tools and still prove something genuinely new.
Did OpenAI create a completely new mathematical theory?
Taras: Based on the published paper, I would not describe it as a completely new theory of partial differential equations.
The construction uses many established methods from PDE analysis. These include self-similar variables, cylindrical coordinates, axisymmetric flow analysis, energy estimates, linearization around a background solution, oscillatory waves, stress cancellation, Fourier or angular-mode decompositions, heat-equation estimates, vector potentials, iterative corrections, and localisation.
So the fairest description is that the result is based largely on established mathematical ideas, combined in a new and highly specialised construction.
What is the first major method in OpenAI's construction?
Taras: The first major component is a self-similar, anisotropically collapsing vortex.
The flow is organised around an axis. Near the singular time, the radial and axial dimensions shrink at different rates. The central region becomes increasingly concentrated, while the azimuthal and axial velocities increase.
The construction combines inward radial motion, rotation around the axis, and axial outflow. Incompressibility is important here: if fluid moves inward radially, it must be redistributed in another direction rather than simply accumulating at the axis.
This type of similarity analysis is an established PDE method. The claimed novelty lies in the particular profile that OpenAI constructs and in making it compatible with the later stress-cancellation mechanism and smooth forcing requirements.
Did Lean discover or prove the mathematics?
Taras: Lean did not discover the construction. According to OpenAI's description, the multi-agent system produced the mathematical proof, and the proof was then formalised in Lean.
Lean is a proof assistant. It checks whether a formal sequence of definitions, lemmas, and deductions follows according to its logical rules. That is different from independently inventing the mathematical strategy.
Formalisation is valuable because it can expose hidden assumptions, incorrect algebra, and gaps in long symbolic arguments. But the formalised theorem must still be compared with the intended mathematical claim. Formal verification is strongest when both the formal statement and the underlying model have been carefully inspected.
Then what was genuinely new about the AI contribution?
Taras: The most interesting novelty may be practical rather than theoretical.
OpenAI reports using a large group of collaborating agents. Different groups were given different variants of the problem and explored different directions. The system could read mathematical material, run code, communicate intermediate results, and consolidate useful ideas. OpenAI reports that the Navier–Stokes effort involved approximately 10,000 concurrent agents and that Lean formalisation took an additional period of verification.
This suggests a new research workflow:
- Search many known methods quickly.
- Try different combinations of techniques.
- Identify useful partial constructions.
- Transfer ideas between groups.
- Automate algebraic and computational checks.
- Formalise the final argument.
That is not a replacement for mathematical theory. It is a new way of applying existing theory at a much greater speed and scale.
Could this be described as "old mathematics applied much faster"?
Taras: That is a fair description, with one qualification.
The tools may be old, but a successful new combination that proves a previously unresolved theorem is still original mathematics. It would be misleading to say that nothing new happened simply because the individual components were known.
At the same time, I would not describe the result as a completely new theory comparable to the invention of functional analysis, distribution theory, or a new class of PDE methods.
I would describe it as a new practice of mathematical research: rapidly combining established methods, exploring a large space of constructions, and using formal tools to check the resulting proof.
Why is that practical acceleration so valuable?
Taras: In difficult differential equations, the bottleneck is often not knowing one isolated theorem. The bottleneck is finding a construction in which many constraints are satisfied simultaneously.
A mathematician may know about similarity variables, vortex stretching, Fourier modes, stress tensors, heat kernels, and energy estimates. The difficult part is determining whether they can be combined in the right order and with the right scaling.
How valuable would the result be if the proof is confirmed?
Taras: Mathematically, it would be very valuable. It would establish a finite-time breakdown result for a formulation of the three-dimensional Navier–Stokes existence and smoothness problem that has remained open for decades.
It would also demonstrate that a large analytical construction can be developed with substantial assistance from AI and then formalised in a proof assistant.
What would you tell people who say, "The AI only combined existing methods, so the result is not important"?
Taras: I would disagree with the conclusion, but I would agree with part of the observation.
Combining known tools does not automatically make a result unimportant. Many major mathematical results use established techniques in a new arrangement. The difficulty may lie in finding the correct architecture and proving that every component is compatible with the others.
However, the opposite exaggeration is also a mistake. We should not claim that AI invented a completely new mathematical theory unless the evidence shows that it did.
The balanced statement is: The result appears to rely heavily on established PDE methods, but it may introduce a new construction and a new research practice for combining those methods quickly and verifying them formally.
What is the main lesson for mathematicians?
Taras: The lesson is that mathematical practice may change. Researchers may increasingly use AI systems to explore known techniques, derive intermediate estimates, test examples, organise the literature, and formalise proofs.
This could allow mathematicians to spend more time selecting important problems, designing concepts, interpreting results, and checking whether a formal statement captures the right mathematical question.
But the human role remains essential. Someone must decide which assumptions matter, whether the construction is meaningful, whether the proof matches the intended problem, and what the result actually implies.
So how would you summarise OpenAI's achievement?
Taras: I would summarise it cautiously. OpenAI has reported a sophisticated analytical construction for finite-time blow-up in a forced three-dimensional Navier–Stokes setting.
The potentially new element is not a completely new theory, but the particular way these methods were combined and the speed with which an AI system explored and formalised the construction.
If independent mathematicians confirm the proof, the result would be important both as a theorem in PDE analysis and as evidence that AI can accelerate advanced mathematical research. The most accurate description would be: Established mathematical methods, assembled into a new construction through a new AI-assisted research practice.
