OpenAI Claims AI System Solved a Millennium Prize Problem Using 10,000 Agents

OpenAI has published a paper asserting that an unreleased artificial intelligence system successfully solved the Navier-Stokes existence and smoothness problem, one of seven Millennium Prize Problems. The research did not rely on a single monolithic language model but instead utilized a large-scale multi-agent computational architecture. OpenAI reported that up to 10,000 AI agents operated concurrently over an 88-hour computational run, sharing intermediate reasoning steps to construct a formal proof in the Lean programming language. The target of the computation, the Navier-Stokes equations, dates back to the 19th century, formulated through foundational work by French engineer Claude-Louis Navier in 1822 and Anglo-Irish physicist George Gabriel Stokes in 1851.

The Navier-Stokes smoothness question was named a Millennium Prize Problem on May 24, 2000, by the Clay Mathematics Institute, a private non-profit foundation established in 1998 in Cambridge, Massachusetts. The institute designated seven historic mathematical problems, attaching a $1 million prize to each. Before OpenAI’s announcement, only one Millennium Prize Problem had been officially solved. Russian mathematician Grigori Perelman resolved the Poincaré conjecture in papers published between 2002 and 2003. After an extensive review by the global mathematical community verified his work in 2006, Perelman declined both the $1 million prize and the Fields Medal in 2010.

Lean, an interactive theorem prover originally created by Leonardo de Moura at Microsoft Research in 2013, requires every step of a logical argument to conform strictly to defined mathematical axioms. While Lean does not assess the conceptual elegance or significance of a mathematical statement, it acts as an automated compiler that verifies whether logical steps are valid. The integration of formal proof languages allows machine learning systems to utilize reinforcement learning mechanisms grounded in objective pass-fail feedback. Because formal code and mathematical logic can be programmatically verified, models can repeatedly attempt, correct, and refine their proofs through trial and error. This feedback loop is significantly harder to replicate in subjective domains such as creative writing or policy analysis.

OpenAI stated that its proof demonstrates the existence of a mathematical breakdown, showing that the three-dimensional equations do not always preserve smooth solutions under all conditions. The company clarified that the result addresses the limits of the equations as a theoretical mathematical framework, rather than predicting physical breakdowns in real-world fluids. OpenAI researcher Dan Roberts described the multi-agent dynamic as an iterative exchange of partial insights across specialized sub-networks, comparing the process to “a bumblebee cross-pollinating across different groups and delivering different bits of information.” Sustaining thousands of active agents over nearly four days required substantial infrastructure. Noam Brown, an OpenAI research scientist known for his prior work on multi-agent game theory architectures, noted that the run was “a very expensive process,” involving an expenditure estimated in the millions of dollars. Brown added that compute costs are anticipated to decrease as system efficiency and underlying infrastructure improve.

The equations describe how viscous fluid substances—such as air, water, and oil—move under physical forces, forming the core mathematical framework for meteorological forecasting, aerodynamics, oceanography, and blood circulation modeling. Despite their widespread practical utility, mathematicians have sought for decades to determine whether the three-dimensional equations always yield smooth, infinitely differentiable solutions over time, or whether mathematical blow-ups—known as singularities—can arise where velocity or energy density becomes infinite. Real-world liquids and gases will continue to behave according to established physical laws.

OpenAI’s project comes amid intensifying efforts across industrial AI laboratories and academic centers to apply automated reasoning to open mathematical questions. OpenAI disclosed that it focused on the Navier-Stokes problem after learning that rival teams were investigating related avenues, though the company stated it “did not see any of their work through any means.” The announcement followed statements by Tristan Buckmaster, a professor of mathematics at New York University specializing in partial differential equations, who noted he had been examining related questions alongside a researcher affiliated with AI competitor Anthropic. Earlier this year, corporate research divisions reported similar milestones on minor open problems. In January, OpenAI and AI startup Harmonic announced that their systems had solved a problem originally posed by Hungarian mathematician Paul Erdős. However, several academic mathematicians observed at the time that the AI-generated approach closely resembled existing human literature.

Because of the Navier-Stokes problem’s prominence within mathematical analysis, external mathematicians and peer reviewers are now preparing an extensive review of the paper and its accompanying Lean proof script. The growing role of high-performance compute clusters in pure mathematics has raised concerns among veteran researchers. Terence Tao, a professor of mathematics at the University of California, Los Angeles, and a 2006 Fields Medalist who has advocated for formalizing proofs in Lean 4, warned about the long-term impact on mathematical training if machines resolve major questions without substantial human guidance. Tao noted that “the effort needed to solve problems is often very instructive” for human progress and conceptual understanding.