Navier–Stokes existence and smoothness, forced finite-time blowup
For three-dimensional incompressible Navier–Stokes flow, can smooth data and smooth forcing produce finite-time breakdown while the kinetic energy remains bounded?
Model / AI: OpenAI (unreleased), GPT-6 Astra, Codex
✓machine-checked•self-reported!disputed (attribution and provenance)
Sep 8, 2026
Forced finite-time singularity on Euclidean space and the torus
Model / AI: OpenAI (unreleased), GPT-6 Astra, Codex
✓machine-checked•self-reported
OpenAI's internal multiagent system produced a 166-page analytical construction showing that, for every positive viscosity, a smooth compactly supported force and initially stationary smooth flow on three-dimensional Euclidean space can develop unbounded velocity in finite time while retaining bounded kinetic energy; compact support gives the corresponding periodic result. OpenAI reports that roughly 10,000 agents found the result after 88 hours, Codex consolidated intermediate insights, and GPT-6 Astra completed the Lean formalization in another 17 hours. The public metadata identifies zero-sorry Lean theorems for alternatives C and D, using only Lean's three standard axioms and Comparator statements adapted from the independently authored Formal Conjectures project.
Source read 2026-09-08. Read the announcement, Theorem 1.1 and proof outline, the official Clay formulation, and the repository README, formalization metadata and Comparator instructions. The 166-page proof was not audited and the Lean project was not rebuilt.
Concurrent-work attribution and data-provenance dispute
Model / AI: OpenAI (unreleased)
!disputed (attribution and provenance)
OpenAI says it began the Millennium-problem run after hearing rumors of concurrent work by Levent Alpöge and Tristan Buckmaster, did not access their specific user data, and cannot rule out influence from de-identified training data. The concurrent result concerns forced Euler rather than this forced Navier–Stokes theorem, but Buckmaster has publicly challenged OpenAI's handling of attribution and provenance. This dispute does not by itself identify a mathematical error in the released proof.
Source read 2026-09-08. Compared OpenAI's concurrent-work statement with same-day reporting quoting Buckmaster. No adjudication or technical proof critique was available at review time.