OpenAI publishes an AI-generated, Lean-formalized proposed solution to Navier–Stokes
OpenAI released a 166-page proof claiming that smooth, forced three-dimensional Navier–Stokes flow can develop unbounded velocity in finite time while retaining bounded kinetic energy—establishing alternatives C and D in the Clay problem statement. The company says an unreleased model more capable than GPT‑6 Astra found the construction through a roughly 10,000-agent effort, and it released the accompanying Lean 4 formalization; the extraordinary result still needs independent mathematical scrutiny and formal recognition.
Why it made the cut: If validated, this resolves a 90-year-old Millennium Prize problem and is direct evidence of a frontier AI system producing—and formally encoding—a major new mathematical result. The complete paper and checkable Lean repository make the claim unusually concrete, even as questions about priority and training-data provenance remain unresolved.
Paper (PDF) · Official announcement · Lean proof repository · Independent coverage (Nature)
Link to this post