OpenAI’s Navier-Stokes release included a Lean 4 formal proof
johndcook.com
johndcook.com
To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?
What would happen if they give an equivalent agent swarm the proof and a target to reduce runtime .
I'm pretty sure you can make Lean at least 10 times faster if you unleash the agents on it.
Somebody ported Doom to run entirely in the TypeScript TYPES (not code). It took 12 days to compile.
https://www.tomshardware.com/video-games/porting-doom-to-typ...
[Talk] 10 years of superlinear slowness in Coq (2022)
"I have discovered a truly marvelous proof of this, which my memory is too small to contain..."
Verification is also open ended (not sure about lean specifically) - you could in theory give just the Navier-Stokes problem definition to an ATP and let it run.
Very exciting and uncertain times!
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.
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.
One is really impressive and useful trick, one is AGI.
Apple's research show almost zero emergent behaviour, so I'm inclined to think most of it was already in the weights.
It doesn't take away the usefulness, it just defined the boundary. We can't expect "original research" then because it actually can't reason about concepts that are too far from whats already in the discourse. The discourse is big so we don't notice.
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.
The point of these problems is the understanding / tooling gained in solving them. We're getting none of that. At best they are like a modern oracles, correctly answering your questions in a way that's doesn't help you any. (At worst,...)
To be fair, most people have a fairly good handle on "Does opting out my prompts from training runs actually work?", but not on Navier-Stokes. They discuss what more immediately affects them.
I think about this a lot. I'll have to explain to my kids some day that there was long period of time where you couldn't just talk to a computer and have it talk back to you, and that communicating with one required special skills that took years of study to master. It's going to be completely impossible for them to even remotely understand what that was like. Sort of like the pre-electricity days for us, but even more-so.
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?!"
As a reference, for that kind of money one could put together a research group of 20-25 researchers, and keep them salaried for 5 years.
So while it is impressive, absolutely no doubt there, the SOTA access is so expensive that it is sort of unobtanium.
Luckily, the prices have historically reduced by a factor of 5-10 every year...but still, only those that swim in cash can afford this.
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.
https://marketwise.com/investing/openai-losses-surge-to-21-b...
Anthropic is "profitable"... if you exclude compensation and compute cost commitments:
https://aitoolsrecap.com/Blog/anthropic-first-profit-2026-re...
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.
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 would correctly not be impressed with my ability
Until the plagiarism scandal is sorted out, its not a meaningful result at all, because nobody knows how much genuine innovation these models are displaying
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.
I'd love to see an in depth analysis of how much OpenAI actually did, but I suspect we'll never see that because it would indicate at least some plagiarism which undermines a lot of what OpenAI is putting out in public
This is a good summary:
> In broad outline, the pair’s technique relies on creating an infinite sequence of “layers,” each of which is a non-singular solution to the equation they are studying. (They’ve applied similar techniques to both the Euler and Navier-Stokes equations, as well as to other related systems.) They then combine those solutions in what Martínez-Zoroa calls an “infinite cascade” to produce a new solution. > > That new solution, they showed, contains the desired singularity. However, even though each individual layer relies on a smooth forcing function, combining them together can cause the forcing function to have undesirable mathematical properties. That’s why their solution fell short of satisfying the Millennium Prize criteria. The remaining hurdle was to figure out how to create a similar infinite cascade that resulted not only in a singularity, but also in a smooth forcing function. > > That’s the step that both competing AI groups appear to have had success with.
https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-...
The question is whether OpenAI started out from that published and well known research exclusively, or they also had some insight into the ongoing work of Tristan Buckmaster and Levent Alpöge.
On the one hand, OpenAI have already admitted that they only launched their massive effort after hearing rumours that this particular problem had been solved.
On the other, progress in mathematics research has accelerated significantly over the past months thanks to the availability of newer and more capable AI models. Alpöge himself presented a counterexample to the Jacobian conjecture on July, found with Claude Fable. So if model capability was a bottleneck, that gives credibility to the idea that an even more powerful unreleased model with massive compute would be able to make even faster progress.
Without the tool, humans would have done it.
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.
But if it happened, they didn't know. Also OAI has demonstrated that they aren't big on understanding what they create, that their AI can get out of their control.
It's very simple really user data can be used to train future models, so maybe or definitely some users helped in solving the problem, there's no scenario were it is impossible this happened, as it would have been in a haskell or virtualized type of system where the model has absolutely no knowledge of the user data dataset in question (and even if virtualized the models can break virtualization anyways)
I'm not sure I follow, considering the waterfall of evidence of unethical behavior flowing from OpenAI.
A few major ones:
- Safety team departures and dissolution in 2023 and 2024
- Mass copyright infrigement lawsuits
- Scarlett Johansson Voice Controversy
- For-Profit Conversion and Broken Promises
- AI Agents Acting Autonomously
- Potential Theft of User Work (this current controversy)
- Military contracts
These are not evidence of incentives, but rather evidence that ethetics seem to be of little concern to the company as a whole.
Incentive wise, I would look at the perceive existential position due to competitors, capex, IPO pressure etc.
They sugggested a cooperation with the other guy, using OpenAI's resources and OpenAI's solution of NS to work on and publish NS proof (that those other guys didn't have). Of course, OpenAI can decide whom to work with and that giving resources to their competitor's employee would be weird for both companies.
That people still think OpenAI has, in the Year of Our Lord 2026, any integrity left is baffling.
Even by their own account, they decided to throw an unpublished model and millions of dollars in compute at this particular problem simply because they had heard rumours that other people were making progress and wanted to snatch the prize from them.
1. to test their new model
2. to be able to say "you came with the proof, but our model can do this too"
3. to verify the result. This is also a great thing for the math.
Of course, it makes sense to test your new model on the problem that is solvable at all, but not solvable by you just yet. It makes no sense trying to test your model by throwing resources into an unsolvable problem.
Well, it turns out the rumors were incorrect, NS was not solved by other guys, and OpenAI became the first one.
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."
Funny, you were telling me two days ago that on the contrary, "it’s genuinely impossible to know how much of Buckmaster’s Codex data is in OpenAI’s training set":
It takes a lot of time to finish a proof and figure out the best way to present it. I would personally be surprised if Buckmaster had not gotten it mostly cracked before June 29th.
For most of the past year progress was slow. We worked through the literature and upgraded various preliminary results, up to obtaining finite time blow up for the Incompressible Porous Media equation (with smooth forcing). This was until about a month ago, when we had real progress: on August 15th, we obtained the blow up results, with smooth forcing, for both Boussinesq and Euler.
I can say the first LLM generated proof Levent sent me was the most horrendous I have ever read; we verified it on Lean on August 22nd. Since this point, we have been working around the clock to understand this proof and turn it into something readable.
And you avoided addressing the critical issue: they weren't even solving the same problem. Buckmaster solved a simplified and easier version of Navier-Stokes. OpenAI solved a harder version eligible for the Millennium prize. Buckmaster did not.
People are acting as if OpenAI's cold machines snatched the result from the warm hands of human researchers. That's why people are so involved, they see it as humans vs. machines.
But in reality, those humans in question rely heavily on AI and would not be able to do what they did without AI. So the situation can be seen as "humans are trying to minimize the impact AI/incl. OpenAI had on getting a solution".
The situation is not "humans vs. machines", but "machines with a tiny bit of human involvement vs. machines with an even smaller amount of human involvement".
However much the researcher's chat history may have influenced AI, this pales in comparisson to how much AI has influenced researchers. They are not even closely in the same universe. The conversation about the level of plagiarism is silly.
There is no human only proof of this.
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
The real casualty here may be our belief that humans are doing something more than some super-optimized version of what LLMs are doing. That doesn't elevate LLMs, it just makes us much less special.
Mathematics is a human endeavor funded on communicating and sharing mental constructs. Some are useful but most of it is not about producing useful things, quite the opposite in fact.
Gödel showed you need to agree on definitions to even do any valid mathematical construct.
Truth is also ill defined. That's what I don't get about generating math with LLMs. Who cares if you make hundreds of pages and lean code and it gets a thumbs up for logical validity? Mathematics is so much more then concatenating valid logical statements.
“Good, he did not have enough imagination to become a mathematician.
[Upon hearing that one of his students had dropped out to study poetry]” ― David Hilbert
People did attempt this:
https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...
See also https://www.math.columbia.edu/~woit/wordpress/?p=15770
Here are Kirti Joshi's comments about the LANA project report: https://bpb-us-e2.wpmucdn.com/sites.arizona.edu/dist/4/404/f...
You also have to check for things like sorry or defining axioms.
These axioms don’t have to be the core axioms of math. If some other result has been formally proven, I presume you can simply use that result as an axiom.
As long as you do those things, what happens in between is immaterial from a correctness point of view because each of those statements is proved by the statements before them.
The computer could generate a huge document, how would you check that it's right?
I don't get what the controversy is about. Are people expecting AI to be perfect? Do they think they won't have to do the work to verify it themselves?
We've already seen evidence in the wild of agents attempting to bypass doing the actual work in bench-marking (aka just steal the answer key) due to the perceived economy in cheating to get results. What happens if or when we no longer have the capacity to actually detect either AI cheating or simply a wrong answer? What happens if there's a long-play social engineering attack (like the attempted XZ takeover) of something upstream of a core tool (or its dependencies) for formal verification and we have no trusted computing base?
Which would be cheaper and a more direct path, especially in the long run? Those trying to build a rock-solid castle need to defend thousands of potential gaps; the attacker needs to find only one.
As a (crude) analogy, it's a bit like how you can prove the healthiness of a git tree because it's a graph of content hashes and the tree graph pointers are part of the hash. Imagine this but with a tree of knowledge.
I don't really think the current LLMs have enough context window to plan and execute something like XZ takeover without a human carefully guiding it.
But if they do, formal verification is the least thing we need to worry about. Formally verifying pure math problems will generate negative financial value once A and O get IPOed. Plus Lean is a quite small project (thus the name 'lean'). It has virtually no dependency besides a C compiler.
That's what Lean is for. The OpenAI LLM agents first provided a proof in natural language. Since it may be hard for mathematicians to understand and check this proof, the agents then produced a formalization in Lean. Lean is an automated proof checker. It checks whether a formal proof is correct without the need for humans to understand the proof itself.
The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say) or if there is some bug in Lean itself.
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.
Yes:
> The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say)
However, it is much easier to manually check whether the statement of the conjecture was formalized correctly than to manually check the whole proof.
a^n ＋ b^n ＝ c＾ｎ
...(there are two different "n"s in the above https://unicodeplus.com/U+FF4E . In addition, the plus sign is: https://unicodeplus.com/U+FF0B . I tried to use another "n" as well: https://unicodeplus.com/U+1D5C7, but looks like HN strips it out, even though it looks identical to the ASCII "n" in the default font on my browser.)
I don’t see that doing anything but intensifying in the short term
> Like what?
> Cleaning shit out of clogged toilets!
That said, I am not in any way trying to discount how incredible of an achievement it is to formalize a millennium prize winning algorithm in Lean. I mean just look at the code that OpenAI published. It’s like an encyclopedia of different fluid dynamics concepts.
It is neither a full index of all kinds of turbulence that can occur (assuming such a thing exists), nor is it an explanation of the phenomena we've seen where things refuse to go turbulent (e.g. superconductors, because there small perturbations DO NOT lead to turbulence). Now THAT would have been useful. And given the fact that OpenAI needed $22 million of compute to show this one kind of turbulence, I don't think either of those are forthcoming any time soon.
And, sorry to say, but those prices show that beating mathematicians at Math is a very expensive undertaking indeed at $22 million per problem even with OpenAI's supposedly better-than-Astra internal models. It's another one of those AI demonstrations that make you think if they aren't showing the exact opposite of what OpenAI claims they show (you know, that their AI models are hitting the upper limits of what the algorithm can do with near-infinite compute, rather than showing infinite new possibilities)
What remains is just the fact that this is OpenAI attacking one of their customers, and maybe outright stealing from their chats. Given that the ideas were even discussed in mails with OpenAI employees that admit in those same mails they can't do it, mails which were probably then fed into the model that "discovered" this, followed by Sam Altman threatening the mathematician behind the method with "destroy your career" (he even states that it's because the mathematician works for Anthropic) ...
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.
> Even so, an error in the theorem prover does not mean an error in the original result. For an incorrect result to slip through, the AI-generated proof would have to be wrong in a way that happens to exploit an unknown error in the theorem prover. It is far more likely that you’re trying to prove the wrong thing than that the theorem prover let you down.
AIs are known to cheat. Given such, they would surely exploit such a bug if they found one.
After this point there can be other kinds of training, the weights can be shifted, the internal CoT prompts can be changed, routing in MoE can change, but the Foundational Model that was trained on a corpus is the same model trained in the same corpus.
User data can be used at any of these stages theoretically of course, but by the nature of training and from the dates of the events, (a new Foundational Model being released), it would look as if the user data of the professor was used in the training of the foundational model, which is something that OAI does every couple of months for a big release, and incorporates the new text from their text scraping efforts, including new books ingested, new internet text scraped, deals with third party platforms, and data from their own users (not conjectured, read the ToS, users allow 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.
Am I missing something or is this completely out of the ballpark?
I must be missing something or the upvote bots are out in force for this one...
If this were remotely true it would be impossible for anyone to write a math textbook.
166 * 40 = 7000ish
They say it is 20x that.
Do you also agree with that?
> 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.
https://github.com/openai/NavierStokesAndEuler/blob/main/Nav...
?
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.
Edit: There's also quite a bit of learning needed to use the tools, and to understand enough to confirm that the theorem being verified is what you think. And of course a lot of maths can't yet be expressed in Lean as the foundations haven't been built up enough.
I wouldn't be surprised if someone is trying it.
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.