Lean 4 kernel forges proofs via nested projections (CVE-2026-72844)
Original title: CVE-2026-72844: Lean 4 kernel soundness bug — forging proofs via nested inductive projections (0 = 1 demonstrated)
A projection can name a structure that does not match the projected value, yielding a checked proof of False.
Jonathan Brossard reported CVE-2026-72844, another Lean 4 kernel soundness bug. The kernel does not check that the structure named in a projection matches the type of the value being projected. environment::add_inductive in src/kernel/inductive.cpp also did not type-check nested inductives, according to the truncated post. A proof of False, including 0 = 1, is accepted without axioms, sorry, unsafeCast, or modified .olean files.
Unconfirmed: The snippet cuts off during the description of nested inductive type-checking, so the full conditions are not shown.
- Posted to oss-security on October 25 by Jonathan Brossard.
- The mismatch is in projection structure names versus value types.
- The cited code path is environment::add_inductive in src/kernel/inductive.cpp.
- No affected or fixed version is stated.
Impact: Checked proofs of false propositions are accepted
| Product | Affected |
|---|---|
| Lean 4 | — |
Vulnerabilities mentioned
All| CVE | Vulnerability | CVSS | EPSS | Signals | Published |
|---|---|---|---|---|---|
| CVE-2026-72844 | The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and… | 6.8 | <1% |
From the original article
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.
seclists.org
A short excerpt; the article and its images belong to the publisher. Summary, key facts and assessment above are AI-written from the article and can be wrong.