The vulnerability allows a Lean process to construct an ill‑typed nested inductive through a metaprogram; because the kernel does not verify that a projection expression references the correct structure, the type system is bypassed, producing a proof of false without any axioms and enabling derivation of any proposition, thereby breaking the soundness of the Lean environment.

All releases of Lean 4 distributed by leanprover:lean4 are affected; no specific version range was listed in the CNA data.

The CVSS score of 6.8 indicates moderate severity; the EPSS score is not available and the vulnerability is not listed in the CISA KEV catalog. Exploitation requires in‑process execution of a metaprogram, typically through building a project or importing a malicious Lake dependency, so the attack vector is local and dependent on trusted code inclusion. While the risk to remote users is low, any local build environment that consumes untrusted code is potentially vulnerable and should be mitigated promptly.