The authors of the Boussinesq blow-up certificate say replaying it needs up to 150 gigabytes of memory. We ran the replay on a machine with 62, and the trick was not compression or cleverness. It was reading the memory figure for what it was: a parallelism number wearing a requirement's clothes.1
The problem
The second of September's two fluid results comes with Lean certificates whose replay the authors budget at "on the order of 100 GB of memory and a few hours at two dozen parallel jobs" for two of the projects and "150 GB at three dozen parallel jobs" for the Boussinesq one. The Boussinesq certificate is the interesting case: about twelve hundred machine-generated interval-arithmetic modules, each decided by the kernel with the ordinary decision procedure rather than a native escape hatch. That is the precedent for kernel-checked interval arithmetic inside a fluid proof, and we wanted the replay recorded as a verification event in our evidence twin. The machine available had a sixteen-core processor, 61.7 GB of memory, and a system-managed pagefile that put the total commit limit near 70 GB.
The observation
Read the quotes again. Memory is stated together with parallelism, and dividing one by the other gives roughly four gigabytes per module. Each module is checked in its own process and writes its compiled object to disk when it finishes. The working set is therefore the modules in flight, not the size of the project. Nothing about the kernel check requires the whole certificate in memory at once. If you can bound how many modules are in flight, you can bound memory, and the price is wall-clock time.
The method
The build runs inside a Windows Job Object with a hard commit limit, the same mechanism we use to demonstrate memory caps elsewhere. A launcher samples memory every thirty seconds to a CSV and writes a JSON summary at exit: start, end, exit code, peak commit for the job, peak commit for any single process, and the maximum number of concurrent checker processes. That summary is the event detail. A module that exceeds the clamp is a contained failure; the build system keeps its traces, so the next attempt resumes where the last one stopped rather than from zero. A pipeline then steps down a thread ladder on failure.
Two details cost time to learn. The build tool at this Lean version has no jobs flag, so the environment variable that bounds the checker's threads is what bounds parallelism, and it has to be set in the launching shell so the build tool and every child inherit it. And the default toolchain for the project had no prebuilt objects for its Mathlib pin, so Mathlib itself had to be compiled from source under the same clamp first.
What was measured
| Phase, 11 September 2026 UTC | Threads | Clamp | Outcome |
|---|---|---|---|
| Mathlib from source, 8,264 modules | 6 then 8 | 28 then 40 GB | Complete by 21:05; peak job 18 GB; largest single process 8.1 GB |
| Certificate modules, first attempt | 8 | 40 GB | Contained failure at 21:10 after 3,112 s; peak job 40.03 GB; nine processes in flight; largest single process 10.4 GB |
| Ladder step | 6 | 28 GB | Clamp hit in 60 s |
| Ladder step | 4 | 28 GB | Clamp hit in 30 s |
| Certificate modules, settled | 2 | 28 GB | Running from 21:12; about 20 GB in flight; job 9,678 of 10,108 at 23:52 |
The certificate modules are the reason the authors' number is what it is. A typical Mathlib module peaks near three gigabytes; a kernel-decided interval certificate peaks near ten. Eight of those in flight is eighty gigabytes, which is where the first attempt hit the wall. Three threads under the 40 GB clamp would have fit and run about half again as fast as two; the running build was left alone rather than restarted, and that trade is recorded too.2
Why the record matters more than the trick
The clamp is a nice trick. The reason to write it down is what happens to the result. When the certificate phase finishes, the pipeline prints the axioms of the three headline theorems, builds the two sibling projects from the shared Mathlib, and replays each solution's full import closure through the kernel from scratch. Each of those steps becomes a typed verification event with a timestamp and an exit code, and those events, not our opinion, move the three atoms for this group's results from the static-audit tier to the independent-build tier in the evidence twin. The final step of the formal ladder is a Comparator match, kernel-checked against a pinned statement, and the twin says exactly which tier each atom has reached and why.3
This is what we mean when we say a rebuild is a commodity and the governance is the product. Anyone can run a build. The question is whether the run leaves behind something a stranger can inspect: what was built, on what, under what limits, with what outcome, and what it entitles you to conclude.
Rules worth keeping
- Quote memory with the parallelism it was measured at, or the number is not reproducible.
- Bound in-flight work with an enforced limit, not a suggestion, and treat the limit being hit as a resumable event rather than a crash.
- Keep every log outside anything that might be rebooted or cleaned.
- Write the summary the moment the process exits, machine-readable, and make it the event.
- When you discover you explained an observation wrongly, leave the wrong explanation in the record with the correction next to it.
What to bring us
- A certificate you cannot afford to replay. If you have a formal development whose replay is budgeted beyond your hardware, send the README numbers and we will tell you whether the clamp applies.
- A Linux host with a current kernel. The one step we could not record here is the sandboxed Comparator match. If you can run it, the event has a place waiting for it.
- Your replay logs. If you have already replayed this or the other September developments, we would like to ingest your run as a registry-neutral event with your name on it.
Write to hello@8braid.com with the subject "Replaying a formal certificate under a memory clamp". You will hear back from an engineer.
Sources and further reading
- tristanbuckmaster/fluid_lean, with the projects' README memory guidance
- Lean 4 and Lake documentation
- Microsoft Learn: Job Objects and JOBOBJECT_EXTENDED_LIMIT_INFORMATION
- 8DB: A Proof Is a Graph Where Confidence Only Flows Downhill
- 8DB: We Put a City's Map on a Phone With No JSON in the Hot Path. Here Is What Stopped Us at the Planet.
All figures were measured on one Windows 11 host (Ryzen 9 9950X3D, 61.7 GB memory) on 11 September 2026 and describe that run. The replay was still in progress when this was published; its outcome is recorded as events in the evidence twin, not edited into this article. Nothing here is a claim about the mathematical content of the certificate or about the Navier-Stokes equations. 8Braid has no affiliation with the authors of the development referenced.
Footnotes
-
This article was written while the build was at job 9,678 of 10,108, on 11 September 2026, because the interesting part was already over and the useful part is the method. The replay was still running at publication; its outcome is recorded as events in the evidence twin, not edited into this article. ↩
-
A note made earlier in the session, attributing the two-process concurrency to a dependency chain, was wrong. It was the ladder. The correction is in the record beside the note. ↩
-
The Comparator match needs a Linux sandbox this machine does not yet have, so the twin will show these atoms one tier below the Navier-Stokes theorem until it does, and it will say why. ↩
Continue the technical conversation
Where could this help your work?
Bring a research question, a database workload or an application you want to build. Let’s connect the ideas in this article to an evaluation that matters to your team.
Discuss this work