v64
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_existe
nc...
|
> cacio-e-pepe
relevant:
https://mathstodon.xyz/@tao/117219101339291693
|
> > goldenarm
Key quote : "Solving the problem by purely
AI-powered methods [would be a] net negative for
the progress of mathematics."
|
> strangescript
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.
|
> > throwaway81523
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.
|
> CSMastermind
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.
|
> > krackers
Elliot Glazer (FrontierMath lead) traces how it
snowballed over
timehttps://x.com/ElliotGlazer/status/209629869643
8906934
|
> > > Arodex
Not reading any x.com content until xcancel
and nitter are back.
|
> > > > nozzlegear
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.
|
> > > > perching_aix
here you go: https://nitter.kareem.one
|
> hodgehog11
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.
|
> > levocardia
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.
|
> > lumost
How do you know the lean is correct? You don't bet
the two trillion dollar company on "the ai said
so"
|
> > > Almondsetat
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
|
> > > adrianN
You carefully check that the problem is
formalized correctly and then trust the Lean
machinery to check the proof.
|
> > > > zarzavat
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.
|
> > > > hodgehog11
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.
|
> > > > wiz21c
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...
|
> > > eru
> 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.
|
> > > krainboltgreene
I feel like that's exactly what's happened.
|
> bee_rider
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.
|
> bilsbie
If it is solved what are the applications of that?
What changes?
|
> > margorczynski
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.
|
> > lumost
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....
|
> > > amluto
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.
|
> > neutrinobro
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.
|
> > > yossarian88
NS absolutely does not only apply to
incompressible fluids and is far more
fundamental than you are implying.
|
> bobmarleybiceps
if there's anything that would convince that LLMS are
one of the biggest innovations ever, it would be this
:-D
|
goldenarm
@dang please can we add a [2014] to the title ?
|
> thomasahle
Yes please. For a moment I thought Terrence Tao had
scooped Anthropic.
|
MeteorMarc
See
https://www.quantamagazine.org/theory-of-fluids-enters-the
-2... if you want to know what the Navier Stokes equations
are about.
|
tacomonstrous
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.
|
> gus_massa
He has rejected papers too
https://mathstodon.xyz/@tao/113721192051328193
|
> > Sharlin
> 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!
|
> hodgehog11
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.
|
> > tacomonstrous
None of this is true.
|
> > > hodgehog11
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.
|
> > > > tacomonstrous
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.
|
> > > > > hodgehog11
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.
|
amai
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.
|
amai
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.
|
michalsustr
If you'd like to explore what the Navier-Stokes blow-up
construction looks like visually, I vibe-coded an
interactive 3D visualization based on the published result
for fun :)
Demo: https://minfx.ai/navier-stokes/
Source code:
https://github.com/minfx-ai/navier-stokes-blowup
|
immmmmm
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.
|
> amluto
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.
|
> > immmmmm
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.
|
> > immmmmm
sorry for the late answer..yes you can :
https://arxiv.org/abs/1211.1983but you might need
to understand it in the context of holographyin
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
|
> > immmmmm
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.
|
> cacio-e-pepe
Could you expand? Curious.
|
> > immmmmm
sorry for the late reply, see answer above
|
amelius
Interesting to see that they are not using the
coordinate-free representation (exterior calculus,
differential forms) that mathematical physicists prefer to
use today.
|
> auntienomen
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.
|