Overview
- OpenAI announced that an internal, unreleased model produced an analytic proof showing a smooth, stationary fluid can develop a finite‑time singularity for cases C and D of the Navier–Stokes problem and supplied a Lean formalization of that proof.
- The formalization was reported to be checked by GPT‑6 Astra in about 17 hours, giving machine‑verified support to the AI‑generated argument but not replacing human peer review and community vetting.
- Independent researchers who recently published related fluid results have questioned whether OpenAI used their unpublished ideas or research stored in Codex, prompting public dispute over research provenance.
- OpenAI denied targeted access to specific user data while saying it cannot rule out contributions from anonymized user data used to improve its models, and it also said it will not seek the Clay Mathematics Institute prize for this result.
- The project used a large, costly AI workflow reported to involve roughly 10,000 collaborating agents over about 88 hours with estimated compute costs in the tens of millions of dollars, and formal adjudication by mathematicians and the Clay Institute remains under way.