CVE-2026-72844: Lean 4 kernel soundness bug — forging proofs via nested inductive projections (0 = 1 demonstrated)
// AI summary
Lean 4 kernel has a soundness bug (CVE-2026-72844) allowing construction of a checked proof of False, demonstrating 0 = 1 without axioms or unsafeCast.
// from the source
Posted by Jonathan Brossard on Oct 25 1. Summary ========== A soundness bug in the Lean 4 kernel allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1 — without axioms, sorry, unsafeCast, or modified .olean files. The kernel does not verify that the structure named in a projection expression matches the type of the value being projected. Additionally, environment::add_inductive in src/kernel/inductive.cpp did not type-check nested...