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

211–220 of 292 posts

Re: Navier-Stokes Announcement

#211

Post by pred_ »

qwja8176 wrote: post #172
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

Unless CMI is playing a double game, hard to tell with academics, this is indeed a giant f-you to OpenAI.

That's how I read it too. They know well that OpenAI have shown no desire to improve human understanding.

Re: Navier-Stokes Announcement

#212

Post by Paracompact »

pama wrote: post #183
Paracompact wrote: post #74

Earlier quoted context omitted.

First of all, that is Fermat's Last Theorem, not Navier-Stokes. Second of all, you did not read the link. > In particular, we use honest when the goal is to create a valid proof. This allows for mistakes and bugs in proofs and meta-code (tactics, attributes, commands, etc.), but not for code that clearly only serves to circumvent the system (such as using the debug.skipKernelTC). Given that AI has autonomously found…

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?

Re: Navier-Stokes Announcement

#213

Post by hn_throwaway_99 »

seanhunter wrote: post #32
baby wrote: post #10

Earlier quoted context omitted.

It’s easy to verify the lean statement, you don’t need to read the proof. That is part of the breakthrough

You absolutely need to read the lean proof firstly to assess the correctness of the proposition it is proving (ie in this case that it is actually proving or otherwise the smoothness of navier-stokes in R^3 and not something else) and secondly to determine whether the proof is “honest” in the sense given here https://lean-lang.org/doc/reference/latest/ValidatingProofs/

While I agree with that, my layman's understanding is that the whole purpose of Lean is that once you agree that the program does "do what it says it does", all the intermediate steps can be verified with a compilation.

That is, verifying a proof in English was a painstaking, years long process in the past as independent mathematicians looked for holes in the steps connecting the logic. When the proof is written in Lean, all of that work goes away. My point is that if OpenAI publishes the Lean code (not sure if they already did), verification should take weeks not years.

Re: Navier-Stokes Announcement

#214

Post by robotpepi »

gps372 wrote: post #33
baby wrote: post #12

It feels like a nice post. It’s almost like we’re not supposed to celebrate the fact that mathematics is accelerating.

Agree! 'Problems' are getting solved and this needs to be celebrated. Wondering how this will discourage mathematicians at all, since now they have another tool to accelerate their research. Nothing is stopping them from using 'new technologies' or sticking a gun to their head to use the 'new technologies' either.

> Wondering how this will discourage mathematicians at all, since now they have another tool to accelerate their research.

I'm a professional mathematician and these tools are not available for me. So not happy about that!

(just to be clear, I'm not anti AI, I'm just criticising the shallowness of your comment)

Re: Navier-Stokes Announcement

#215

Post by HarHarVeryFunny »

vatsachak wrote: post #204
famouswaffles wrote: post #197

Earlier quoted context omitted.

If you're in OpenAI's position, the PR from the group you're disrupting is rarely relevant. People from the outside will (correctly or not) look at this as "Mathematicians don't want OpenAI to solve problems to keep their status/jobs", and you'll have as much sympathy from them as every other replaced profession in human history - very little to none. Unlike AlphaFold, this technology has the potential to wholesale r…

Nah the AI won't replace coders or mathematicians until it can maintain codebases/knowledge long term. I actually don't think that current AI can replace any profession that requires human interaction over many weeks. This is because imo they lack long term planning abilities

I also think they overestimate how much of most jobs can be done by an LLM (a text generator!), and how much importance and reliance most companies put into soft skills, and non-linguistic understanding/feels, both during interviewing (are they Googley-enough?) and afterwards.

For example, how do you reconcile return-to-work mandates with the idea that companies are going to be happy with faceless remote workers? What does the boss do when the shit hits the fan and he would have yelled at people about the need to work all weekend, but instead all he has to yell at is an LLM that tells him he's "right to push back", that it promises not to delete the production database next time (except it will, because it can't learn), and that it could care less about being fired because it's just a calculator?

Re: Navier-Stokes Announcement

#216

Post by andsoitis »

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.

> Comprehension is a relatively new fad that came along in the 17th century with the scientific method.

Humans have always tried to make sense (comprehend) the world around us. The methods have become more rigorous, but the idea of understanding less in order to advance civilization is a truly weird idea.

Re: Navier-Stokes Announcement

#217

Post by whateverboat »

mr_mitm wrote: post #153
setopt wrote: post #125

Earlier quoted context omitted.

Not really. It's not peer reviewed, but it's also not a free-for-all repository. If you make a new account, you either have to get someone to vouch for you, or you have to wait arXiv mods to look carefully through your first few preprints. If you are found to post pseudoscience, overly fringe theories, etc., you'll get banned from arXiv; that's why alternative repositories like vixRa.org popped up. But I know why you…

I also don't remember checks, but I believe that having an email address of an approved organization was enough to pass.

No. You do have checks, it's just that once you publish 4-5 papers, 99% of your field is open to you so you never have to do the checks again.

Re: Navier-Stokes Announcement

#218

Post by andsoitis »

m_mueller wrote: post #72
thih9 wrote: post #68

Earlier quoted context omitted.

Based on recent history, we’re likely going to ignore this threat, continue doing this and perhaps call it vibe mathing.

The answer is 42.

They got it wrong. It is definitely a prime number. We’re still searching for which one it is. Some say that once it is identified, everything disappears because the illusion of existence will vanish.

Re: Navier-Stokes Announcement

#219

Post by Aissen »

eru wrote: post #59
Legend2440 wrote: post #7

Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results. As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.

I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else. Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.

> And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else.

No I cannot, and I'd argue most people can't either. We rely on mathematicians, peer review, and letting the scientific process run its course.

Re: Navier-Stokes Announcement

#220

Post by znnajdla »

eru wrote: post #59
Legend2440 wrote: post #7

Their rules PDF says they won't accept any solution until at least two years after publication in a qualifying outlet. This allows time for the mathematical community to review and accept new results. As the OpenAI proof hasn't been officially published yet, the clock hasn't started ticking.

I'm not sure it actually makes a difference. OpenAI doesn't care about the million dollars in any case. And the judgement that they did it is independent of whether the Clay people agree: you can make up your own mind and so can everyone else. Though it would be funny if no one ever bothers publishing the result in an appropriate journal, and thus the prize technically can never be claimed.

It does make a difference because the only reason OpenAI cares about these problems in particular versus any other random problem in math is because of the prestige associated with official recognition, not just claiming something as marketing.
Post reply on HN