CVE-2026-72711: Lean 4 kernel soundness bug — inference cache poisoning via opaque declarations (0 = 1 demonstrated)
// AI summary
Lean 4 kernel has a soundness bug (CVE-2026-72711) allowing construction of a checked proof of False, such as 0 = 1, without relying on unsafe mechanisms.
// 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, debug.skipKernelTC, or modified .olean files. The proof passes the kernel at maximum checking (--trust=0). The kernel s add_opaque path skips the closure check (check_no_metavar_no_fvar) that the definition and theorem paths perform. A stale...