Dear @el_Commendante,
I would probably be a little more cautious before drawing very strong conclusions from the recent claims around AI and fundamental mathematics.
First, if OpenAI publishes a claimed solution related to the Navier–Stokes problem, I think the right thing to do is simply wait for the actual mathematics.
I am somewhat familiar with this class of equations, and I would be very surprised if such a difficult problem had suddenly been settled in the full sense required by the Millennium Prize formulation without a long period of scrutiny.
The important question is not whether an AI produced something that looks like a proof, or even whether a formal system accepted a theorem.
The important question is: what exactly was proved?
What are the assumptions?
What class of initial data is covered?
What notion of solution is used?
Is the result really global?
Does it address the full 3D incompressible problem, or only some restricted case?
Are there hidden regularity assumptions?
Does the formal statement correspond exactly to the mathematical claim being advertised?
Even a Lean proof, while potentially very valuable, does not automatically settle all of those questions.
If the theorem statement is correct, the assumptions are explicit, and Lean verifies the derivation from those assumptions, that is a very strong result. But formal verification only proves the formal statement that was actually encoded. It does not by itself prove that the formalization corresponds exactly to the original physical or mathematical claim.
So I think we should let mathematicians and specialists examine such a result very carefully before concluding that AI has solved anything of that magnitude.
And this leads to the larger point I wanted to make.
I think it is still too early to say that current AI systems have brought us to a fundamentally deeper understanding of the mathematical structure of our physical world.
There are many problems at least as conceptually difficult as the famous Millennium problems.
The Riemann hypothesis remains open.
P versus NP remains open.
There are deep unresolved questions throughout quantum field theory, mathematical physics, spectral geometry, general relativity and quantum gravity.
And of course the history of mathematics is much broader than the Millennium Prize problems. Hilbert formulated his famous 23 problems in 1900, and a century later the Clay Mathematics Institute selected a different set of seven Millennium problems. These are only landmarks in a much larger landscape.
My personal skepticism is not based on the idea that AI is useless in mathematics. Quite the opposite.
I think AI will become an extremely powerful scientific instrument.
It can already search enormous bodies of literature, combine methods, generate conjectures, write symbolic and numerical code, interact with theorem provers, test special cases and help researchers explore mathematical structures much faster than before.
But there is a difference between being an extremely powerful research instrument and possessing the level of mathematical creativity required for a genuine conceptual breakthrough.
That difference is especially important in areas such as quantum field theory, the Standard Model, general relativity or spectral geometry.
These subjects are difficult not simply because the equations are long.
They involve many layers of abstraction at the same time: geometry, topology, operator theory, functional analysis, symmetry, representation theory, renormalization, causality, observables, and finally the relationship between the mathematics and experimental reality.
Historically, major advances in fundamental mathematics and physics have often come not from solving the existing equations more efficiently, but from inventing a new language in which the problem can be seen differently.
New objects.
New invariants.
New geometrical structures.
New notions of symmetry.
New ways of connecting apparently unrelated areas.
This is where I am still unconvinced by the present generation of language models.
They are very impressive at local reasoning and at recombining existing mathematical knowledge, but they can still lose assumptions over long chains of reasoning, confuse formal consistency with physical meaning, and sometimes validate their own mistakes in surprisingly sophisticated ways.
The example discussed above, where a verification procedure can effectively degenerate into something equivalent to “proof = True”, is actually a very good illustration of the problem.
A system can satisfy the formal test while completely missing the scientific intention of the test.
That is why, at least for now, I would hesitate to describe current LLMs as autonomous mathematical scientists.
I would describe them as increasingly powerful components of a scientific system.
And that system still needs carefully separated stages of hypothesis generation, independent verification, numerical testing, formal proof where possible, comparison with established results, and human examination of the premises and interpretation.
Perhaps future models will cross that boundary.
I actually expect that they eventually will.
But in my view, we are not there yet.
So for the moment I would wait for the Navier–Stokes result, read the actual theorem, let the mathematical community examine it from every possible direction, and only then decide whether we are looking at a major scientific breakthrough or simply another impressive demonstration of what current AI systems can already do.
Evgeny Monakhov
