Journal series · 10 articles
Read the complete sequence or enter at the question most relevant to your architecture.
Iterating on Navier-Stokes
We reproduced the formal checks, proved an explicit bound for one construction step, and tested how 8DB handles its evidence. The larger opportunity is to help AI catch checkable errors while it works, before they become the next step's assumptions.
Iterating on Navier-Stokes
The forced Navier-Stokes breakdown proof runs on oscillatory loops with a safety margin. We took one of those loops at its reference profile, found a shape with a margin about twenty percent wider than the best any single sine wave can achieve, then let the research graph choose the next experiment and found a second shape that lowers four of the construction's own cost bounds at the same margin. Every bound is a certified interval, every candidate that lost is kept, and the database did the bookkeeping.
Iterating on Navier-Stokes
In the second week of September 2026 a kernel-checked Lean proof established two of the four Clay alternatives for Navier-Stokes, and a second group published machine-checked forced blow-up for three related equations. Within seventy-two hours we had rebuilt the proofs from source, audited their axioms, matched them to the pinned statements under two kernels, and recorded every step as governed evidence in 8DB with host, time and exit code. This is the map of what is established, what is open, and what a database adds when the frontier of an open problem moves in a week.
Iterating on Navier-Stokes
Five months of Navier-Stokes work leaves a lot of documents, and documents are where attractive ideas quietly become premises. We read every accessible file on the subject, 573 of them, and asked one question of each claim: does it survive an exact counterexample? Ten did not. The review also found three real defects in the database itself, fixed them with regression controls, and recovered a formal contribution that older summaries had been calling missing. The ideas survived; the invalid inferences stopped supporting conclusions.
Iterating on Navier-Stokes
The state of an open problem is not a document. It is a graph of statements, each with evidence, each implying others, some still open, and it changes every time someone posts. We built that graph for Navier-Stokes as governed atoms in 8DB: intervals instead of scores, restriction maps that refuse at write time to let a conclusion outrank its premise, typed gaps for what is open, tiers derived from verification events rather than assigned, and a retraction query that answers in one call what falls if a premise is withdrawn. This is the design, with the numbers it holds.
Iterating on Navier-Stokes
A proof assistant tells you a proof matches a statement. It cannot tell you the statement matches the problem. When the Navier-Stokes breakdown proof landed, the statement it was checked against was a Lean encoding of the Clay Institute's prose, written months earlier by someone else. We audited that encoding clause by clause: sixteen faithful, one concern, and three that rested on an argument in English, which we replaced with twenty-two kernel-checked lemmas.
Iterating on Navier-Stokes
Store a loop from a fluid-dynamics proof as a table of sampled values and you can plot it. Store it as one object with six views, a symbolic formula with exact parameters, a charted manifold, a point cloud in state space and again in derivative space, a weighted field on a declared domain, and an interval certificate, and you can ask which questions the table hides. Here is the loop, view by view, and the query in which two identical states turned out to be moving in different directions.
Iterating on Navier-Stokes
The Lean certificate for forced Boussinesq blow-up contains about twelve hundred machine-generated interval-arithmetic modules that the kernel decides one by one, and its authors budget 100 to 150 gigabytes of memory to replay it. We had 62. The number turned out to be parallelism times per-module footprint, not a requirement of the check, so we ran the build inside a hard memory clamp and let it fail and resume until it fit. Every run left behind a record a stranger can inspect.
Iterating on Navier-Stokes
Research claims inflate in a predictable way: a correct observation is written down, an implication that nobody typed as a claim gets attached to it, and five months later the two travel together into a deck. A claim ledger exists to make that impossible. This is a worked case from our own Navier-Stokes record, with the exact implication, the arithmetic that falsifies it, what the ledger now says, and the eight claim shapes any governance system for research has to hold without flattening them.
Iterating on Navier-Stokes
Since April 2026 we have used the Navier-Stokes regularity problem as a test article for 8DB, under one rule: every attempt is composed from the database's own primitives, and every place the database cannot express what the mathematics needs is written down as friction and becomes an engineering task. Six months of that produced an exact list of where a store built for regulated data falls short of research, and the fixes that shipped because of it: asymmetric uncertainty, typed proof obligations, write-time audited implications, derived trust tiers.