A GitHub repository with two commits and 1,900 stars contains the bluntest claims in fluid dynamics, stated in a language a compiler can read. The repository holds Lean 4 certificates for two papers: "Finite time blowup for Navier–Stokes" and "Finite time blowup for the Euler equation." The Euler result is a single sentence. Take smooth, compactly supported, divergence-free initial velocity on all of three-dimensional space. Its solution to the unforced incompressible Euler equations develops a singularity in finite time: the velocity's \(C^1\) norm becomes unbounded near that time, and the time integral of the vorticity's \(L^\infty\) norm diverges. For Navier–Stokes with any positive viscosity, the certificates cover two companion statements — on the whole space, there exist smooth initial data and forcing for which no global smooth solution with uniformly bounded kinetic energy exists; on the periodic torus, smooth periodic data and forcing for which no global smooth solution exists. Those two statements are alternatives (C) and (D) in the Clay Mathematics Institute's official description of the Navier–Stokes Millennium Prize problem.
A blowup theorem is a strange object to certify. Most formalization efforts encode positive claims — objects that exist, proofs that construct them. A blowup theorem asserts nonexistence: that nothing smooth survives past a finite time. To prove that in a machine-checkable way, you must encode "smooth solution" with total precision, because the theorem is precisely about where that definition fails. In prose mathematics, "smooth" is a handshake. The author writes it, the reader supplies the regularity the argument needs, and the community has run on that arrangement for a century. A blowup certificate is the one place the handshake is unusable, because the subject of the theorem is the moment the handshake breaks. The certificate has to say, in exact terms, what it is that fails to exist — which space, which norm, which class of solutions — before it can prove the failure.
That requirement explains why blowup results need certificates more urgently than almost anything else in analysis. The standard proof of a singularity is a chain of inequalities — hundreds of estimates, each a bound on a norm, each depending on the previous one. The failure mode of such a proof is not a gap in reasoning. It is a sign error buried in a line nobody re-reads, which inverts the conclusion: nonexistence becomes existence, or the blowup time moves. The field's history includes blowup claims that collapsed under scrutiny, and the collapses were almost always of this kind — a chain that didn't actually close, an estimate that held only in the wrong space, an inequality that pointed the wrong way on the last step. A machine-checked certificate makes the chain a compilable artifact: every norm typed, every inequality discharged against a library that refuses to accept a handshake. Lean, with Mathlib underneath, will not supply the regularity the reader was supposed to supply. It demands the estimate, in full, and the estimate either holds or the build fails.
The repository has two commits. That detail matters, because it means the certificates were written by the same people who wrote the theorems. In prose mathematics, self-checking is the norm: the author of a proof is its first and most careful reader, and peer review supplies the external check. A certificate inverts the arrangement in a way nobody has fully absorbed: the machine check is the strongest check the artifact will ever receive, and it happens inside the authoring loop, before any peer sees the work. The external check therefore has to move one level up. That is what the repository’s second artifact is for. Alongside the certificates, it ships a Comparator — a second, independent proof checker that re-checks the formalizations with different machinery. The logic of that choice is worth stating because it is the machine version of a very old idea. A certificate is only as trustworthy as the checker that accepts it, and a single checker is a single point of failure. Independent replication, in the machine world, means a second checker: if two checkers built by different people on different principles both accept the artifact, the probability that both are wrong in the same way is the probability the community actually cares about. The Comparator is verification of the verifier. It is what peer review becomes when the paper is a data structure.
There is a precedent for the exact situation this puts the field in, and it is the Four Color Theorem. In 1976, Kenneth Appel and Wolfgang Haken proved it with a computer that checked 1,936 configurations, and mathematics spent the next decades arguing about whether that was a proof at all — a proof no human could read in a lifetime. The argument ended not with a committee verdict but with a certificate: in 2005, Georges Gonthier and Benjamin Werner rebuilt the entire proof in the Coq proof assistant, and the dispute collapsed. A machine proof is contested until it becomes a certificate, and then it stops being contested, because the thing under dispute — whether the case analysis was complete, whether the code was right — becomes a compilable claim with a yes-or-no answer. The blowup results arrive at the contested stage with their certificates already written. The exit was built before the argument started.
The remaining gap is not in the certificates. It is the bridge between the certificate and the community's meaning, and it is worth being precise about its shape, because it is exactly the shape of an old infrastructure problem. The United States ran two definitions of the foot for six decades: the international foot, defined as exactly 0.3048 meters, and the survey foot, defined as exactly 1200/3937 meters. They differ by two parts per million — nothing on a doorframe, everything on a state boundary. Surveyors knew both existed, converted between them by convention, and the error sat in the joints of the system: small, systematic, permanent. The National Geodetic Survey deprecated the survey foot only in 2023. The lesson of the two feet is that a definition is infrastructure, and parallel definitions are infrastructure debt: nothing breaks visibly, everything drifts slightly, and the drift accumulates in exactly the places nobody re-checks. Prose mathematics has been running two definitions of "smooth" for a century — the reader's and the checker's — and the blowup certificates are the first place the two are forced to meet on the same page, in the same artifact, with the drift visible.
The singularity is now a compilable object: a specific time, a specific norm, a specific divergence, each discharged against a library that does not do handshakes. What has not been formalized is the sentence that connects the two — the claim that what Lean proved is what the community meant when it asked whether Euler blows up. Every formalization is a draft of that sentence. The certificates are the moment the field stops pretending the handshake is costless, and once the bridge is written down, the two definitions of smooth will have to pick a survivor — the way the two feet finally did, after sixty years, with a date on a government notice.