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

121–130 of 292 posts

Re: Navier-Stokes Announcement

#121

Post by tristanj »

u1hcw9nx wrote: post #86
tristanj wrote: post #8

It's worth mentioning that OpenAI will not be eligible for the Millennium Prize for quite a while. Per the rules listed https://www.claymath.org/wp-content/uploads/2022/03/millenni... , Clay Mathematics Institute have some requirements to make this process deliberately slow. 1) The solution must be published in a qualifying outlet, i.e. a peer-reviewed math journal. Publishing on your own website (which is what OpenA…

OpenAI has stated that they will not claim the prize. https://openai.com/index/navier-stokes-solution/ While the scandal is still unraveling, it seems that OpenAI did a rush job to steal other mathematicians' thunder and finish the proof first. OpenAI released a statement that their work does not relate to the work of the other team, but it clearly does. They use the same niche smooth-forcing mechanism. Altman and Bu…

1) OpenAI and Buckmaster did not solve the same problem. Per https://x.com/IlinVasily29521/status/2097554700321329393 , here is a breakdown of who solved what.

  Tristan + Levent: 3D incompressible Euler with forcing
  OpenAI: 3D incompressible Euler without forcing
  OpenAI: Navier-Stokes with forcing
  No one: Navier-Stokes without forcing
Euler equations = Navier-Stokes without viscosity. Forcing means external force. Absence of viscosity and presence of external force make blowup easier to construct.

Tristan+Levent ticked the weakest case, OpenAI ticked the two next weakest, then the final case is unsolved. Only the last two are eligible for the Millennium Prize. The Navier-Stokes general case remains unsolved.

Navier-Stokes has an extra viscosity term compared to Euler, which makes the problem noticeably harder to find a blowup. They are not the same problem.

2) The approach both chose to use (by Luis and Diego) was published in 2023 and is included in every frontier model's training dataset. An AI model could independently choose the same route as Luis and Diego, without access to Buckmaster's work.

3) You mischaracterized OpenAI's statement. They issued a blanket denial on using Buckmaster's Codex data from after July 3.

"We can say categorically that it is impossible for Dr. Buckmaster’s Codex prompts over the last two months to have influenced the system in any way, including training. After investigating, we can say with full confidence that no user inputs past July 3rd could have influenced this system in any way.”

July 3 was the training cutoff date for the model that solved Navier-Stokes. No user data after that date influenced the model.

4) Buckmaster and Alpöge found their blow-up for 3D incompressible Euler with forcing on August 15 https://cims.nyu.edu/~tristanb/statement.pdf , over a month after the model training cutoff point. They stated they did not have real progress prior to this point.

Re: Navier-Stokes Announcement

#122

Post by JumpCrisscross »

i_no_can_eat wrote: post #120
u1hcw9nx wrote: post #71

Earlier quoted context omitted.

Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms. Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.

Can you elaborate on what constitutes a vacuous proof?

> Can you elaborate on what constitutes a vacuous proof?

Trivially, a proof that relies on a bug in Lean. Less trivially, a proof that is technically true but about something trivial and does not, in fact, prove what it claims to have proven.

Re: Navier-Stokes Announcement

#123

Post by [deleted] »

tristanj wrote: post #121
u1hcw9nx wrote: post #86

Earlier quoted context omitted.

OpenAI has stated that they will not claim the prize. https://openai.com/index/navier-stokes-solution/ While the scandal is still unraveling, it seems that OpenAI did a rush job to steal other mathematicians' thunder and finish the proof first. OpenAI released a statement that their work does not relate to the work of the other team, but it clearly does. They use the same niche smooth-forcing mechanism. Altman and Bu…

1) OpenAI and Buckmaster did not solve the same problem. Per https://x.com/IlinVasily29521/status/2097554700321329393 , here is a breakdown of who solved what. Tristan + Levent: 3D incompressible Euler with forcing OpenAI: 3D incompressible Euler without forcing OpenAI: Navier-Stokes with forcing No one: Navier-Stokes without forcing Euler equations = Navier-Stokes without viscosity. Forcing means external force. Abs…

[deleted]

Re: Navier-Stokes Announcement

#124

Post by Tanjreeve »

i_no_can_eat wrote: post #120
u1hcw9nx wrote: post #71

Earlier quoted context omitted.

Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms. Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.

Can you elaborate on what constitutes a vacuous proof?

I present to you my new theorem as follows:

If 1 == 3 then 3 == 3

----

This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.

Re: Navier-Stokes Announcement

#125

Post by setopt »

moffkalast wrote: post #109
auggierose wrote: post #11

Earlier quoted context omitted.

The Lean proof is published, you can download it. The clock definitely is ticking. Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.

Anyone can put anything on arxiv, it counts the same as printing it on tissue paper.

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 think this; when I first joined arXiv many years, there were no such checks in place, at least not that I can remember.

Re: Navier-Stokes Announcement

#126

Post by u1hcw9nx »

i_no_can_eat wrote: post #120
u1hcw9nx wrote: post #71

Earlier quoted context omitted.

Lean roof search tactics can generate vacuous proofs. They are not errors or a degenerate cases. They are completely valid, sound proof terms. Building a system that reliably detects vacuous proofs in all cases is fundamentally undecidable. It's equal to the halting problem.

Can you elaborate on what constitutes a vacuous proof?

It can happen when the proof process ends up with universal implication that holds trivially. Then you end it with something like Forall x, x is empty -> P(x).

Re: Navier-Stokes Announcement

#127

Post by thrance »

c7b wrote: post #93
eru wrote: post #59

Earlier quoted context omitted.

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.

Even funnier that it wouldn't even be the first time that happens: https://en.wikipedia.org/wiki/Grigori_Perelman

And he also gave up his trophy, which is displayed in a random corridor of a random math museum in Paris, where visitors pass by without looking, lacking most, if not all, of the context. Only because I knew the story and the man did I recognize the object for what it was.

Re: Navier-Stokes Announcement

#128

Post by raverbashing »

auggierose wrote: post #77
athrowaway3z wrote: post #65

Earlier quoted context omitted.

By peers. Peer in peer-reviewed is a logical coherent and functional definition with answers. The logical issue with 'peers' is how to bootstrap it. At that bootstrap moment you can ask "by whom?". We are several centuries past that moment. The cultural/social question you might ask today is "why (keep) them?". At which point people will naturally ask you to make a strong case for "why not them?".

> Peer in peer-reviewed is a logical coherent and functional definition with answers. What is the definition? If you tell me that, then I might be able to tell you if it is logical coherent and functional, I have a PhD in computational logic.

> I have a PhD in computational logic.

And you don't know how the peer-review system works?

Just a hunch but Claude saying your work is "PhD level" does not count

Re: Navier-Stokes Announcement

#129

Post by yen223 »

c7b wrote: post #93
eru wrote: post #59

Earlier quoted context omitted.

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.

Even funnier that it wouldn't even be the first time that happens: https://en.wikipedia.org/wiki/Grigori_Perelman

It's very likely that no one will claim any of the cash prizes, which is funny to me

Re: Navier-Stokes Announcement

#130

Post by monatron »

hyperbovine wrote: post #106
mi_lk wrote: post #45

Earlier quoted context omitted.

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

For one thing it was, I’m guessing, 100% written by actual humans. An increasingly rare phenomenon.

This was the first thing I noticed as well. It was refreshing to read.
Post reply on HN