A proof can be impeccable while the question it answers is narrower than the one you meant to ask. For a research team, that makes the translation from a written requirement to a formal statement part of the evidence worth keeping.
We put that translation under review in our Navier-Stokes work. The useful result was a clause-by-clause record: which conditions matched, which needed an equivalence argument, which argument had become machine-checkable, and which questions still needed specialist judgment.
8DB gives the 8Braid Reasoning Fabric a place to connect those records to the statements and conclusions they affect. The payoff is practical: a later reviewer can inspect the specific bridge behind a claim instead of inheriting a vague “verified” label.
Two checks, two different questions
A proof kernel checks a formal derivation under its logical rules and assumptions. A statement audit asks whether the formal target represents the intended problem. Both matter.
Lean's Comparator helps compare a submitted solution with a separately supplied challenge, under its documented trust and sandbox assumptions. That protects the formal target. Reading a mathematical specification and deciding that the target faithfully captures it remains another task.
Our audit compared the Clay problem description with a pinned Formal Conjectures statement. It was machine-assisted. Its verdicts should be read as documented audit judgments, with specialist review kept visible.
Two distinct review questions
What passed, and what still needs a judgment?
Keep the requirement, its formal meaning and the checked derivation connected.
What did we ask?
Original wording, eligible inputs, allowed solutions and any amendments.
Did the translation preserve it?
Clause correspondence, equivalence evidence and unresolved interpretations.
Does this derivation establish that target?
Exact theorem, assumptions, checker version and recorded result.
The decay equivalences support a particular translation. They do not settle a separate pressure condition or replace specialist review.
One changed condition can change the claim
Consider a claim that some admissible starting data have no solution in a specified class. Two translation changes have different consequences:
- Restricting the starting-data class can be safe: an example from that smaller class still belongs to the intended class.
- Restricting the solution class needs scrutiny: excluding one kind of solution leaves open the possibility of another kind the original problem permits.
That direction check is why an audit needs more than a list of matching words. Each clause must say which side of the claim it constrains and what would overturn its verdict.
Our recorded audit contains 17 clause records. Its summary classifies 16 as faithful or equivalent under the stated readings and flags one concern for the periodic alternative, called (D). Some readings still carry explicit ambiguity flags; 16 is not a count of independently certified clauses.
The periodic-pressure requirement illustrates the distinction. It appears in the formal statement and in the errata attached to Clay's problem description. Our record flags how that added requirement relates to the original periodic formulation. It is an interpretation question about (D), not a finding that the formalization ignored the errata. The concern does not apply to the separate nonperiodic alternative (C).
Turn an equivalence argument into reusable evidence
Three decay conditions offered a constructive next step. One phrasing bounds individual derivative components; the other bounds the operator norm of an iterated derivative. The audit initially relied on an argument that these descriptions give the same bounds after adjusting constants.
We wrote a Lean module to make that bridge explicit. Its 22 theorems include the three main equivalences and the supporting finite-dimensional estimates. In plain terms: each component is bounded by a norm, and a finite sum of component bounds can bound that norm in return.
The preserved 11 September 2026 build record reports successful checking with Lean 4.33.1. Its axiom output lists only propext, Classical.choice and Quot.sound for all 22 theorems. During this editorial review, we recovered the source, matched its SHA-256 to the recorded value, and inspected the saved axiom output. This is a source-matched historical result; we have not presented it as a new execution.
That closes a specific representation question. It gives later work a named, inspectable equivalence to reuse. It establishes no new result about the fluid equations themselves.
Keep the open question attached to what it affects
The 8DB implementation records each clause's scope, verdict, argument, sources and any falsifier. It associates the periodic-pressure concern with the affected (D) relation. The decay equivalences name their Lean theorems, source hash and recorded check.
This is where a connected evidence record earns its place. A successful check of the decay lemma should improve the status of that bridge. It should not silently settle the pressure interpretation, a different smoothness question or the entire Millennium Problem.
The model also has a policy for adjusting confidence bounds when a concern is present. Those numbers are internal reasoning controls, not calibrated probabilities that a theorem is true. For an outside reviewer, the named unresolved obligation and its source are the more informative starting point.
The saved sign-off list includes a specialist reading of smoothness at the initial-time boundary, authority on the pressure errata, admissibility questions about the exhibited data, review of the proof-to-challenge bridges and confirmation of a cited endorsement. Closing each item requires the relevant evidence or judgment. A database record makes that work inspectable; it does not confer the reviewer's authority.
Bring the requirement as well as the proof
The same review pattern can help with a formalized safety requirement, an optimization constraint or a mathematical model used by an agent. Preserve the original wording, its exact formal encoding and the assumptions that connect them. Then make any unresolved interpretation a named task.
Bring us one formal statement and the requirement it is meant to capture. We can map the clauses, evidence and open questions into a bounded 8RF evaluation. The first outcome is a reviewable correspondence between question and result.
This article describes 8Braid's machine-assisted audit and preserved check records. It is not a PDE-specialist sign-off, an institutional ruling or a claim to have solved the Navier-Stokes Millennium Problem. 8Braid is unaffiliated with the cited institutions and projects.
Evidence scope Source-matched audit · 22 recorded Lean theorem checks · Specialist review remains distinct. Explore the evidence.