Lean’s promise is beautifully severe: tactics can be clever, metaprograms can be weird, proofs can be huge, but the kernel checks the final terms. That bargain is why people trust proof assistants for mathematics, compilers, cryptography, and any software claim too expensive to audit by hand.
A new Lean 4 issue cuts straight through that bargain. The report says the kernel accepted a checked declaration containing a projection whose structure name did not match the value being projected. The reduced reproduction then proves False with no axioms, using the ordinary checked addDecl path. No sorry. No unsafeCast. No disabled kernel type checking. No edited .olean artifact. Just a declaration the system should have rejected.
the proof checker became the object under proof
The public reproduction is ugly in the useful way. It builds expressions directly through Lean’s metaprogramming API, pads two Boolean constants until their hash and approximate depth collide, constructs an inductive declaration whose constructor type contains C projections applied to a W, and feeds the declaration through addDecl. Lean accepts it. The file then derives boom : False by pattern matching on a theorem of type T false, while #print axioms reports that both the intermediate theorem and boom do not depend on any axioms.
The key phrase in the issue is “checked-kernel soundness.” This is the part of the machine that is supposed to survive tactical cleverness. Lean’s own language reference describes the core type theory as implemented in a minimal kernel that checks proof terms, while tactics merely produce terms for that kernel to check. That division is the social contract. A tactic bug should create garbage the kernel rejects. A kernel acceptance bug lets the garbage become certified structure.
a Collatz toy found a real trust bug
The bug surfaced while reviewing a Lean repository claiming a refutation-oriented Collatz result in less than 300 lines. The repository is small enough to look like internet theater, which makes the punchline meaner: toy-looking proofs can still exercise the trusted base in ways ordinary examples miss. The issue author credited the original CollatzLean source and reduced the behavior into a standalone Bug.lean file against Lean 4.34.0-nightly-2026-07-27.
That path matters. A bad theorem about Collatz is forgettable. A minimal reproduction proving False through checked declaration admission is infrastructure news. The useful artifact is the reduction, not the mathematical claim around it.
theorem provers need provenance like package managers
Formal methods people already know this, but the rest of software culture keeps flattening “proved” into a magic adjective. A proof artifact carries assumptions: axioms, universe rules, imported modules, compiler version, kernel implementation, elaboration behavior, native extensions, build flags, and cached artifacts. If a policy, compiler optimization, smart contract audit, cryptographic proof, or safety case treats the certificate as a policy key, the certificate needs provenance.
That does not make Lean broken as a project. It makes the boring engineering visible. Proof assistants earn trust by reducing the trusted computing base, publishing bugs, shrinking reductions, fixing kernels, and making artifacts reproducible across versions. The whole point of a small kernel is that the blast radius can be located. The whole point of open issue trackers is that the locating happens in public.
the weird machine is inside the trusted base
Proof assistants are weird machines in the purest sense: languages where programs construct proofs, proofs construct programs, and tiny rules decide whether whole towers stand. That weirdness is productive. Mathlib exists because automation and abstraction work. Verified compilers exist because small kernels can certify large derivations. The same machinery gives adversarial metaprograms a place to poke.
The right cultural response is neither panic nor priesthood. Panic treats one bug as the death of formal methods. Priesthood treats “machine checked” as a spell users should accept without artifact hygiene. Both are childish. The adult posture is mechanical: pin versions, retain proof artifacts, publish reductions, track soundness advisories, isolate untrusted metaprograms, and make certificate consumers record exactly which checker blessed the term.
A proof of False is funny until the proof checker is underwriting real systems. Then it becomes a reminder that trust minimization still leaves something to trust. The kernel is small because humans need a place to stare.