Loading page…
The company says its result was formalized in Lean after a costly agent run. Mathematicians must still assess the proof as a dispute over provenance and credit unfolds.
Listen to this story
OpenAI claims its internally developed, Lean-formalized proof shows Navier–Stokes solutions can develop singularities, but the result is not yet independently settled. The company says more than 1,000 AI agents ran for over 50 hours at a compute cost in the millions of dollars. The announcement has also triggered a priority and attribution dispute with mathematicians Tristan Buckmaster and Levent Alpöge, whose related work reportedly influenced the timing and resembles OpenAI’s approach.
OpenAI says it redirected substantial compute to Navier–Stokes on August 28 after rumors of progress at Anthropic.
The claimed result concerns possible “blow-up,” or infinite fluid speed at some points, and relates to a Clay Millennium Problem with a $1 million prize.
Buckmaster and Alpöge say their work used Claude and Codex; OpenAI denies using their prompts or proof to guide its systems.
OpenAI says an internal AI system produced a solution to the Navier-Stokes problem, a major open question about how fluids move. The company says the proof was formalized in Lean, but its announcement has been met with allegations about how the work began and who should receive credit.
The Navier-Stokes equations describe the movement of fluids including water and air. A solution would address one of seven Clay Millennium Problems, each tied to a $1 million prize. OpenAI says its proof shows the equations can sometimes “blow up,” implying infinite fluid speed at some points.
Lean is a programming language used to write formal mathematical proofs. OpenAI said it started training a model with advanced math capabilities on August 28, then assigned substantially more computing power to Navier-Stokes after rumors of progress at Anthropic.
Tristan Buckmaster and Levent Alpöge posted documents describing advances relevant to Navier-Stokes. They said they used several AI models, including Claude and Codex. Buckmaster alleged that OpenAI learned of their progress, then devoted significant resources to the problem.
Scientific American reported that OpenAI’s full Navier-Stokes proof follows a method similar to the other mathematicians’ approach and was developed over the weekend, according to Bubeck. Sorting out the differences between the proofs will likely take further examination by mathematicians.
Story updates
I spent much of the weekend talking with the team who did this work. Seb--and everyone else--acted with integrity and generosity throughout. Initially we believed the other team had also solved the problem. We wanted to collaborate and do a joint release. When we learned that they had Euler but not Navier-Stokes, we offered to let them go first, to suggest that they should be the ones to get the prize, and optionally for Tristan to be the lead author on a rewrite of the OpenAI proof. We felt it was challenging to offer the same to Levent (an Anthropic employee), who was not willing to talk or coordinate with us anyway. We were open to other solutions. We would have greatly preferred...
We congratulate Levent Alpöge and Tristan Buckmaster on their remarkable mathematical work. We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem. While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models. However, our proofs differ significantly and even the precise results proved are different in the Euler case (forced vs. unforced).
Editorial analysis
The immediate test is not simply whether a large agent swarm can produce code that Lean accepts. It is whether mathematicians can examine the underlying argument and distinguish independent discovery from overlapping lines of work. That distinction matters more as AI systems turn proofs into rapidly produced, machine-checkable artifacts. OpenAI’s claim goes beyond the earlier reported AI formalization of an established Fermat’s Last Theorem proof: it says the system found a solution to an open problem. Public technical detail on the proof and its relationship to other work would clarify both questions.
Loading discussion...
Join the conversation
Share what disclosure would make credit feel fair.
Be the first to share a perspective or an experience.
Reader comments
Newest comments first. Replies stay oldest first.