8Braid pins an exact margin inside OpenAI’s fluid proof

8Braid, a database company with no ties to OpenAI, re-ran the formal checks on OpenAI’s Navier-Stokes proof, released September 8. It then added a result of its own: an exact error allowance for one algebraic step of the construction, proved in Lean. The team describes the work in a technical post on the 8braid journal. It also loaded that result into 8DB, the data system it is building, and tested what happens to the stored result when the evidence behind it is withdrawn.

For 8Braid the database test was the real goal. In its words, another person or agent using the work needs to know “which statement was checked, which assumptions it needs, what still lacks evidence and what changes if that evidence is withdrawn.”

What the replay established

OpenAI’s release is a 166-page paper plus a Lean formalization. OpenAI says roughly 10,000 concurrent agents running on an unreleased internal model produced it. The theorem covers the forced versions of the Millennium Prize problem. The OpenAI repository identifies them as alternatives (C) and (D) in the Clay Mathematics Institute’s problem description. For every positive viscosity, it says, there exist smooth initial data and a smooth force for which no global smooth solution exists, both in whole space and on the periodic torus. In 8Braid’s summary, the construction starts with a fluid at rest and applies a smooth force.

8Braid replayed the submitted checks at upstream revision f9e8bc5b38b6. Comparator, the checking workflow the repository points to, matched the submitted C/D results to their expected formal statements. Two independent kernel checkers accepted the solution: Nanoda and Lean’s default kernel. The axiom reports listed only Lean’s three standard axioms: propext, Classical.choice and Quot.sound. The successful Linux run kept the original challenge configuration and a real sandbox. The team also recorded dependency pins, checker identities, commands and the actual outcomes.

8Braid is careful about what this proves. The formal proofs were accepted against the encoded statements. Reading the mathematics, checking that the encoded statement matches the physical problem, and applying the result somewhere new “remain distinct jobs.” Lean confirms that an argument follows from its definitions. It cannot confirm that those definitions capture the question that was meant. The post also separates formal reproduction from specialist peer review and from any Clay decision. As of September 9, Clay had not accepted the result, and OpenAI has said it will not claim the $1,000,000 prize.

The m/4 allowance

The new result sits inside Proposition 7.5, equations (7.24) to (7.28), on printed pages 82 to 83 of the paper. That step uses a positive covariance decomposition. In practice, the construction combines two contributions with weights that must stay positive. The question 8Braid asked is how far the inputs can drift before that positivity fails. The original argument assumes some sufficiently small tolerance without giving its value.

In the step’s normalized coordinates, the matrix is [[1+a, 1+b], [-1+c, 1+d]] and the target is (1, s). The target must sit inside its allowed cone with margin m, meaning |s| ≤ 1−m, where 0 < m < 1. Under that condition, an error of at most m/4 in each of the four entries keeps the correction weights positive, and the determinant stays at least 7/8. The fractions are exact. The bound holds over the whole stated real-parameter domain rather than at sampled points. Separate Python checks rebuild the rational algebra, and a standalone Lean proof checks the general implication.

8Braid does not frame this as fixing a gap. “The original argument was not defective because it left a sufficiently small constant abstract,” the post says. Its contribution is “an explicit conditional bound, with its assumptions attached.” The conditions matter. Applying the bound to OpenAI’s actual construction still requires the source’s analytic error envelope and profile bounds, and physical interpretation needs the stated frame and positive scales. According to the footnotes, the attachment does not instantiate the source profiles, prove their error envelope, or settle smooth extension at a zero target. The team makes no claim that m/4 is the best possible allowance. So far, the independent work covers one proposition across two printed pages of a 166-page paper.

The proof attachment includes the exact Lean source, toolchain and Mathlib pins, axiom output and a file manifest. Replay instructions are on a public GitHub companion.

What happens when support is withdrawn

The database test ran as a separate native 8DB research workload. It tracked whether the lemma was available, alongside the obligations needed to apply it. The team then withdrew the lemma’s supporting admission and read the saved state again. Three kinds of record were tracked:

• The conditional covariance lemma: available for its declared scope before withdrawal, no longer supported as available after.
• Its application to the actual source construction: separate obligations unadmitted before, still unadmitted after.
• Unrelated historical results: kept their existing support throughout.

“Withdrawal changes the record of available support. It does not make the mathematical implication false,” the post says. The test fixture holds 88 facts and 26 rules. Seven adapter tests and 24 refusal controls passed. The six source and PDE obligations stayed unadmitted, and an earlier qualified 1/73 result was preserved. The run went through both the native consumer and a separate reader, including a replay from a fresh local directory.

The scope here is narrower than the headline suggests. The consumer uses a fixed Taylor-Green research context, a standard textbook flow, and works on frozen snapshots. It did not ingest OpenAI’s full construction and did not independently certify the PDE. The mathematical verification sits outside the database consumer. 8Braid also separates same-host relocation, which it checked, from new ingestion into its Store or reproduction by an outside team, which it has not done.

Checks inside an agent’s loop

OpenAI’s own run shows the scale at which unchecked steps can pile up. About 1,000 agents first solved the Euler variant in roughly 50 hours. About 10,000 then reached the Navier-Stokes result after about 88 hours. GPT-6 Astra spent about 17 more hours on the Lean formalization. The Navier-Stokes effort alone used about 2.7 million agent messages and 130 billion output tokens.

8Braid proposes putting a checker between an agent’s proposal and its acceptance into the research record. A changed polynomial coefficient would fail an exact identity check. An artifact from the wrong context would fail an applicability check. An inference without support would stay unadmitted, which gives the agent a concrete reason to revise its next step. The team says its tests exercise refusals at the mathematical, scope and evidence-integrity boundaries. It has not measured any reduction in an end-to-end agent’s error rate, and it has no production latency guarantee.

The idea reaches a field where checking AI proofs is already contested. In September, Caltech mathematicians wrote in an open letter that verifying an AI lab’s claimed proof “goes uncompensated, uncredited, and unacknowledged.” 8Braid’s version of the handoff has an agent pass along a claim together with its executable check, its assumptions and its open questions. A second agent reproduces the check, and a third works on an open condition. The company says that interoperable evidence formats and use in other research programmes “are still work for the wider community to do.”

The planned integrations are also unbuilt. 8Braid’s Verified Thermodynamic Truth Engine, VTTE, includes interval-backed numerical tools that could supply bounded inputs to the inequality. Sheaf and homology methods could check consistency and gaps between certified parameter regions. The post says this integration “remains to be built and qualified.” It also notes that the research and writing used AI assistance, with the mathematical and evidence checks identified separately.

The company has set itself two next steps. On the database side, it plans to move the result into a context-independent theorem and evidence workflow. On the mathematical side, the next task is “to supply the analytic bounds needed to apply the covariance allowance to selected source columns.” Until that is done, the m/4 bound applies to the normalized step and has not been carried through OpenAI’s actual construction.