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.
CVE-2026-72711
leanprover lean4 — Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable
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 —
TIMELINE
Aug 10 Reserved by VulnCheck
Aug 24 EXPLOIT PUBLISHED — CVE-2026-72711 (leanprover lean4). Public exploit reference added.
Aug 24 Published (CNA: VulnCheck)
Aug 29 EXPLOIT PUBLISHED — CVE-2026-72711 (leanprover lean4). Public exploit reference added.
Description
The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.
Lifecycle
Complete event history — 4 events, chronological
| Date | Event | Detail |
|---|
| August 10, 2026 | Reserved | Reserved by VulnCheck |
| August 24, 2026 | EXPLOIT PUBLISHED | EXPLOIT PUBLISHED — CVE-2026-72711 (leanprover lean4). Public exploit reference added. |
| August 24, 2026 | Published | Published (CNA: VulnCheck) |
| August 29, 2026 | EXPLOIT PUBLISHED | EXPLOIT PUBLISHED — CVE-2026-72711 (leanprover lean4). Public exploit reference added. |
Affected
Affected products and packages — 1 row
| Vendor | Product / Package | Ecosystem | Version introduced | Fixed |
|---|
| leanprover | lean4 | — | — | — |
About this page
This is a reference page, not a dated page of record. It assembles the complete lifecycle of CVE-2026-72711 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.
