leanprover lean4 vulnerabilities

Latest leanprover lean4 CVEs

Newest publication first

1. CVE-2026-72711 Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable

   Published 2026-08-24

   Medium·CVSS 6.8 EPSS 0.18%

   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 rej...

2. CVE-2026-72844 Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

   Published 2026-08-20

   Medium·CVSS 6.8 EPSS 0.19%

   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 type...

Sources: CVE.org, NVD, CISA KEV, FIRST EPSS, OSV and public exploit-reference metadata. Product matching comes from the published CVE records. A proof-of-concept means public code exists; it is not evidence of exploitation.