TI-2026-50947 CVE-2026-72711 · GHSA-fhmq-xvc2-q54h
Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable
Priority MEDIUM 63
The Lean 4 kernel does not check that the body of an opaque declaration is closed.
Vulnerabilities
3 records
TI-2026-51070 CVE-2026-72844 · GHSA-4fhc-8rq3-cjvg
Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections
Priority MEDIUM 63
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 neste…
TI-2026-25224 CVE-2026-32732 · GHSA-6ggm-pwr9-r5h2
XSS in @leanprover/unicode-input-component
Priority LOW 3
Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant.