OpenAI announced artificial intelligence solved one of the "Millennium Prize Problems"
OpenAI announced that its experimental artificial intelligence system found a solution to the problem of existence and smoothness of Navier-Stokes equations - one of the seven "Millennium Prize Problems", each of which carries a $1 million prize. The company published a mathematical proof and its formal verification in Lean.
The result concerns the Navier-Stokes equations, which describe the motion of fluids and gases and are used, among other things, in modeling air flows, designing aircraft, weather forecasting, and blood flow research. One of the fundamental mathematical problems was whether in the three-dimensional case initially smooth solutions of these equations could develop a singularity in finite time - a state in which certain mathematical quantities grow without bound.
According to OpenAI, its system proved that such a singularity can occur in finite time. The company believes that this satisfies conditions of variants "C" and "D" of the official Clay Mathematics Institute problem formulation.
About 10,000 AI agents worked on the proof
To search for a solution, OpenAI used a new internal model which, according to the company, significantly outperforms GPT-6 Astra in capabilities. This model is not yet accessible to the general public.
The system was built as a group of autonomous agents that could exchange results, work with a local copy of the internet, and execute program code. The group that found the Navier-Stokes solution consisted of about 10,000 concurrently working agents.
The work was launched on September 1, and the system obtained the required proof on September 5 - approximately after 88 hours. Another 17 hours were needed for its formalization and verification in Lean using GPT-6 Astra. During the work specifically on the Navier-Stokes problem, the agents exchanged about 2.7 million messages and generated roughly 130 billion output tokens.
According to OpenAI researcher Sebastien Bubeck, as cited by Quanta Magazine, the computational cost of the experiment amounted to several million dollars.
Mathematicians still must verify the result
Quanta Magazine notes that the formal verification of the proof in Lean gives strong grounds to consider it correct. At the same time, humans still need to ensure that the formalized statement fully corresponds to the exact mathematical problem that was supposed to be solved. If the proof withstands further scrutiny, this could become the most important mathematical result achieved by an artificial intelligence system to date.
One of the authors of the official Navier-Stokes problem formulation, Princeton University mathematician Charles Fefferman, positively assessed the appearance of the result. Meanwhile, Quanta emphasizes that the mathematical community will still need time for a detailed analysis of the new proofs.
Clay Mathematics Institute continues to classify the Navier-Stokes problem as unsolved. According to the institute's rules, before a proposed proof can be officially considered for the prize, it must be published in a qualified venue, at least two years must pass after publication, and the result must gain general recognition by the world mathematical community.
OpenAI itself stated that it does not intend to claim the $1 million prize for this result and views it primarily as a demonstration of the rapid progress of its AI systems.
The Navier-Stokes equations were formulated back in the 19th century, and the problem of smoothness of their three-dimensional solutions remained open for about 90 years. In 2000, Clay Mathematics Institute included it among the seven "Millennium Prize Problems". Until now, the only officially solved problem from this list was the Poincaré conjecture.
Based on: OpenAI, Quanta Magazine, Clay Mathematics Institute