- Sources: report, statement, discussion
- Summary: Scientific American reported on 2026-09-08 that OpenAI states an internal model, which OpenAI has not named, produced a proof of finite-time blowup for the Navier-Stokes equations certified in Lean, and the article characterizes that claim as the second solution ever of one of the seven Millennium Prize Problems. The same article reports Tristan Buckmaster alleging the result draws on work he and Levent Alpoge, a mathematician employed by Anthropic, had not yet released. OpenAI mathematician Sebastien Bubeck denied that at a press briefing, said the Navier-Stokes solution followed a method similar to the two mathematicians' while the Euler result did not, and said the proof was developed over the weekend, which the article notes is after the point at which Buckmaster claims news of his result had reached OpenAI.
- Why it matters: OpenAI states the proof was certified in Lean, which makes the claim machine-checkable rather than prose, and the unresolved question is whether the lab's result was independent of work it had already learned about.
- Follow-up: Track the release of the Lean artifacts and any independent account of the timeline.
send feedback on this story