Crystal ball: OpenAI has released a paper claiming that an unreleased AI model solved the Navier-Stokes existence and smoothness problem, one of the Clay Mathematics Institute's Millennium Prize Problems. The company said the system reached its result in 88 hours by coordinating as many as 10,000 AI agents and producing a formal proof in Lean.
Mathematicians outside the company will now review the paper. If the proof holds up, it could show that AI systems can help solve some of mathematics' hardest open problems, rather than simply produce convincing-looking answers.
The Navier-Stokes equations describe how fluids move. They are used in weather forecasting, aerodynamics, and other areas of fluid mechanics. The Millennium problem asks whether the equations always yield smooth solutions in three dimensions or whether, under certain conditions, they can develop a singularity – a point at which the mathematical model breaks down.
OpenAI said its proof identifies such a breakdown. The result does not mean water or air will behave in physically impossible ways. It concerns the limits of the equations as a mathematical system, not a prediction that fluids will suddenly violate the laws of physics.
The Clay Mathematics Institute selected the Navier-Stokes question as one of seven Millennium Prize Problems in 2000. Each carries a $1 million prize, and only one, the Poincaré conjecture, has previously been solved.
OpenAI's work depended on a multi-agent setup rather than a single model attempting the problem alone. The company said groups of AI agents pursued different lines of reasoning while OpenAI researchers passed useful ideas among them. Researcher Dan Roberts described the process as "a bumblebee cross-pollinating across different groups and delivering different bits of information."
The agents used Lean, a formal proof language that checks whether every logical step follows the system's rules. Lean does not determine whether a result is important, but it can establish whether the steps in a proof are valid under a defined set of assumptions. That makes it useful for AI-generated mathematics, where a model can produce convincing but flawed reasoning in ordinary text.
The project reflects a growing effort to train models on tasks with hard pass-fail signals. In mathematics, a proof can be tested. In code, a program can be run. That gives reinforcement-learning systems a way to learn through repeated attempts, errors, and corrections. The same approach is harder to apply in areas where correctness is less clear-cut, including creative work and ethical questions.
OpenAI and other AI companies have reported progress on open mathematical problems over the past year. In January, OpenAI and Harmonic said their systems had solved an Erdős problem. Some mathematicians said the result resembled earlier human work and questioned whether the systems had produced a genuinely new approach.
The Navier-Stokes claim is more consequential because of the problem's prominence and difficulty. OpenAI said it turned its attention to the problem after learning that other researchers were pursuing related work. The company said it "did not see any of their work through any means."
The announcement came shortly after Tristan Buckmaster, a mathematics professor at New York University, said he had been investigating related questions with a mathematician who works at Anthropic, an OpenAI competitor.
The compute required for OpenAI's effort was substantial. The company said it ran up to 10,000 agents, a process that likely required millions of dollars in computing resources. OpenAI research scientist Noam Brown called it "a very expensive process," but said costs should fall as the company improves its systems and infrastructure.
For many mathematicians, the issue is larger than whether the proof holds up. Terence Tao, a professor at the University of California, Los Angeles, has warned that AI could weaken the discipline if machines begin solving major problems with limited human involvement. "The effort needed to solve problems is often very instructive," he told The New York Times.