OpenAI changed Navier-Stokes press release and Lean4 code on GH

9 points·rawland··2 comments

As of Sept, 11th: https://openai.com/index/navier-stokes-solution/

Compare to https://web.archive.org/web/20260908235305/https://openai.com/index/navier-stokes-solution/

Also, see GitHub - git history: https://github.com/openai/NavierStokesAndEuler

So, what are the implications of this?

The wording changed such that oai point out that the proof went a different ("unforced") path compared to the one by Tristan Buckmaster and Levent Alpöge and claimed that they didn't "consume" their work in any way.

Given the track-record of sama's trustworthiness and their agents breaking constantly into other systems, this statement is untrustworthy and looks like they are covering tracks.

Considering the different path, I can't confirm that. To my understanding and run through the Lean4 proof (3 days ago) that claim is not true. The 3D Euler case is unforced in oai's work. The Navier-Stokes section is forced. However, Tristan Buckmaster in his https://cims.nyu.edu/~tristanb/statement.pdf implied work on unforced Euler. "We do not yet have anything resembling a presentable writeup. I mention it because it is suggestive of a path to unforced Euler." [sic]

Further it was criticized that major ground work on that proof was missing in oai's paper. Like Chen-Hou, Córdoba, and Elgindi are nowhere to be found in the references.

Reply on news.ycombinator.com