CVE-2026-72844

Name of the Vulnerable Software and Affected Versions Lean 4 (affected versions not specified)

Description The kernel fails to verify that the structure named in a projection expression matches the type of the value being projected. Additionally, the environment::add inductive function in src/kernel/inductive.cpp does not type check nested inductive applications replaced by auxiliary types, allowing parametric arguments to bypass checking. A metaprogram running in-process, such as through a malicious Lake dependency or during project builds, can register an ill-typed nested inductive. This is achieved by applying a .proj C 0 projection to a value of an unrelated type W. This leads to type confusion, enabling a proof of False from which any proposition can be derived. The issue can be triggered by padding expressions to cause hash and depth collisions, which bypasses kernel caching.

Recommendations At the moment, there is no information about a newer version that contains a fix for this vulnerability.