Overview
- OpenAI announced Tuesday that an unreleased internal model produced a Lean-formalized proof it says resolves the Navier–Stokes existence and smoothness question after about 88 hours using roughly 10,000 concurrent agents and millions of dollars in compute.
- NYU mathematician Tristan Buckmaster and Anthropic researcher Levent Alpöge published related AI-assisted advances earlier and say OpenAI shifted focus after learning of their work and proposed authorship arrangements that would exclude Alpöge.
- OpenAI denies that its researchers or agents accessed Buckmaster and Alpöge’s unpublished drafts but acknowledges it cannot fully rule out that de-identified user data indirectly improved its models.
- The Clay Mathematics Institute requires publication, peer review and a prolonged community acceptance period before convening a prize committee, so any Millennium Prize determination will follow extended scrutiny.
- The episode highlights new tensions in mathematics over credit, reproducibility and the growing advantage held by labs with vast private compute, which may reshape who leads frontier mathematical work.