The Lean 4 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 escape checking. A metaprogram can exploit this by registering an ill-typed nested inductive whose constructor applies a projection to a value of an unrelated type. This type confusion is admitted by the kernel through the normal checked addDecl path without requiring unsafe flags or modifications. The result is a proof of False carrying no axioms, from which any proposition can be derived. The published proof of concept uses hash and depth collisions to defeat kernel caching, but this technique is not the root cause. Exploitation requires running a metaprogram in-process, such as building a project or importing a malicious Lake dependency.

This vulnerability allows an attacker who can run a metaprogram inside the Lean 4 process to create ill-typed nested inductive declarations that lead to type confusion. This results in a proof of False without axioms, effectively breaking the soundness of the proof system and allowing derivation of any proposition. There is no impact on confidentiality or availability, but the integrity of proofs is compromised.

Patch status is not yet confirmed — check the vendor advisory for current remediation guidance. Until a fix is available, users should avoid running untrusted metaprograms or importing untrusted dependencies that could exploit this vulnerability. No official fix or temporary workaround is currently documented.