Lean 4 kernel bug lets metaprograms forge proofs of False

A soundness bug in the Lean 4 theorem prover kernel allowed a malicious metaprogram to make the kernel accept invalid proofs, including proofs of False and 0 = 1, with no axioms and full kernel checking still enabled.

Jonathan Brossard disclosed the issue. The kernel failed to ensure that projection expressions in nested inductive type declarations referred to the correct structure. An in-process metaprogram could register an ill-typed inductive whose constructor applied a projection to a value of the wrong type. Paired with an expression hash collision, that type confusion yielded a fully checked, axiom-free proof of False, from which any statement follows.

The path was the ordinary checked declaration interface used when Lean adds new definitions. Exploitation required only that a metaprogram run inside the Lean process, for example during a project build or while importing a dependency. Every Lean 4 release through v4.31.0 was affected, as were nightlies through 2026-07-27. The fix shipped in the 2026-07-29 nightly.

The practical stakes sit with anyone treating Lean proofs as high-assurance evidence. Common Criteria (ISO/IEC 15408) and related regimes such as DO-178C and ISO 26262 place machine-checked formal proofs at the top of the assurance ladder for national security systems, cryptographic modules, avionics, and automotive software. A hole in the checker undercuts the trust those certifications place on the proofs until the proofs are revalidated on a corrected kernel.