Specification Seams · Lean 4

A proof can compile and still not prove the claim.

Lean’s kernel checks that a proof matches its formal statement. It cannot check that the statement means what the paper, the audit report, or the press release says.

When OpenAI and Anthropic each published a Lean 4 formalization refuting the Exponential Time Hypothesis in October 2026, both kernels accepted the proofs within days. Determining whether the formal statements actually say “ETH is false”—and on what machine model, input encoding, and crossover size—took independent readers, bridge proofs, and weeks of close inspection.

“The kernel certifies that the proof matches the statement. Whether the statement matches the claim is the specification seam.”

SeamCert reads your Lean statement files for the places where a formal theorem and its intended claim come apart: escape hatches, custom definitions the theorem quietly leans on, hypotheses that contradict each other, hidden existential constants, and planted wrong variants your proof should refuse.

Check a Lean file free Read the 2026 claims ledger ↓

In Brief · What the Scan Reads

1. Escape Hatches Flags sorry, admit, custom axiom declarations, native_decide, implemented_by, extern, unsafe, #exit, and disabled kernel checks.
2. Seam Surface Lists every custom definition, structure, typeclass instance, notation, and non-Mathlib import that shapes what the theorem means.
3. Statement Shape Checks for contradictory hypotheses, False premises, vacuous natural-number bounds, trivially true conclusions, size promises, and existential constants.
4. Planted Wrong Variants Generates a ready-to-run Mutants.lean with a vacuity probe and perturbed constants or relations for each theorem. Every one should fail to compile.

Free Scan

Check a Lean 4 statement file

Paste the file that states your main theorem—the challenge or specification file. The scan is a static reading of the text: nothing is compiled or executed, and it finishes in a second. A clean scan means we found none of these patterns, not that the statement is right.

Claims

The October 2026 complexity formalizations

What each headline paper claims, what is stated in Lean versus prose only, and who has replayed the proof. Every entry is footnoted to the public source that reported it. SeamCert has not replayed these proofs; the kernel replays cited below are independent third parties’.

Claim	What Lean states	Prose only / open seam	Replayed by	Sources
OpenAI ETH refutation A deterministic algorithm counts the satisfying assignments of a k-CNF in subexponential time, refuting ETH.	`exact_count_and_sat`: Proposition 6.4 bound n(log log n)²/√log n on OpenAI's multitape machine over unary words.	Headline Theorem 1.1 exponent n·log log n/√log n; textbook ETH definition (bridged externally by Toledo).	Toledo (Comparator 80 GiB, nanoda, leanchecker --fresh); Szeider (crossover reading). Not replayed by SeamCert.	[1], [2], [3], [4] Full notes →
Anthropic ETH refutation 3-SAT (and #3-SAT) in time 2^o(n), with ETH defined in Lean and its negation proved.	`ETHIsFalse` (0 < s₃ negated over FinTM2) and `MainTheorem` for k ≥ 1, m ≥ 2, n ≥ 4 with every variable occurring.	Reduction from general k-CNFs (unused variables, small m/n) to the `MainTheorem` promise class.	Toledo (Comparator 24 GiB, nanoda, leanchecker --fresh, C2 bridge); Szeider; Majdoddin. Not replayed by SeamCert.	[5], [2], [4], [6] Full notes →
Deterministic factoring in N^o(1) A deterministic Turing machine computes the smallest prime factor of every N in N^o(1) steps: for every k ≥ 1, within C_k·2^(n/k) steps on n-bit inputs.	13-line Mathlib statement: ∀ k ≥ 1, ∃ C_k bounding steps by C_k·2^(n/k) (~35,000-line proof generated by Claude Opus 5.5).	Magnitude of existential C_k and the crossover input size where the bound improves on N^(1/5+o(1)).	None found in the sources read. Not replayed by SeamCert.	[7], [3] Full notes →

Sources checked 7 November 2026. Corrections or newer independent replays: [email protected].

Deep Audit · Fee Schedule

Commission a Deep Audit — £349

For a formalization you need to rely on in production or in print: a zero-knowledge circuit specification, a smart-contract invariant, or an AI-generated proof you are about to cite or ship. Delivered within five working days of payment.

Independent kernel replay. Your pinned commit built on a disposable build machine and checked with Lean’s kernel, leanchecker --fresh, and the independent kernel nanoda, with #print axioms recorded on every named theorem.
Planted variants & witness check. Every generated mutant compiled against your proof, plus an explicit witness proving your theorem’s hypotheses can hold simultaneously.
Definition reading & bridges. Each custom definition compared line by line against the standard Mathlib notion, with short bridge lemmas proved where practical.
Explicit constants. Existential constants and crossover thresholds worked out where the theorem statement leaves them implicit.
Written correspondent’s report. Published at a private URL, with every finding marked clearly as either kernel-checked or our reading.

Order a Deep Audit (£349) Run SeamCert in GitHub Actions →

Questions & Scope

Is a scan or audit a certificate of truth?

No. A scan lists the specification seams to read; a Deep Audit checks those seams with independent kernels, planted variants, and a human reading. Neither guarantees that an underlying informal mathematical claim is true.

Do you execute code during the free scan?

Never. The free scan only parses the text you submit. Building a Lean 4 project can run arbitrary code at build time, so Deep Audits always run inside an isolated, disposable machine.

Why not replay every headline proof automatically?

Mathlib-scale replays are expensive: Carlos Toledo reports Comparator peaking at 80 GiB of RAM on OpenAI’s ETH proof and 24 GiB on Anthropic’s.

Can we run SeamCert on pull requests?

Yes. Use our free GitHub Actions workflow & README badge, or see SeamCert for teams for custom CI gates and scheduled audits.