A flaw in the Lean 4 kernel allows the creation of opaque declarations whose bodies contain free variables that are not present in the local context. By exploiting the kernel’s caching mechanism, a metaprogram can cause the kernel to accept an opaque constant of type False. From this false proposition any statement can be derived, effectively granting an attacker the ability to prove arbitrary propositions within the Lean environment. The vulnerability is a pure logical flaw; it does not involve traditional code execution or network abuse, but it undermines the soundness of Lean’s proof system.

The issue affects Lean Prover’s Lean 4 product. All releases prior to version 4.32.2 are vulnerable because the closure check for opaque declaration bodies was omitted. Users of these earlier versions are at risk, while 4.32.2 and later include a fix that enforces the necessary closure validation.

The CVSS score of 6.8 indicates a moderate severity logical flaw. No EPSS score is available, and the vulnerability is not listed in CISA’s KEV catalog. Exploitation requires the ability to run malicious Lean code or metaprograms in the environment, so the likely attack vector is local execution of untrusted Lean code. Once the kernel accepts an opaque declaration of type False, the attacker can derive any proposition, compromising the soundness of the system.