Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Navier-Stokes Announcement

claymath.org

Post reply on HN
Print view View original

261–270 of 292 posts

Re: Navier-Stokes Announcement

#261

Post by rawland »

mpardalos wrote: post #240
soerxpso wrote: post #223

Earlier quoted context omitted.

It's formalized in Lean, isn't it? Do you also rely on a community of C++ experts to tell you whether a program compiles or not?

Yes, but there's still the possibility that it's either exploiting a bug in Lean, or that the theorem statement is not set up correctly (i.e. it's actually proved a different theorem). My understanding is that the theorem statement is quite simple, so i guess the latter is not very likely, but the former is very much a possibility in a proof this large, and it will take some human eyeballs to go over it before convin…

I ran the proof 3 days ago.

They do a Comparator Challenge to validate that they actually solved the correct theorem from the result, which they copied from Google/DeepMind: https://github.com/openai/NavierStokesAndEuler/blob/f9e8bc5b... - this is valid for both Euler and NS. Also, they validated with an external kernel from the Lean Kernel Arena. That way bugs in the Lean kernels were found in the past already, iirc.

Having said that, I strongly believe a positive result with the challenge above is the reason why they published it. I highly doubt anybody at OpenAI (or anywhere else) fully gets the proof after such a short time since publishing. This is also what Terry Tao criticized the most in my opinion.

Independent of the remaining drama [0], from my point of view, the proof is correct and an achievement.

[0]: https://news.ycombinator.com/item?id=49661928 - I am pretty much on the critical side, however, one can not ignore that it is an achievement. Esp. the unforced result.

Re: Navier-Stokes Announcement

#262

Post by pama »

Paracompact wrote: post #212
pama wrote: post #183

Earlier quoted context omitted.

Perhaps you did not understand the Fermat theorem proof announcement/repo or the link. The 13 million lines did not use any external, possibly not honest libraries, as the proof eventually only used the fundamental axioms. So for the Fermat theorem formalization, no open open questions remain.

https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke... Do you believe no open questions remain as to the truth of the Collatz conjecture?

Not sure what you mean. Here is what happened in that case: https://news.ycombinator.com/item?id=49137060#49140177

Re: Navier-Stokes Announcement

#263

Post by famouswaffles »

HarHarVeryFunny wrote: post #258
famouswaffles wrote: post #233

Earlier quoted context omitted.

>Most research mathematicians are employed as academics, and it's hard to see universities replacing teaching staff with AI even if that were possible. If universities come to only need research mathematicians for teaching ability, then it would still gut the profession. You would presumably need far fewer of them for their research ability, and hopefully hire more people who can actually teach. It's strange that you…

> You would presumably need far fewer of them for their research ability, and hopefully hire more people who can actually teach I suppose you are suggesting that research mathematicians are either over-qualified mathematically and/or under-qualified in ability to teach, but it seems pretty clear that universities prefer to hire domain experts whose reputations and long publication lists attract students and raise the…

>I suppose you are suggesting that research mathematicians are either over-qualified mathematically and/or under-qualified in ability to teach, but it seems pretty clear that universities prefer to hire domain experts whose reputations and long publication lists attract students and raise the perceived academic standards of the school.

I'm saying there's little correlation in how brilliant a researcher you are and your teaching abilities. Yes universities optimize for the former. That's not necessarily a good thing for students even if it increases the prestige for the university. If there's some future where research and teaching are decoupled, I don't expect things to remain the same, but who knows I guess.

>I was pointing out that giving a free research tool to mathematicians would likely be better received, and receive better press, than doing something that most top-tier mathematicians are opposed to.

At least currently, it's not possible for this to be a free tool. Both OpenAI and Anthropic have discounts for Universities/Education for such use cases as far as I'm aware.

>As far as the AI companies acting in slimy fashion goes, the most slimy behavior of all is to strongly believe you are doing something that will kill people and cause massive societal disruption ... and still keep doing it.

This is pretty bad, but I wouldn't call it slimy. And it's no longer up to any one person or company anymore.

Re: Navier-Stokes Announcement

#264

Post by teovall »

mi_lk wrote: post #45
tristanj wrote: post #3

Smart move by them for waiting until the drama died down before making a completely neutral statement. The statement is so sterile they don't even mention who solved it. The word "OpenAI" doesn't appear at all.

I really like this style of writing for some reason. Not sure how to put it but it’s a rare combination of a vague post and confidence

The bureaucratic voice

Re: Navier-Stokes Announcement

#265

Post by groundzeros2015 »

Stevvo wrote: post #190
andsoitis wrote: post #66

Proving things without comprehending them is a threat to intellectual work.

No, it is not. Proving things without comprehending them built much of human civilization. Comprehension is a relatively new fad that came along in the 17th century with the scientific method.

The world began in 1600

Re: Navier-Stokes Announcement

#266

Post by zeroimpl »

stbede wrote: post #253

What I'm not seeing reported on much is if the result reveals any new techniques or ideas that advance mathematics - which is what we usually hear is the reason to work on these problems. Or does the resolution of NS just add a fact to the list without any new understanding.

My understanding is that it’s proof by counterexample, so the main thing to study would be the implications of the counterexample. The technique used to find it sounds like a lot of brute force. But I’m not a mathematician, and maybe the AI used some clever techniques to narrow in on it.

Re: Navier-Stokes Announcement

#267

Post by cryptonector »

DrBenCarson wrote: post #4

> Today, CMI shares in the excitement of the global mathematical community as we contemplate the announcement that the Navier-Stokes problem has apparently been settled. We hope to see waves of new human understanding unleashed as the innovations behind this work are analysed and interrogated. That “apparently” feels load-bearing

> load-bearing

Apart from LLMs, who speaks this way?

Re: Navier-Stokes Announcement

#268

Post by willsmith72 »

cryptonector wrote: post #267
DrBenCarson wrote: post #4

> Today, CMI shares in the excitement of the global mathematical community as we contemplate the announcement that the Navier-Stokes problem has apparently been settled. We hope to see waves of new human understanding unleashed as the innovations behind this work are analysed and interrogated. That “apparently” feels load-bearing

> load-bearing Apart from LLMs, who speaks this way?

structural engineers?

Re: Navier-Stokes Announcement

#269

Post by aarstid »

HotHotLava wrote: post #252
gerdesj wrote: post #244

Earlier quoted context omitted.

"It's formalized in Lean, isn't it?" If that's the current burden of proof required in your world for maths then that's fine! 't'ain't in my world: I want to see peer reviewed and published. Surely that's not too much to ask. Its not perfect but generally works rather well for maths. I'm not a sodding programmer so please don't assume everyone here is one. I'm not a mathematician either but I do have standards: Your…

In what world is peer review a higher standard than formal verification in Lean? Not in the world mathematicians have been living in for the past decades at least. Nearly all big theorems that have been formalized so far had been published beforehand, and it was usually regarded as a step up in rigor. Wrong results get published in peer reviewed journals all the time.

I find it really strange the way “peer-reviewed” is used by the general public as some gold standard of truth. As a former academic who has been there, the process is extremely arbitrary and variable. Are people aware that the “peer” refers not to a community or a committee, but literally to one random guy or maybe a couple with zero accreditation? And that the journal editor can do whatever they want with this peer’s “review” including completely ignoring it?

Re: Navier-Stokes Announcement

#270

Post by AnimalMuppet »

Razengan wrote: post #222
AnimalMuppet wrote: post #194

Earlier quoted context omitted.

Depends. What replaces it? Does that replacement do better at keeping false claims out, or worse? Does it do better at letting true claims through, or worse?

One thing's for certain: True and false should not depend on convincing people.

Real true or false - which I define as correspondence (or lack thereof) with reality - does not depend on convincing people. Reality does not change when people become convinced; ideas correspond to reality whether people are convinced or not.

But perceived truth and falsehood depend on convincing people - either convincing them one by one, or else convincing some gatekeeper, whose word will convince those who accept the gatekeeper.

Post reply on HN