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

OpenAI’s Navier-Stokes release included a Lean 4 formal proof

johndcook.com

Post reply on HN
Print view View original

131–139 of 139 posts

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#131

Post by jasonfarnon »

entrope wrote: post #101
wewewedxfgdf wrote: post #59

"no one is talking about" - classic AI tell.

Drawing a strong conclusion from one shaky data point - classic human tell? I've been reading John D. Cook for years (maybe decades? "The Endeavour" is one of my oldest bookmarks), and this post was no more written by AI than his oldest posts.

yeah, there were some posts of his that always got top hit on certain google searches in the days before stackexchange. And this sounds like typical John D Cook. All these people claim to identify some "tells" and whenever a study is done people are horrible at distinguishing AI vs non-AI prose.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#132

Post by oursland »

hatthew wrote: post #104
alberto-m wrote: post #86

The other part no one is talking about is the applicability. Navier-Stokes is the most “physical” of the Millennium Problems. Is the exploding solution a mathematical curiosity, just like the Banach-Tarski Paradox does not allow me to double my RAM by cutting my memory modules in five pieces and mounting them back appropriately? Or does it have application in the real world, pointing to hitherto unknown resonance phe…

My understanding of the result that was found is that the blowup doesn't happen in the real world, and only happens in an NS simulation. The bottom line is that NS is insufficient to model the real world, because in this case the real world is more stable than the model. [Take this with a grain of salt, I barely knew of NS before a couple days ago]

I'm not too familiar with the exact problem as I only became aware of it due to this drama, but I think you're correct. That said, another commenter noted that it may also be one of the Millennium Problems with the least application. We already know "all models are wrong, but some models are useful" (George E. P. Box), the fact that this holds for Navier-Stokes is not a surprise.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#133

Post by jasonfarnon »

khazhoux wrote: post #75

The part that most stood out to me was where Sama said, “we read last week about people trying to solve Millenium problems and so gave it a shot.” One week of work on a whim gives us a math breakthrough. Crazy.

That sounds like PR nonsense to me. These companies have had teams of mathematicians for at least 1.5 years looking to make headlines, and they didn't bother trying all 10 millennium problems? Yeah right.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#134

Post by tomjakubowski »

adverbly wrote: post #96
Paracompact wrote: post #64

Earlier quoted context omitted.

By formalizing, they mean within a proof assistant like Lean or Rocq, not simply in prose in a textbook. I can attest, 40 hours per page is by no means an overestimate for this sort of work.

Can you also attest to the scaling factor they suggest and that it doesn't have any scaling time benefits? 166 * 40 = 7000ish They say it is 20x that. Do you also agree with that?

The scale factor comes from this number in the article, seemingly an intuited estimate:

> Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook.

That would suggest formalizing a 10-page research article might take 200 weeks (assuming 40h/wk) of effort, or about four years. Not a mathematician, I have no idea if that's in the ballpark.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#136

Post by tristanj »

20k wrote: post #35
boshalfoshal wrote: post #5

People seem to be talking about anything except the actual results with this particular announcement. Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time. I'd be curious to see if the new model can also do more direct proofs/inductive proofs.

Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people wo…

It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved.

This is the timeline:

On June 29, Buckmaster disabled model training, and stopped allowing his chats to be used as training data with OpenAI https://mastodon.social/@tristanbuckmaster/11723341370570119...

On August 15, Buckmaster and Alpöge found their blow-up for 3D incompressible Euler with forcing https://cims.nyu.edu/~tristanb/statement.pdf

In late August, OpenAI completed a pretrain of its latest internal model. A model derived from this pretrain, built after August 28, found a solution to 3D incompressible Euler without forcing and Navier-Stokes with forcing. https://openai.com/index/navier-stokes-solution/

To explain who solved what (I copied from here: https://x.com/IlinVasily29521/status/2097554700321329393 )

  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.

Buckmaster disabled model training long before the August 15 breakthrough results, so these chats were not used as training data for OpenAI's model which solved Navier-Stokes.

Additionally, Tristan and Levent only solved the easiest version of the problem and did not have the key insights to solve the harder versions of the problem required for the Millennium Prize.

And OpenAI directly addressed these plagiarism claims, and called them impossible: https://www.nytimes.com/2026/09/10/science/tristan-buckmaste...

"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"

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#137

Post by jesuslop »

tecleandor wrote: post #58
3m4r wrote: post #48

Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools? We've already seen evidence in the wild of agents attempting…

Well that happened already without AI to Mochizuki with his proposed solution to the abc conjecture.

I know it adds no value, but cannot resist telling I have thought that exact same analogy.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#138

Post by ggoo »

tristanj wrote: post #136
20k wrote: post #35

Earlier quoted context omitted.

Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people wo…

It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved. This is the timeline: On June 29, Buckmaster disabled model training, and stopped allowing his chats to be used as training data with OpenAI https://mastodon.social/@tristanbuckmaster/11723341370570119... On…

I’m unsure or not if this is true but I did see some people saying that that checkbox when off only anonymizes your data, but it still may be trained on. Someone correct me if I am wrong

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#139

Post by alasano »

Ohentis wrote: post #100
lordnacho wrote: post #14

How do you know that it's formalizing what you think it's formalizing? If your Lean 4 has a bug, won't you be proving something other than what you thought?

The only places you can really have a bug are your theorum statement, your axioms, your environment (hardware, operating system, etc.), and the lean kernel itself. In most situations you don't have the AI control any of these. The only risk is the AI discovering and exploiting a bug in one of these systems instead of actually providing what you want to prove.

The only risk is pretty much the greatest risk, from what we've seen recently at least.
Post reply on HN