dregg microsites 14 · Mathematics

A review, an erratum, and a roadmap

Reading a
millennium proof.

In August 2026 an independent researcher published a claimed proof of global regularity for the three-dimensional Navier–Stokes equations on the torus · statement (B) of the Clay Millennium formulation · with a Lean verification companion on GitHub. We did the thing the setup invites: we read it.

The identity.

The paper's vorticity argument leans on a compact display in its §3.1: the growth of vorticity magnitude along trajectories. Written as displayed, it says:

as printed
Dt|ω|  =  α|ω|
for ν > 0, the identity is
Dt|ω|  =  α|ω| + ν ξ·Δω

The printed form is the inviscid identity · true when viscosity is zero · appearing in a proof that is entirely about positive viscosity. And it is not a typo in passing: the per-trajectory chain in §16.2 and the localization step in §10 rely on the display as written. A viscous term that the whole argument exists to wrestle with had gone missing from the equation that carries it.

What happened next.

This is the part worth telling. The review went in as an ordinary pull request against the verification repository, stating the finding plainly. The author engaged immediately and honorably: the finding was acknowledged as a genuine error in the paper as published, an erratum section was added crediting the review, the repository was reorganized to separate the frozen published version from the revision in preparation, and a revised release followed within days.

No drama, no defensiveness, no burying. An independent researcher put a bold claim where anyone could check it, and when someone checked it, the record got corrected in public with the reviewer's name on the erratum. Whatever the final fate of the revised argument · on which we make no claim either way · this is what good looks like.

The turn.

A review can catch an error after it is claimed. A formal library can refuse it at the moment it is stated · a Lean development of the viscous equations simply does not let the inviscid identity stand in for the viscous one, because the missing term is sitting in the definition.

So the story ends somewhere better than an erratum. The same month, we joined Tau Ceti · a new experiment incubated by the Lean FRO and the Mathlib Initiative, where humans own the roadmaps and AIs write the mathematics, subject to adversarial review · and contributed the roadmap for incompressible flows and the Navier–Stokes equations: the Helmholtz–Leray projection, the Stokes semigroup, strong and mild solutions, Leray–Hopf weak solutions, the two-dimensional global theory, partial regularity. Library results, not a bespoke encoding of one proposed proof.

The roadmap's scope line is its spine: the three-dimensional global regularity problem is not a completion target. The library must make the open problem precise enough to state, and must support research about it · and no assertion of global smoothness or blowup is a deliverable. First contributions are already in the tree: periodic integration on the unit torus, the incompressible Gelfand triple, Galerkin projections.

Make the question stateable before it is claimed. That is the whole lesson, and it generalizes well past fluid dynamics.

Status, plainly: the review, erratum, and revision are on the public record in the author's repository. We assert nothing about the revised argument's correctness in either direction. The Tau Ceti roadmap and first Lean contributions are public in the TauCetiProject repositories.