In an October 2 World Science Festival interview, mathematician Tristan Buckmaster described a result produced with AI that he considers correct but difficult for other mathematicians to read. His account gives the recent Navier–Stokes announcement a more specific question: how does a research community examine a formal argument when a readable explanation takes further work?

Buckmaster was discussing his work with Levent Alpöge on the three-dimensional Euler equations with smooth forcing. Their result is separate from OpenAI’s September 8 claim about the Navier–Stokes equations with smooth forcing. Navier–Stokes includes viscosity; Euler does not. OpenAI released a paper and Lean formalization for its claimed finite-time breakdown result. The institute that administers the Millennium Prize has not announced an award.

The big change

  • What changed: Buckmaster has given a first-person account of using AI-generated arguments and Lean to establish the separate forced-Euler result, and of the work still required to explain such proofs to mathematicians.
  • Why it matters: A formal check can establish that an encoded argument follows from specified definitions and dependencies. Mathematicians also need to understand what the theorem says, how its ideas work and whose prior work it uses.
  • What to watch: Clay’s evaluation of OpenAI’s Navier–Stokes claim, readable accounts of the proof, and public treatment of authorship and access will show how this result is assessed. Buckmaster’s confidence in the result is an expert view, not a prize decision.

A checked argument still needs an explanation

In the interview, Buckmaster says the first AI-produced proof of his Euler result mixed useful ideas with irrelevant calculations and difficult prose. His team first used other agents to examine individual steps, then converted the argument into Lean for a formal check. He says the resulting proof was correct despite its poor presentation. That account is about his Euler work; it should not be read as his independent verification of every part of OpenAI’s different Navier–Stokes paper.

The distinction is practical. Lean checks a precisely formalized statement in a specified proof environment. It does not, by itself, make a long argument legible to a researcher who wants to reuse its method. Buckmaster told Brian Greene that other AI systems could parse passages he found barely readable, and that asking AI to translate them into ordinary mathematical language became part of the work. He also said he could still understand the ideas in the Navier–Stokes argument, even though its published PDF was hard to read. These are his reported assessments, not a BIG CHANGE proof audit; we did not run the Lean files or referee either theorem.

NYU Courant’s September 14 account identifies Buckmaster and Alpöge’s achievement as finite-time loss of regularity for forced 3D Euler, with a smooth force and finite-energy initial data. It says three papers from the collaboration were formalized in Lean and places the result within a strategy begun by Diego Córdoba and Luis Martínez-Zoroa. Those details matter when assigning credit: a model-generated proof can extend an existing mathematical route without erasing the people who established it.

Two results in one fast-moving sequence

OpenAI says its internal agent system first produced an unforced Euler result, then used that line of work in its separate Navier–Stokes construction. Its announcement acknowledges the priority of Buckmaster and Alpöge’s forced Euler result while saying its proof was developed independently. Buckmaster, in the interview, describes the mathematical mechanisms as related and says OpenAI added an idea involving a collapsing vortex to handle viscosity. The accounts agree that the claims concern different equations and different proof steps; they do not settle every question about chronology or intellectual credit.

The European Mathematical Society welcomed the announcement while emphasizing earlier work and calling for attention to authorship, credit and access to the internal model. Clay’s September 11 response said the Navier–Stokes problem had apparently been settled and that evaluating the achievement and assigning credit would be deliberately unhurried. Buckmaster told Greene he believes OpenAI has a solution. Readers can hold both statements at once: a specialist's positive assessment and an institution's continuing evaluation.

The recent withdrawal of three other OpenAI math manuscripts is a separate event. Their reported sign error is a reason to examine claims individually; it is not evidence that the Navier–Stokes proof contains the same error. BIG CHANGE’s repository inspection explains how to locate manuscript versions and proof artifacts, while our opinion on review capacity argues that explanation and checking need dedicated support. The earlier Navier–Stokes article records the start of this sequence. This interview adds the working mathematician’s account of what comes after an AI system produces an argument.

For a claim this consequential, the next useful publications are precise human-readable accounts, inspectable formal artifacts, and independent mathematical responses. Each does a different job. The speed of generating a proof candidate makes those jobs more urgent, while Clay’s stated process leaves room to do them carefully.

Sources & further reading