On the Navier–Stokes Millennium Prize Problem • Hacker News Board

Re: On the Navier–Stokes Millennium Prize Problem

#821

Post by lukewarm707 » Wed, Sep 09, 2026, 12:37 AM UTC

jampekka wrote: post #447

tiborsaas wrote: post #16

> We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean. WOW?

> WOW This. I do dislike the AI oligarchs as much as the next person, but I do find the thread full of complaining a bit depressing still. If the result holds (and it looks it does), this may be one of the, if not the, biggest things to happen in computing to date. A lot bigger than e.g. Deep Blue beating Kasparov in chess or AlphaGo beating Sedol in Go.

assume all you want is the proof. now you have the proof. did openai make the world a better place, by turning on 300b tokens in 7 days and bulldozing members of the community who were also working on the problem? just to undercut a rival?

what would have happened if they didn't do this? they could have done things the right way. we could celebrate this achievement.

perhaps they could have taken just a few weeks, even, to work out something with buckmaster and apoge.

i am very concerned that this is a glimpse of things to come. a malign elite with powerful ai, who will turn the sublime of technology into barbarity, violence and human oppression.

if sam altman has destroyed openai's public benefit corp with lesser tools why would he aid humanity with even greater power?

Re: On the Navier–Stokes Millennium Prize Problem

#822

Post by dataflow » Wed, Sep 09, 2026, 12:39 AM UTC

Is blockchain going to finally be the solution to something?

I'm only half joking. Should researchers perhaps put hashes of their attempts on a public blockchain tied to their own public keys, verify their claims asynchronously, and then whoever reveals the first believable attempt gets the credit?

I know some people started doing this years ago but now it might need to become standard practice.

Re: On the Navier–Stokes Millennium Prize Problem

#823

Post by throwaway81ag81 » Wed, Sep 09, 2026, 12:39 AM UTC

jampekka wrote: post #447

tiborsaas wrote: post #16

> We’re sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We’re sharing both a writeup of the proof and a formalization in Lean. WOW?

> WOW This. I do dislike the AI oligarchs as much as the next person, but I do find the thread full of complaining a bit depressing still. If the result holds (and it looks it does), this may be one of the, if not the, biggest things to happen in computing to date. A lot bigger than e.g. Deep Blue beating Kasparov in chess or AlphaGo beating Sedol in Go.

I dislike both AI oligarchs as much as people who do this kind of deflection.

People are not complaining about problems being solved or advancement in technology. They are complaining about terrible people doing terrible things.

Re: On the Navier–Stokes Millennium Prize Problem

#824

Post by monk_grilla » Wed, Sep 09, 2026, 12:43 AM UTC

aeve890 wrote: post #566

intenex wrote: post #440

I think this is clear evidence that AI models are now at the far frontier of mathematics innovation and discovery and exceed human limits. This specific problem having had a $1 million bounty on its head and still remaining unsolved for 26 years after the bounty was placed is pretty clear evidence that many of the world's best human mathematicians would have solved this problem if they could have, and none were able…

