Overview
- OpenAI published a paper and a Lean formalisation on Sept. 8 asserting an unreleased internal model and about 10,000 coordinating AI agents produced a proof that three‑dimensional Navier–Stokes solutions can develop a finite‑time singularity.
- The company says the multi‑agent run reached the result in roughly 88 hours and that a follow‑on Lean verification took about 17 hours, with the overall compute effort costing millions of dollars.
- A credit and data‑access dispute has emerged after NYU mathematician Tristan Buckmaster and Anthropic researcher Levent Alpöge released related work and raised concerns that OpenAI may have pursued their research direction; OpenAI denies seeing their drafts but says it cannot fully rule out de‑identified training exposure.
- Mathematicians note that a Lean proof checks logical steps but does not by itself settle whether the exact Clay Prize formulation has been met, and the Clay Mathematics Institute requires peer review and a period of community validation before convening a prize committee.
- If verified, the result would mark a major example of frontier AI producing formal mathematics and will prompt debates about authorship, data governance, and how machine‑generated discoveries should be credited and integrated into human research workflows.