The Proof Watch

Claimed solutions, against the field’s own ladder · 3 claims tracked · 1 contested

Claimed solutions to famous open mathematics problems, tracked against the field's own acceptance ladder. A claim enters when it is announced and moves only when something verifiable happens to it. The desk does not referee mathematics; it records where each claim sits on the ladder its own institutions defined, and what is still unmet.

Self-check: 9 of 9 cited documents re-read 2026-09-09; 15 of 15 quoted spans located in the live text.

Read this first — what this page does, and what it does not

This desk does not referee mathematics and has no capacity to. It records where a claim sits on the ladder the field’s own institutions defined, and what is still unmet.
An unmet rung is not an accusation. Most of these rungs take years by design — the Clay Institute will not consider a Millennium solution until two years after a qualifying publication, specifically so the community has time to find errors.
A machine-checked proof is not a verified claim. Lean checks that the steps follow from the statement as formalised. It cannot tell you the statement formalised is the one the problem asks for. That gap is where the interesting arguments live.
Quotes are verbatim from the document at the URL beside them, read on the date shown.

The ladder

Announced — A claim exists in public.
Artifact public — The argument itself is readable by outsiders, not just described.
Machine-checked — A proof assistant (Lean, Coq, Isabelle) compiles the formalisation. Checks the steps, not the statement.
Preprint posted — Filed where the field archives and timestamps work.
Refereed publication — Published in a refereed journal of world-wide repute.
General acceptance — The relevant community treats it as settled.
Prize-eligible — For Millennium Problems only: two years elapsed since qualifying publication.

Claims on file

Navier-Stokes existence and smoothness

Clay Millennium Problem

OpenAI · claimed 2026-09-08 · 3 of 7 rungs

What is actually claimed: Finite-time blowup for the forced 3D Navier-Stokes equations - the breakdown direction, with a smooth forcing term.

✓Announced2026-09-08
✓Artifact public2026-09-08
✓Machine-checked
—Preprint posted
—Refereed publication
—General acceptance
—Prize-eligible

Fefferman's official statement asks for a proof of one of four statements. (C) and (D) are the breakdown cases and both explicitly admit a smooth forcing f, so a forced-blowup result is one of the four accepted routes and not a lesser substitute for it. What it is not is statement (A) or (B), the unforced existence questions most readers have in mind when they hear the problem described.

Machine involvement: An unreleased internal model; OpenAI describes roughly 10,000 concurrent agents over about 88 hours from 1 September, with a further period spent formalising in Lean.

Contested — Tristan Buckmaster (NYU), 2026-09-08

Buckmaster states he was told the result before it was announced, describes what he was offered, and raises a question about training data. He explicitly does not claim the proof is wrong.

the forcing function is smooth option c and d in Fefferman.
I was told the proof is about 100 pages. I have not seen it.
I asked whether the model had been trained on, or had access to, our sessions in Codex, into which we had been putting all our drafts for the whole of this project. I was told the model did not look up user data. I asked again, about training, and I did not get an answer.
The reply was, "Why would you ruin your career?"
I have not seen OpenAI's proof. I do not know what their model did, or how. I do not know whether our data was used. I am not accusing anyone of anything.

source ↗ · read 2026-09-08

Announcement ↗ · Proof (PDF) ↗ · checked 2026-09-08

Finite-time blowup with smooth forcing: incompressible porous media, Boussinesq, 3D incompressible Euler

Open problem, not a Clay prize problem

Tristan Buckmaster (NYU) and Levent Alpoge · claimed 2026-09-08 · 3 of 7 rungs

What is actually claimed: Three results made public together: finite-time blowup with smooth forcing for incompressible porous media, for Boussinesq, and for 3D incompressible Euler.

✓Announced2026-09-08
✓Artifact public2026-09-08
✓Machine-checked
—Preprint posted
—Refereed publication
—General acceptance
—Prize-eligible

Euler is not on the Clay list, by the official Navier-Stokes description's own words, so however strong these results are they are not a Millennium Prize solution. Buckmaster also assigns the underlying idea to others rather than to a machine.

Machine involvement: Buckmaster states several LLMs were used throughout - Anthropic's Claude and OpenAI's Codex - on a personal collaboration with no institutional agreement, and that a Lean verification was completed on 22 August.

In the claimant’s own words

Today, Levent Alpöge and I have made public three results: finite-time blowup with smooth forcing for incompressible porous media, for Boussinesq, and for 3d incompressible Euler.
The program this fits into was not started by us nor was it proposed by a Large Language Model.
My work with Levent has been a purely personal collaboration, free of any institutional agreements or official involvement by either of our employers.
The Euler writeup, in particular, can only be described as AI slop.

source ↗

Statement ↗ · checked 2026-09-08

Poincare conjecture

Clay Millennium Problem

Grigori Perelman · claimed 2002-11-11 · 6 of 7 rungs

What is actually claimed: Proof of the geometrisation conjecture, which implies the Poincare conjecture, posted in three preprints between November 2002 and July 2003.

✓Announced2002-11-11
✓Artifact public2002-11-11
—Machine-checked
✓Preprint posted2002-11-11
✓Refereed publication
✓General acceptance2006
✓Prize-eligible2010-03-18

The only Millennium Problem resolved to the Clay Institute's satisfaction, and the calibration entry for this page: seven and a half years from preprint to prize, no machine involved, and the prize declined.

Machine involvement: None.

Preprint (2002) ↗ · Clay problem page ↗ · checked 2026-09-08

What the authorities actually say

Rules for the Millennium Prize Problems

the proposed solution must be published in a Qualifying Outlet
at least two years must have passed since publication
the proposed solution must have received general acceptance in the global mathematics community

source ↗ · read 2026-09-08

Existence and Smoothness of the Navier-Stokes Equation (Charles L. Fefferman, official problem description)

we ask for a proof of one of the following four statements.
Then there exist a smooth, divergence-free vector field u◦ (x) on R3 and a smooth f (x, t) on R3 × [0, ∞), satisfying (4), (5), for which there exist no solutions
These problems are also open and very important for the Euler equations (ν = 0), although the Euler equation is not on the Clay Institute's list of prize problems.

source ↗ · read 2026-09-08

[OUTPUT] Proof Watch: 3 claimed solutions tracked against a seven-rung acceptance ladder, 1 of them contested on the record. Position on a ladder, never a verdict on a proof; every span verbatim from the cited document. probability mass ≠ 1.0