>If anyone has counterpoints to this I'd love to hear them! Sure. A proof without an unknown amount of human steering (and/or stolen research) would be an unquestionable achievement. To this day there's zero (0) evidence of any result by an LLM alone (maybe I'm wrong). If I just prompt ChatGPT right now with "give me a proof of the Riemann Hypothesis" and this thing delivers, I'm sold. But anything close to "yeah Cha…

> I'd expect idk, a unified theory on fundamental physics, or a novel engineering solution for material science and nuclear fusion, or at least improve itself to not need a bazillion GPUs to emulate a 20 watts wetware.

I think the counterpoint here is simply to look at what was being achieved with LLMs one year ago versus today, and extrapolate that trend. Sure, there may not be examples of what you've asked for yet, but Astra is literally a couple of months old, the model that solved Navier-Stokes is less than two weeks old. It appears that we're seeing the hockey stick that only the most bullish thought was possible.

Re: On the Navier–Stokes Millennium Prize Problem

#825

Post by sebzim4500 » Wed, Sep 09, 2026, 12:45 AM UTC

cool_dude85 wrote: post #273

blake__dev wrote: post #238

Earlier quoted context omitted.

Yeah I'm surprised they posted a chart, you would think they would keep specifics like that hidden until they're closer to launch

The chart is as non-specific as could be. It improved in some very vague metric by some amount at different (increasing) levels of training.

Isn't the y axis just what portion of the open problems it could solve? The axis is unlabelled though, I'll give you that

Re: On the Navier–Stokes Millennium Prize Problem

#826

Post by tim-kt » Wed, Sep 09, 2026, 12:47 AM UTC

cv5005 wrote: post #381

nater5000 wrote: post #229

Earlier quoted context omitted.

>there's still the problem of does this logical result actually prove the initial question that was asked? In math, the question being asked is the validity of a logical statement. That is, there is some rigorous, logical statement which may or may not be true (or even provable, etc.), and the question is whether or not it is actually true or false (or even provable, etc.). Having a proof, fundamentally, means you ha…

I was thinking something along the lines of making a mistake when inputing the initial statement, like you wanted to prove that '2 is even' but what you actually stated was that '3 is odd'. Of course in this simple example it's obvious, but my assumption was that these machine generated lean proofs are millions of lines of code and who knows what they actually say..

You're correct that nobody really understands what these huge Lean proofs actually say. However, the initial statement, even for Navier-Stokes, is not very long [0]. Still, you are also right that sometimes the problem statement can be wrong but it is highly unlikely here.

[0] https://github.com/openai/NavierStokesAndEuler/blob/main/Com...

Re: On the Navier–Stokes Millennium Prize Problem

#827

Post by cman1444 » Wed, Sep 09, 2026, 12:47 AM UTC

HarHarVeryFunny wrote: post #581

sobellian wrote: post #549

Earlier quoted context omitted.

Even under your interpretation, OAI pushed a button and solved NS. Yes, that is very impressive. Are you kidding me? Imagine building an automated system that can solve NS.

That's not my interpretation - that is literally what OpenAI say in that press release.

Even if true, I don't see why this is an issue. Are they not allowed to work on problems others are working on? Did Anthropic get first dibs on this problem? Competition is good. And I don't exactly have tons of sympathy when the other side is just a leading AI lab. It's not like it's some scholar who dedicated his life to this problem.

Re: On the Navier–Stokes Millennium Prize Problem

#828

Post by sebzim4500 » Wed, Sep 09, 2026, 12:49 AM UTC

preommr wrote: post #786

danielmarkbruce wrote: post #591

Earlier quoted context omitted.

With Lean, math has become a really well suited problem for LLMs. We will likely see large gains for many years from here, just doing more and more rlvr, like continuously, non stop. No need to train from scratch. It really doesn't speak to the general intelligence of models though. It does speak to how good these things can become when a problem space has verifiable rewards, especially when you can verify one step a…

It's crazy how deep Microsoft's bench is (Lean was started there, vscode is another), for everything not directly related to the the ai models (hell, even github for data). So interesting how everything played out, I remember in the early days when MS came out with the partnership with OpenAI it seemed like they were playing 5d chess and were poised to win big. And it all just fizzled out. Second biggest fumble after…

Don't they own a large portion of OpenAI? Things could be worse

Re: On the Navier–Stokes Millennium Prize Problem

#829

Post by throwaway81ag81 » Wed, Sep 09, 2026, 12:50 AM UTC

Eridrus wrote: post #466

jampekka wrote: post #447

Earlier quoted context omitted.

> WOW This. I do dislike the AI oligarchs as much as the next person, but I do find the thread full of complaining a bit depressing still. If the result holds (and it looks it does), this may be one of the, if not the, biggest things to happen in computing to date. A lot bigger than e.g. Deep Blue beating Kasparov in chess or AlphaGo beating Sedol in Go.

Seeing mathematicians such as Terry Tao being unhappy with open problems being solved makes me sort of question the usefulness of any of this pure mathematics. If we're not happy that the problems are being solved, why care about this field at all?

Where did you even read that Tao is unhappy with “open problems being solved”? There was no indication of that in his Bluesky thread.

Why would you go out of your way to make a case of something being not useful when, ironically, so much advancement in human history has come from the discipline?

Your motive is more worrying than your straw man argument.

Re: On the Navier–Stokes Millennium Prize Problem

#830

Post by samrus » Wed, Sep 09, 2026, 12:51 AM UTC

piloto_ciego wrote: post #815

noir_lord wrote: post #781

Earlier quoted context omitted.

Recursive self improvement of their upcoming IPO value maybe. They are fluffy PR pieces otherwise.

How can you possible say this sort of thing in context of what looks like a millenium prize being solved. I swear there's nobody blinder than those who won't see.

You have to look at the incentives