---
id: "lib-2026-09-08-on-the-navier-stokes-millennium-prize-problem"
type: "library"
title: "On the Navier-Stokes Millennium Prize Problem"
lang: "EN"
org: "OpenAI"
source_type: "Paper"
date: "2026-09-08"
week: "2026-W37"
url: "https://nosov.ai/library/lib-2026-09-08-on-the-navier-stokes-millennium-prize-problem/"
original_url: "https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf"
tier: "A"
tier_name: "Strong evidence"
tier_reason: "A 166-page proof with a Lean formalization claiming to settle a Clay Millennium Prize Problem, produced by an OpenAI system; a major primary claim, but unverified, credited to no named researchers, and disputed on whether the Lean code matches the paper."
summary_basis: "full-text"
original_minutes: "900"
tags: ["capability", "formal proof"]
---

# On the Navier-Stokes Millennium Prize Problem

Tier A (Strong evidence): A 166-page proof with a Lean formalization claiming to settle a Clay Millennium Prize Problem, produced by an OpenAI system; a major primary claim, but unverified, credited to no named researchers, and disputed on whether the Lean code matches the paper.

Summary based on the full text.

## In short

"Finite Time Blowup for Navier-Stokes", credited to OpenAI as author and released on 8 September 2026, claims to resolve the Navier-Stokes existence and smoothness problem, one of the seven Clay Millennium Prize Problems. It constructs a three-dimensional incompressible fluid that starts at rest, is pushed by a smooth force confined in space and time, keeps finite energy, and still reaches unbounded velocity in finite time. The proof was found by an internal OpenAI multi-agent system and comes with a Lean formalization; I read the abstract, introduction, physical description and structure of the paper, not every technical step.

## Key numbers

- 166: pages in the proof paper, including three appendices
- (C) and (D): alternatives of the official Millennium problem statement the paper claims to establish
- 1934: year Leray proved weak solutions exist; whether they stay smooth stayed open until this claim

## What it reports

- Theorem 1.1: for every positive viscosity there is a smooth, compactly supported force and smooth velocity and pressure fields, starting from zero velocity, whose kinetic energy stays bounded while maximum velocity becomes infinite as time approaches 1.
- This establishes alternative (C) of the problem as stated by Charles Fefferman for the Clay Institute; compact support gives the periodic case on the torus, alternative (D) (Corollary 10.6).
- The singular flow is a vortex whose radial width shrinks faster than its axial length: inward spiral, axial outflow, faster spin as the core contracts.
- The background vortex alone needs a force that becomes unbounded; the construction adds oscillatory pulses whose nonlinear momentum flux cancels that singular part, so the remaining force stays smooth through the blowup time.
- The paper positions itself after Tao (2016, blowup for an averaged equation), Buckmaster and Vicol (nonuniqueness of weak solutions), Albritton, Brue and Colombo (force singular at the initial time) and Cordoba, Martinez-Zoroa and Zheng (forced Euler and hypodissipative cases).
- Structure: ten sections from leading-order flow to compact forcing and whole-space breakdown, plus appendices on radial moments, analytic profiles and the admissible stress cone.

## How they got it

The mathematics is a constructive proof: build a self-similar collapsing vortex, correct it to every order, then use oscillatory pulses to realise the required stress and keep the force smooth. According to the companion announcement, the proof was found by about 10,000 concurrent agents on an unreleased model over about 88 hours and formalized in Lean in 17 more hours.

## Limits

- At release the result had no independent peer review; the Lean formalization checks the stated theorem, and experts still need to confirm it matches the Clay formulation.
- The solution uses an external force, which the Clay statement allows under alternative (C); the unforced smooth-data case is a different question.
- No human authors are named and OpenAI says it will not claim the prize, so the usual accountability of authorship is missing.

## Why it matters for companies

If the proof holds, AI systems can now produce new, checkable results on problems that defeated specialists for decades. For companies, the practical signal is about method: many agents in parallel, structured exploration, and machine-checked verification before a person signs off. Expensive analytical work with a clear correctness test (engineering simulation, formal verification, some legal and financial checks) is where this pattern will arrive first. Results without such a check remain hard to trust at this scale.

Original: https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf