What the July 2026 Lean kernel bug meant for us, and what we did in the week it landed

On July 28, 2026, a fix merged for a soundness bug in the Lean 4 kernel: nested inductive types with phantom parameters could bypass the type checker, enabling an axiom-free proof of False. Within a day, an AI-generated “proof” of the Collatz conjecture exploiting it was public — and dead. It died fast because Lean artifacts are re-checkable by anyone. That is the lesson most coverage missed: the prover was never trusted; the checker was, and the checker's bug was found by checking.

Our exposure when the news broke

Our Lean pin was eighteen minor versions behind the fix. Our library contains roughly ten parametric inductive types whose exposure to the bug class was not settleable by reading — and “we inspected it and it looked fine” is not a verdict our own rules accept. Our axiom-audit gates are structurally blind to kernel-implementation bugs, because a proof built on one carries a clean axiom footprint. That blindness was already recorded in our gate registry's blindness column; this was the week it stopped being theoretical.

What we did, in order

1. Locked the toolchain identity as a gated artifact, both directions — a silent version change fails the build, and the gate states what it checks: identity, not soundness.
2. Added kernel replay of our compiled environment through an external checker to CI, which fired on first contact: 26 orphaned build artifacts asserting declarations our source no longer makes. Not the bug we installed it for. A real defect anyway.
3. Migrated the pin v4.14.0 → v4.32.2 through six intermediate versions, each accepted against a pass bar written before the step was walked. End-to-end result: 57 headline theorems, axiom footprints identical across eighteen versions of kernel drift, measured against a frozen v4.14.0 baseline — never chained through an intermediate, because chaining would let a drift launder itself across two comparisons.

What we will not claim

Immunity. Our current pin is patched but externally unreplayed: the independent kernel reimplementation is broken at every version that can read our environment — it segfaults on Lean's own core library, with no Monogate code involved — which we reported upstream with minimal reproductions. Until that is fixed or the alternative checker gains a matching tag, v4.28.0 stands sealed as our last dual-verified position, and our current state is graded accordingly in the migration record: accepted, with two criteria formally recorded as unmeasured and the reason named.

The compensating control, unchanged since before the incident: no headline claim rests on the prover or the checker alone — each is also enumerated, numerically certified, or measured on physical hardware, and a false theorem would have to defeat those independent oracles too.

Standing consequence

Safety, in a verification system, is not a state. It is an enumerated exposure with a watch on every open item. Ours is public, and the accountability page is where it drifts loudly instead of silently.

Artifacts: upstream issue (lean4lean #17) · migration plan and pass bar · axiom ledger · migration log and snapshots (unpublished — see disclosure above).

← Back to Accountability