Particle.news
Download on the App Store

OpenAI Publishes Claimed Navier–Stokes Proof and Machine‑Checkable Formalization

The release has raised urgent questions about credit, training‑data use and how fast commercial AI should disclose major mathematical claims.

Overview

  • OpenAI said an internal, unreleased model running about 10,000 cooperating agents produced a proposed solution to the Navier–Stokes existence and smoothness problem after roughly 88 hours of search and about 17 hours of Lean formalization.
  • The company published a 166‑page paper and Lean proof files but said it will not seek the Clay Millennium Prize and emphasized that human verification is still required.
  • NYU mathematician Tristan Buckmaster publicly accused OpenAI of following an approach similar to his unpublished work with Levent Alpöge and questioned whether use of OpenAI tools exposed their drafts; OpenAI denies direct access but acknowledged it “cannot rule out” that de‑identified usage‑derived data influenced its models.
  • Twenty‑five Fields Medal winners published a joint declaration warning that commercial incentives to rush headline results conflict with mathematics’ norms for careful verification and attribution, and OpenAI withdrew sponsorship of a Caltech math event after criticism.
  • Independent peer review and specialist scrutiny are now under way and will determine whether the Lean formalization and the argument for a finite‑time singularity hold up, with the Clay Institute’s established prize and vetting processes still in place.