Overview
- OpenAI published a 166‑page proposed proof and said about 10,000 AI agents worked in parallel for 88 hours to build and check a construction that it claims yields finite‑time singularities for the forced (C and D) formulations of 3D incompressible Navier‑Stokes.
- The company reported that parts of the argument have been formalized in the Lean proof assistant to provide machine‑checkable structure, but Lean formalization does not replace independent expert scrutiny.
- The claim addresses only cases with an external, smooth forcing term and does not prove global regularity for the unforced Navier‑Stokes equations, so it would not by itself settle the broader Millennium Problem.
- Independent peer review and further formal checking are still required and are expected to take months; the Clay Mathematics Institute continues to list Navier‑Stokes as unresolved and has not awarded any prize.
- The announcement raises procedural and integrity questions, including reported plagiarism accusations and the novel use of thousands of AI agents, and could reshape how machines assist frontier mathematics if the work is validated.