Agent Horizon

OpenAI says an internal, unreleased model, working through a coordinated system of roughly 10,000 AI agents, produced a proof addressing the Navier–Stokes existence and smoothness problem, one of the seven Clay Mathematics Institute Millennium Prize Problems. The company published a full writeup along with a machine-checked formalization of the proof in the Lean proof assistant, describing a scenario in which a smooth, finite-energy fluid at rest develops a singularity in finite time. Read the official announcement for the technical details.

Why this is a bigger deal than another benchmark score

If it holds up, this would mark one of the first times an AI system produced original progress on a problem long considered among the hardest in mathematics, one that has resisted a full resolution for about 90 years. That distinguishes it from typical “our model scored higher on a math benchmark” announcements: OpenAI is describing a system that generated, checked, and formalized new mathematical content rather than reproducing known techniques faster.

But the announcement lands in the middle of a genuinely messy credit dispute, and a grounded read has to include it. NYU mathematician Tristan Buckmaster and Anthropic researcher Levent Alpöge had independently been working on a related but distinct result involving forced Euler blowup, and Buckmaster has publicly alleged that OpenAI staff pressured him to drop Alpöge from authorship because of his employer, an allegation an OpenAI researcher has called false. OpenAI’s own post says it began its effort after hearing rumors connected to that work and reached out to offer a joint, concurrent release once its own proof was complete.

The scale of the compute involved is also worth noting on its own terms: millions of agent messages and hundreds of billions of output tokens, reportedly costing millions of dollars, for a single mathematical result. That is a very different model of “doing research” than a lone mathematician with a notebook, and it raises real questions about reproducibility, verification workload for the broader math community, and how credit gets assigned when unpublished work shared with AI coding tools becomes visible to the companies building those tools.

The healthy caveat: OpenAI is explicitly not claiming the Clay Institute’s prize money, and independent mathematicians still need to scrutinize the proof before it’s accepted as resolving the problem. Treat this as an important, closely watched claim rather than a settled fact until that review happens.