CVE-2026-72844: Access of Resource Using Incompatible Type ('Type Confusion') in leanprover lean4

The Lean 4 kernel does not properly verify type consistency in projection expressions and nested inductive applications, allowing a metaprogram to register an ill-typed nested inductive type. This results in type confusion that can produce a proof of False without axioms, effectively breaking the soundness of the proof system. The vulnerability is exploitable only by running a metaprogram within the Lean process, such as during project builds or when importing malicious dependencies. The published proof of concept uses hash collision techniques to bypass kernel caching, but this is a method to reach the flaw rather than the root cause.

An attacker able to run a metaprogram in the Lean 4 process can exploit this vulnerability to cause type confusion, resulting in a proof of False without axioms. This undermines the soundness of the proof system, allowing derivation of arbitrary propositions, which compromises the integrity of proofs generated by Lean 4. There is no indication of direct impact on confidentiality or availability. Exploitation requires local code execution within the Lean environment.

Patch status is not yet confirmed — check the vendor advisory for current remediation guidance. Until an official fix is available, avoid running untrusted metaprograms or importing untrusted dependencies in the Lean 4 environment to mitigate risk.