This is going around due to rumors and baseless speculation on Twitter [1] right now that Anthropic has solved the Millennium problem related to Navier-Stokes [2]
This is a step beyond baseless predictions. Tao also had a "weird" "hypothetical" comment about LLMs solving complex proofs with impossible to human verify Lean.
There are theorems like that now, like de Grey's lower bound for the Hadwiger-Nelson (unit distance graph) problem. He used a SAT solver to check that a certain graph with 1581(?) vertices is not 4-colorable. There's no way for a human to check that.
Even simpler, imagine Anthropic announces Goldbach's conjecture is false and they have a billion digit counterexample. Anyone can download it (300MB compressed), but how do you check it?
Doron Zeilberger for decades has expected incomprehensible computer proofs to eventually take over mathematics.
Lol as far as I know that post was the origin of that claim and it's clearly just a guy predicting something that will happen in the future with no information about it.
Yeah, can't read anything on xitter due to the gigantic dickover they put over the content when you don't have an account. A screenshot would've been more helpful than an xitter link.
Why would they send it out for "expert review"? Every time, they have just made the AI generate a Lean proof. In fact, it seems like the most plausible direction to NS is computationally assisted detection of a blowup solution, which has fantastic automatic validation.
The surface of bugs in Lean is infinitely smaller than the human error involeved in a committee of peer reviewers. It's way more probable to say "it's proven because Lean says so" than "it's proven because a couple of reviewers said so".
Also, if a bug is found, all previosuly proven theorems can be reproven to immediately and conclusively find out if things went wrong somewhere
As the recent "proof" of the Collatz conjecture shows, that's not enough in an adversarial context. Human mathematicians don't submit proofs that take advantage of soundness bugs in Lean. AIs do.
Exactly, and the advantage is that checking that the problem is "formalized" here is essentially isolated to verifying that the final theorem statement matches the claim. If there are no 'sorry's and the program compiles, then it has been proven. That's the point of Lean.
Each word of your answer is carefully chosen. I'll add one sentence though: you let time do its job.
Of course there may be errors in lean, of course AI can take advantage of it, of course "carefully" is full of errors. So the only thing left is waiting to see if the result holds. And yes, it may take 30 years...
For a second I thought they were aiming the scary proof machine at us mortals doing PDE stuff. Fortunately the speculation is just that they happen to be aiming it at a nearby mathematician type problem. Phew.
None really. It just says if the NS equations are realistic and can really model real physics or there exist some solutions that make it blow up (infinite energy). But even if that would exist (a solution that blows up) it doesn't mean it doesn't work for 99,999999% of the stuff we're interested in.
The question is basically a pure math question about PDEs.
Maximally, a closed form solution would remove the need for Computational Fluid Dynamics. Any property could be derived from a (presumably expensive) analytic function.
Minimally. It could say that no such analytic function can ever exist. Which would be rather boring.
Turbulent fluids look awfully predictable with their spirals….
That would be surprising IMO. We have closed form solutions to Newton’s Laws plus gravity (albeit not very many of them), we have several closed form solutions to Einstein’s equation in GR, and we have a whole lot of closed form solutions to Maxwell’s equations. But we still use numerical methods to solve interesting problems in all of these fields.
Honestly, for practical engineering purposes not that much. The Navier-Stokes equations are an approximation for a mathematically ideal in-compressible fluid. Even ignoring compressibility, physical fluids in the real world are not continuous fields since they are composed of discrete molecules. However, for that small class of problems where an analytic solution can be found, then it means you can be confident in the answer (it won't blow up to infinity), and that there are no other alternate solutions to the same problem.
This is essentially irrelevant to the content of the post, but it's amusing to me that he casually mentions submitting to JAMS as if its acceptance were a mere formality.
> With hindsight, some of my past rejections have become amusing. With a coauthor, I once almost solved a conjecture, establishing the result with an "epsilon loss" in a key parameter. We submitted to a highly reputable journal, but it was rejected on the grounds that it did not resolve the full conjecture. So we submitted elsewhere, and the paper was accepted.
> The following year, we managed to finally prove the full conjecture without the epsilon loss, and decided to try submitting to the highly reputable journal again. This time, the paper was rejected for only being an epsilon improvement over the previous literature!
Uh, care to explain? I have several colleagues that stopped submitting to journals once they reached full professor. They only submit papers from their students for the benefit of their careers. First-author papers, not so much.
Touche, I used to work in pure probability where that ridiculous Hardy-Littlewood rule used to cause all sorts of problems, but now work in statistics, where it is no longer an issue.
To be clear, the colleagues I am referring to mostly work in math phys. They are sole author papers, but I refer to them as first author, since that is the language I am now accustomed to.
And no, the culture in maths vs. theoretical stats is not really that different at the end of the day, and the latter is most assuredly like other STEM fields. I still collaborate on pure math papers (geometric analysis and PDEs mostly) from time to time, and it isn't really a different head space. My name is typically later in the alphabet, so I never even think about the alphabetical ordering.
In classical Newtonian physics, singularities exist, but only in frictionless systems. One example is the driven oscillator. Another more complex one the https://en.wikipedia.org/wiki/Painlev%C3%A9_conjecture .
However, as soon as friction is taken into account, the singularities (e.g., infinitely high amplitudes in the oscillator) are damped.
Fluids without internal friction or viscosity are described by the Euler equations. Therefore, singularities (finite time blowups) occur there, which has recently been shown with a computer assisted proof:
The Navier-Stokes equations are the Euler equations plus friction/viscosity: As a physicist, I do not expect singularities there, since energy is always lost due to friction.
I don’t think this problem is very relevant. The Millennium Problem only asks about the smoothness of solutions to the incompressible Navier-Stokes equations. Real fluids are compressible and also conduct heat. In other words, if you solve the problem, you only learn how fluids behave under unrealistic assumptions. Physically speaking, one learns nothing from such mathematical exercises. Furthermore, singularities in the velocity field essentially imply velocities greater than the speed of light. That, too, is physically nonsensical, as we know from the theory of relativity. In other words, the solution only tells us that the incompressible Navier-Stokes equations are not realistic. But physicists have known that for a long time.
It’s pretty crazy what dynamics you get from NS.. until one realise they emerge from a tiny part of the solution space of Einstein equations.. which themselves emerge at the low energy limit of sth much bigger.
Can you actually credibly find NS or even Euler’s equations as an effective theory from GR?
Euler’s equations and NS have this pesky velocity field, which requires the fluid’s state to be well described by a velocity at each point in space (and a density and a pressure, but I think GR has no problem with those). This means that you need some kind of interaction between particles to get them to exchange energy so that they thermalize instead of staying in the collisionless regime. (In other words, if you have two blobs of fluid collide, you need them to not go right through each other.) And I don’t think that GR is dissipating on the relevant scales.
As a real-world example, the universe contains neat structures (the horsehead nebula is a somewhat famous example) that are consistent with dark matter distributions that don’t really resemble fluids.
Ps: your comment on dissipation is good. But in certain frames GR can reproduce that. I’m far from an expert, but definition of energy is rly hard in GR (need both Noether thms).
Research on the topic seems to have stalled a decade ago. Probably for a good reason.
but you might need to understand it in the context of holography
in some frame you can recover non-relativistic symmetries, we got a paper on this back then, but so hardcore i only understand parts of it https://arxiv.org/abs/1205.5777
PS2: AdS/CFT (and we have at least one good candidate since Maldacena in string theory) correspondence shows that strongly coupled quantum systems in d dimensions are dual to *classical* gr systems in d+1 dimensions.
Somewhere somehow dualities seems to relate completely different systems, that non relativistic dissipative systems happen in all generality somewhere in that mess is barely a surprise.
I mean, if one believes ER=EPR GR and quantum mechanics are just the same thing.
Interesting to see that they are not using the coordinate-free representation (exterior calculus, differential forms) that mathematical physicists prefer to use today.
Those notations are used when writing down the models, because they make clear the intrinsic geometry, the basic symmetries, etc. But they're not used so much in the study of solutions to the equations. Solutions tend to have peculiar features, tend to break underlying symmetries, etc. and there only needs to be one nasty particular solution to prove the NS conjecture wrong.
This is going around due to rumors and baseless speculation on Twitter [1] right now that Anthropic has solved the Millennium problem related to Navier-Stokes [2]
[1] https://x.com/AndrewCurran_/status/2096062392442724805 for example
[2] https://en.wikipedia.org/wiki/Navier%E2%80%93Stokes_existenc...
relevant: https://mathstodon.xyz/@tao/117219101339291693
Key quote : "Solving the problem by purely AI-powered methods [would be a] net negative for the progress of mathematics."
This is a step beyond baseless predictions. Tao also had a "weird" "hypothetical" comment about LLMs solving complex proofs with impossible to human verify Lean.
There are theorems like that now, like de Grey's lower bound for the Hadwiger-Nelson (unit distance graph) problem. He used a SAT solver to check that a certain graph with 1581(?) vertices is not 4-colorable. There's no way for a human to check that.
Even simpler, imagine Anthropic announces Goldbach's conjecture is false and they have a billion digit counterexample. Anyone can download it (300MB compressed), but how do you check it?
Doron Zeilberger for decades has expected incomprehensible computer proofs to eventually take over mathematics.
Lol as far as I know that post was the origin of that claim and it's clearly just a guy predicting something that will happen in the future with no information about it.
Elliot Glazer (FrontierMath lead) traces how it snowballed over time
https://x.com/ElliotGlazer/status/2096298696438906934
Not reading any x.com content until xcancel and nitter are back.
Yeah, can't read anything on xitter due to the gigantic dickover they put over the content when you don't have an account. A screenshot would've been more helpful than an xitter link.
here you go: https://nitter.kareem.one
Dear diary...
Why would they send it out for "expert review"? Every time, they have just made the AI generate a Lean proof. In fact, it seems like the most plausible direction to NS is computationally assisted detection of a blowup solution, which has fantastic automatic validation.
Anthropic sent out its Fermat's Last Theorem result to an expert on formalizing Fermat's Last Theorem in Lean, for what that's worth.
How do you know the lean is correct? You don’t bet the two trillion dollar company on “the ai said so”
The surface of bugs in Lean is infinitely smaller than the human error involeved in a committee of peer reviewers. It's way more probable to say "it's proven because Lean says so" than "it's proven because a couple of reviewers said so".
Also, if a bug is found, all previosuly proven theorems can be reproven to immediately and conclusively find out if things went wrong somewhere
You carefully check that the problem is formalized correctly and then trust the Lean machinery to check the proof.
As the recent "proof" of the Collatz conjecture shows, that's not enough in an adversarial context. Human mathematicians don't submit proofs that take advantage of soundness bugs in Lean. AIs do.
Exactly, and the advantage is that checking that the problem is "formalized" here is essentially isolated to verifying that the final theorem statement matches the claim. If there are no 'sorry's and the program compiles, then it has been proven. That's the point of Lean.
Each word of your answer is carefully chosen. I'll add one sentence though: you let time do its job.
Of course there may be errors in lean, of course AI can take advantage of it, of course "carefully" is full of errors. So the only thing left is waiting to see if the result holds. And yes, it may take 30 years...
> You don’t bet the two trillion dollar company on “the ai said so”
Making an ill-advised press release hardly dooms the company. Just like the hugging face incident hasn't doomed OpenAI.
I feel like that's exactly what's happened.
For a second I thought they were aiming the scary proof machine at us mortals doing PDE stuff. Fortunately the speculation is just that they happen to be aiming it at a nearby mathematician type problem. Phew.
If it is solved what are the applications of that? What changes?
None really. It just says if the NS equations are realistic and can really model real physics or there exist some solutions that make it blow up (infinite energy). But even if that would exist (a solution that blows up) it doesn't mean it doesn't work for 99,999999% of the stuff we're interested in.
The question is basically a pure math question about PDEs.
Maximally, a closed form solution would remove the need for Computational Fluid Dynamics. Any property could be derived from a (presumably expensive) analytic function.
Minimally. It could say that no such analytic function can ever exist. Which would be rather boring.
Turbulent fluids look awfully predictable with their spirals….
That would be surprising IMO. We have closed form solutions to Newton’s Laws plus gravity (albeit not very many of them), we have several closed form solutions to Einstein’s equation in GR, and we have a whole lot of closed form solutions to Maxwell’s equations. But we still use numerical methods to solve interesting problems in all of these fields.
Honestly, for practical engineering purposes not that much. The Navier-Stokes equations are an approximation for a mathematically ideal in-compressible fluid. Even ignoring compressibility, physical fluids in the real world are not continuous fields since they are composed of discrete molecules. However, for that small class of problems where an analytic solution can be found, then it means you can be confident in the answer (it won't blow up to infinity), and that there are no other alternate solutions to the same problem.
NS absolutely does not only apply to incompressible fluids and is far more fundamental than you are implying.
[dead]
if there's anything that would convince that LLMS are one of the biggest innovations ever, it would be this :-D
@dang please can we add a [2014] to the title ?
Yes please. For a moment I thought Terrence Tao had scooped Anthropic.
See https://www.quantamagazine.org/theory-of-fluids-enters-the-2... if you want to know what the Navier Stokes equations are about.
This is essentially irrelevant to the content of the post, but it's amusing to me that he casually mentions submitting to JAMS as if its acceptance were a mere formality.
He has rejected papers too https://mathstodon.xyz/@tao/113721192051328193
> With hindsight, some of my past rejections have become amusing. With a coauthor, I once almost solved a conjecture, establishing the result with an "epsilon loss" in a key parameter. We submitted to a highly reputable journal, but it was rejected on the grounds that it did not resolve the full conjecture. So we submitted elsewhere, and the paper was accepted.
> The following year, we managed to finally prove the full conjecture without the epsilon loss, and decided to try submitting to the highly reputable journal again. This time, the paper was rejected for only being an epsilon improvement over the previous literature!
It basically is a formality at this level. Many top math researchers now hardly even submit to journals at all and just put up a preprint.
At this scale, peer review happens by the audience. They don't need a journal to get people reviewing their work.
None of this is true.
Uh, care to explain? I have several colleagues that stopped submitting to journals once they reached full professor. They only submit papers from their students for the benefit of their careers. First-author papers, not so much.
The fact that you talk about 'first author' papers in math only reinforces my point. It's not the same culture as other STEM fields.
Touche, I used to work in pure probability where that ridiculous Hardy-Littlewood rule used to cause all sorts of problems, but now work in statistics, where it is no longer an issue.
To be clear, the colleagues I am referring to mostly work in math phys. They are sole author papers, but I refer to them as first author, since that is the language I am now accustomed to.
And no, the culture in maths vs. theoretical stats is not really that different at the end of the day, and the latter is most assuredly like other STEM fields. I still collaborate on pure math papers (geometric analysis and PDEs mostly) from time to time, and it isn't really a different head space. My name is typically later in the alphabet, so I never even think about the alphabetical ordering.
In classical Newtonian physics, singularities exist, but only in frictionless systems. One example is the driven oscillator. Another more complex one the https://en.wikipedia.org/wiki/Painlev%C3%A9_conjecture . However, as soon as friction is taken into account, the singularities (e.g., infinitely high amplitudes in the oscillator) are damped.
Fluids without internal friction or viscosity are described by the Euler equations. Therefore, singularities (finite time blowups) occur there, which has recently been shown with a computer assisted proof:
https://www.quantamagazine.org/computer-helps-prove-long-sou...
The Navier-Stokes equations are the Euler equations plus friction/viscosity: As a physicist, I do not expect singularities there, since energy is always lost due to friction.
I don’t think this problem is very relevant. The Millennium Problem only asks about the smoothness of solutions to the incompressible Navier-Stokes equations. Real fluids are compressible and also conduct heat. In other words, if you solve the problem, you only learn how fluids behave under unrealistic assumptions. Physically speaking, one learns nothing from such mathematical exercises. Furthermore, singularities in the velocity field essentially imply velocities greater than the speed of light. That, too, is physically nonsensical, as we know from the theory of relativity. In other words, the solution only tells us that the incompressible Navier-Stokes equations are not realistic. But physicists have known that for a long time.
It’s pretty crazy what dynamics you get from NS.. until one realise they emerge from a tiny part of the solution space of Einstein equations.. which themselves emerge at the low energy limit of sth much bigger.
Can you actually credibly find NS or even Euler’s equations as an effective theory from GR?
Euler’s equations and NS have this pesky velocity field, which requires the fluid’s state to be well described by a velocity at each point in space (and a density and a pressure, but I think GR has no problem with those). This means that you need some kind of interaction between particles to get them to exchange energy so that they thermalize instead of staying in the collisionless regime. (In other words, if you have two blobs of fluid collide, you need them to not go right through each other.) And I don’t think that GR is dissipating on the relevant scales.
As a real-world example, the universe contains neat structures (the horsehead nebula is a somewhat famous example) that are consistent with dark matter distributions that don’t really resemble fluids.
Ps: your comment on dissipation is good. But in certain frames GR can reproduce that. I’m far from an expert, but definition of energy is rly hard in GR (need both Noether thms).
Research on the topic seems to have stalled a decade ago. Probably for a good reason.
sorry for the late answer..
yes you can : https://arxiv.org/abs/1211.1983
but you might need to understand it in the context of holography
in some frame you can recover non-relativistic symmetries, we got a paper on this back then, but so hardcore i only understand parts of it https://arxiv.org/abs/1205.5777
PS2: AdS/CFT (and we have at least one good candidate since Maldacena in string theory) correspondence shows that strongly coupled quantum systems in d dimensions are dual to *classical* gr systems in d+1 dimensions.
Somewhere somehow dualities seems to relate completely different systems, that non relativistic dissipative systems happen in all generality somewhere in that mess is barely a surprise.
I mean, if one believes ER=EPR GR and quantum mechanics are just the same thing.
Could you expand? Curious.
sorry for the late reply, see answer above
Interesting to see that they are not using the coordinate-free representation (exterior calculus, differential forms) that mathematical physicists prefer to use today.
Those notations are used when writing down the models, because they make clear the intrinsic geometry, the basic symmetries, etc. But they're not used so much in the study of solutions to the equations. Solutions tend to have peculiar features, tend to break underlying symmetries, etc. and there only needs to be one nasty particular solution to prove the NS conjecture wrong.
[dead]