Reference page — cumulative record through Sunday, October 4, 2026 UTC. Reference pages update as the archive grows; only dated daily editions are immutable pages of record.
AV AC AT PR UI VC VI VA CVSS EPSS %ile KEV L L N N P N H N 6.8 .0018 6.5 —
AFFECTED Product Versions Fixed lean4 unspecified 4.32.2
TIMELINE Aug 10 Reserved by VulnCheck Aug 20 Published (CNA: VulnCheck) Aug 21 EXPLOIT PUBLISHED — CVE-2026-72844 (leanprover lean4). Public exploit reference added.
The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.
| Date | Event | Detail |
|---|---|---|
| August 10, 2026 | Reserved | Reserved by VulnCheck |
| August 20, 2026 | Published | Published (CNA: VulnCheck) |
| August 21, 2026 | EXPLOIT PUBLISHED | EXPLOIT PUBLISHED — CVE-2026-72844 (leanprover lean4). Public exploit reference added. |
| Vendor | Product / Package | Ecosystem | Version introduced | Fixed |
|---|---|---|---|---|
| leanprover | lean4 | — | — | 4.32.2 |
Authoritative record: CVE-2026-72844 at cve.org
Vendors: leanprover
Weaknesses: CWE-843
This is a reference page, not a dated page of record. It assembles the complete lifecycle of CVE-2026-72844 from the CVE Program record, NVD enrichment, the CISA KEV catalog, EPSS, and OSV advisories. The box score's numbers (CVSS, EPSS, KEV status) are current as of Sunday, October 4, 2026 UTC and are re-derived as the archive grows; only dated daily editions are immutable pages of record. The authoritative source for this identifier is cve.org.
