Lean 4: Kernel soundness vulnerability via nested inductive projections (CVE-2026-72844)

A soundness vulnerability in the Lean 4 kernel (CVE-2026-72844) enables the construction of checked proofs of 'False' (e.g., 0 = 1). The flaw stems from two primary issues: the kernel fails to verify that the structure named in a projection expression matches the type of the value being projected, and the environment::add_inductive function in src/kernel/inductive.cpp fails to perform necessary type-checking for nested definitions. This compromise undermines the foundational logical guarantees of the theorem prover. No further update has been provided regarding fixed versions or mitigation timelines beyond the initial disclosure.

Impact

This vulnerability allows for the creation of arbitrary proofs of logically false propositions within the Lean 4 environment. It does not require the use of explicit axioms, the sorry keyword, unsafeCast operations, or the modification of .olean files, allowing the exploit to bypass standard verification checks.

Recommendation

• Inventory environments utilizing Lean 4 for formal verification or critical logical proofs.
• Monitor the official Lean 4 repository and the oss-security mailing list for the release of security patches or official mitigation guidance.
• Review critical proof developments that depend on the integrity of the Lean 4 kernel; consider re-verifying proofs using patched versions once updates are available.