CVE-2026-72844

MediumCVSS 6.3

Published: 20/08/2026(UTC)Updated: 21/08/2026(UTC)Translated: 22/08/2026(UTC)NVD NIST

Exploitation Probability (EPSS)

Low risk

0.12%

2th percentile - higher than 2% of all known CVEs

Summary

The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and does not type check nested inductive applications replaced by auxiliary types. A metaprogram can register an ill-typed nested inductive, leading to type confusion and a proof of False without axioms.

Risk Assessment

An attacker can derive any proposition, potentially leading to logical integrity breaches and possibly remote code execution in the Lean process.

Recommendation

Update Lean 4 to a patched version or avoid running untrusted metaprograms and importing malicious Lake dependencies.

Other vulnerabilities in Lean 4

CVE-2026-72711Medium
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. A metaprogram can exploit this to accept an opaque declaration with a free variable, leading to an opaque constant of type False and proving any proposition. Fixed in 4.32.2.

Original NVD description (English source)

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.