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

What would happen if they give an equivalent agent swarm the proof and a target to reduce runtime .

People are grasping at straws it seems to dismiss the power of this new model they may have. Hate OpenAI for any reason you want, but denying the capabilities of models has been a losing game for the past 5 years.

Isn't that how research works? Everything is built on the shoulders of the ones that came before, attribution is a real problem (I don't know if OpenAI released a paper citing the previous contributions, I'm assuming not but they should), but using previous maths to prove new maths shouldn't be controversial

There is no human only proof of this.

This is the timeline:

On June 29, Buckmaster opted out of 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

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

It's also true however that I haven't seen a single write up trying to discern what did more of the work in those AI chats - the prompts or the responses - bubble to the surface, also since we don't have access to them.

For example, if I prompt Codex with "Make me a website about strawberry cake" and nothing else, and OpenAI announces they have the best strawberry cake minutes before I launch, I'm not sure they plagiarized anything.

We just don't know if this is quibbling over "who prompted first" or if the researchers came up with anything strikingly original by themselves.

At market prices. All the estimates I've seen are based on OpenAI API costs. It doesn't mean that's what they paid, or how they paid for it.

But yes, the surprising willingness of humans to solve hard problems in exchange for food and board is underrated.

If you tried to raise 25M to have 20 researchers on a salary for 5 years solving a specific math problem only academics care about, you probably wouldn't get much interest, or you would be able to solve 1 or 2 problems.

If however you promise that the money will go towards a technique that would allow to solve 10 thousand different math problems, and that costs will go down in the future, then you can raise much more than 25M.

And that's before we get into the whole 'salt the earth' way they ended up solving it. For a short period of time it may well have been the least valuable proof in mathematics yet. In their haste it's dubious they actually read the proof, and I don't think anyone has had time yet to truly understand it (the original researchers are best placed to do so, but are they even willing?).

So now it is solved, the proof has been independently verified and nobody has an incentive to investigate further. OpenAI has spent millions to uncover 1 bit of information that so far nobody has learned anything from, and they've demotivated all the people who wanted to.

Even with many of our best minds working on it for nearly a century, it _just_ now was solved just as AI became very good at math. Doesn't seem too farfetched to me to assume that AI played an outsized role in solving it. If it was really just a matter of "stitching things together" to solve it (granted, this is a very reductive way to look at it) , I suspect we would've solved this a while ago.

It might also be that they won't even ask or wonder, similar to how most don't really do with pre-machining skills.

Or it could be like our "How did they build the Great Pyramid?!"

You also have to check for things like sorry or defining axioms.

The computer could generate a huge document, how would you check that it's right?

It's unlikely to be the case here as instead of hillclimbing a Lean proof for validity it appears the proof was first constructed in English before being translated to Lean, which intuitively (hopefully) reduces the chance it exploits a bug.

I don't know whether I'm just paying more attention this time, but I found the discussion on this be a perpetual game of telephone, where people get small, but important, details just completely wrong.

The person "threatening" the mathematician was _sama_; and the person who the threats were being directed _to_ is not an Anthropic employee!

(And the person who _did_ say these things have come out and explained what they meant; whether you believe them is up to you.)

I don't know if this is worse because everyone is so tired/angry at the big AI Labs; whether something about people's reading comprehension and attention span has gotten markedly worse or if this is just selection bias on my end; but it's _very weird_ to keep seeing this.

See, e.g., Barak Ravid regularly reporting in Axios the impending ceasefire negotiation progress in the Iran War, which largely have failed to come to pass.

166 * 40 = 7000ish

They say it is 20x that.

Do you also agree with that?

But my advice, in this weird new world we’re living in, is not to dismiss claims like this as PR fluff. Just about every time I’ve been incredulous of some ridiculous new AI advance and I think it’s BS, it turns out I’m the one that hasn’t caught up with the exponential rate of advancements.