# CVE-2026-72844: Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

Status: published. Published: 2026-08-20. Updated: 2026-11-08.

The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.

## Remediation

- fix: The reporting source identifies this reference as a patch. Check the advisory for affected versions and supported release branches. (source: CNA: VulnCheck) — https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808
- fix: The reporting source identifies this reference as a patch. Check the advisory for affected versions and supported release branches. (source: CNA: VulnCheck) — https://github.com/leanprover/lean4/pull/14577

## Affected products and versions

- leanprover / lean4: ≥ 0; < 4.32.2 (affected, semver); 4.32.2 (unaffected, semver); 4.33.0-rc1 (affected, semver). Source: CNA: VulnCheck

## Severity and prioritization

- CVSS 3.1: 6.3 (medium); CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N; source: CNA: VulnCheck

- CVSS 4.0: 6.8 (medium); CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N; source: CNA: VulnCheck

- CISA KEV: No listing in collected sources

- EPSS: 0.19% as of 2026-11-08; percentile 8.31%

- SSVC: exploitation poc; automatable no; technical impact partial; source ADP: CISA-ADP

- Weaknesses: CWE-843

## Exploit evidence

- exploit: https://github.com/endrazine/lean-cve-poc (CNA: VulnCheck)
- exploit: https://github.com/xrchz/CollatzLean (CNA: VulnCheck)

## References

- https://github.com/leanprover/lean4/issues/14576 (CNA: VulnCheck; issue-tracking)

- https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808 (CNA: VulnCheck; patch)

- https://github.com/leanprover/lean4/pull/14577 (CNA: VulnCheck; issue-tracking, patch)

- https://github.com/endrazine/lean-cve-poc (CNA: VulnCheck; exploit)

- https://github.com/xrchz/CollatzLean (CNA: VulnCheck; exploit)

- https://www.openwall.com/lists/oss-security/2026/08/02/1 (CNA: VulnCheck; third-party-advisory)

- https://github.com/leanprover/lean4 (CNA: VulnCheck; product)

- https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections (CNA: VulnCheck; third-party-advisory)

- http://www.openwall.com/lists/oss-security/2026/10/26/2 (ADP: CVE)

## Provenance

- CNA: VulnCheck: https://www.cve.org/CVERecord?id=CVE-2026-72844; retrieved 2026-11-08; source updated 2026-11-08

- FIRST EPSS: https://api.first.org/data/v1/epss?cve=CVE-2026-72844; retrieved 2026-11-08; source updated Not reported

Revision: c4dbd23396d08ed07147349b3f3e6c45519b2066c4c8419d4e6e66e483fd2200

Canonical: https://y2.dev/cve/CVE-2026-72844

## Agent and API access

Public CVE pages, Markdown, and JSON are free to read without an account or API key.

- Public catalog: https://y2.dev/cve/index.json. Follow nextCursor with the same search, filters, sort, and limit (1–100). A null cursor marks the end.

- WebMCP: search_cve_disclosures, get_cve_disclosure, get_cve_page_markdown, get_y2_cve_access. Available in compatible browsers.

- Cyber API: https://api.y2.dev/api/v2/cyber/cves and https://api.y2.dev/api/v2/cyber/cves/{cveId}.

- Y2 Pro or Elite: create a workspace API key with the intel:cyber scope and send Authorization: Bearer <Y2_API_KEY>. Setup: https://y2.dev/docs/api/create-key.

- x402: Pay per request without an account or API key. Omit Authorization, read the HTTP 402 PAYMENT-REQUIRED challenge, validate its current requirements, and retry with PAYMENT-SIGNATURE through an authorized payment client. These browser tools never make payments. Guide: https://y2.dev/docs/api/x402.

- OpenAPI: https://y2.dev/api/openapi.yaml. Agent access metadata: https://y2.dev/cve/agent.json.

Collected public records only. Check source status for coverage and freshness.