Analysis
NYU mathematician Tristan Buckmaster and Anthropic researcher Levent Alpöge published a Lean-verified proof of finite-time blowup for the 3D incompressible Euler equations late Monday night, and within a day the story had shifted from a mathematics breakthrough to a public fight over credit with OpenAI (Quanta Magazine).
The underlying math: Buckmaster and Alpöge showed the Euler equations -- the frictionless cousin of the Navier-Stokes equations that describe fluid flow -- can blow up in finite time, building on a "forcing" method from earlier work by CĂłrdoba and MartĂnez-Zoroa. The pair used Anthropic's Claude and OpenAI's Codex to help write and check the proof, completing the underlying result on Aug. 15 and finishing Lean formal verification -- meaning the logic is machine-checked line by line, not just peer-reviewed -- on Aug. 22.
Where OpenAI enters the story
Buckmaster says word of the unpublished result reached OpenAI by Sept. 3, and that OpenAI researcher Sébastien Bubeck told him on two calls on Sept. 6 that an internal OpenAI model had independently produced a roughly 100-page proof of a related, forced Navier-Stokes result -- and proposed publication arrangements Buckmaster says would have stripped Alpöge of authorship credit because of his Anthropic affiliation (Unite.AI). Bubeck has publicly called the characterization "false and inflammatory" and said a fuller response is coming. Neither side disputes that both labs' models were involved in proof-adjacent work the same week; they dispute who reached the result first and who should be credited.
Why the "solved a Millennium Prize problem" framing is overstated
Some early coverage described this as solving one of math's Clay Millennium Prize problems. That's not accurate: the actual Millennium Prize is for global regularity of the Navier-Stokes equations, and the Clay Mathematics Institute has explicitly declined to call any of this week's results -- Buckmaster and Alpöge's Euler blowup, or OpenAI's disputed forced Navier-Stokes claim -- a resolution of the prize problem. What both results actually demonstrate is narrower, and arguably more useful for AI labs: that current frontier models can now produce and verify genuinely novel proof steps in an active, unsolved area of PDE theory, not just reproduce known mathematics.
The Anthropic pattern
This is the second major AI-assisted formalization result tied to Anthropic in under a week -- Claude formalized a full, 13-million-line Lean proof of Fermat's Last Theorem using the open-source Prove2Me framework just days earlier, on Sept. 5. Anthropic has been visibly building a portfolio of hard-math showcases ahead of its expected IPO, and mathematical formalization -- because it's machine-verifiable and hard to fake -- is a cleaner marketing surface than benchmark scores labs can be accused of gaming.
The takeaway for VCs
However, the more durable signal here isn't the math -- it's the credit dispute. As AI-assisted research output becomes genuinely novel rather than derivative, capability claims from frontier labs are now contestable in public by named academics with timestamps and call logs, not just marketing copy. Diligence on any lab's research claims increasingly needs to ask who actually did the work, not just whose name is on the release.
