Skip to content
OpenAdvisories

Vendor

leanprover

3 known vulnerabilities.

leanprover at a glance

Last 12 months
3
Critical · all time
0
Exploited · all time
0
Public exploit · all time
2
New vulnerabilities per month · last 12 months
0 1 2 December 2025: 0 vulnerabilities Dec 2025 January 2026: 0 vulnerabilities February 2026: 0 vulnerabilities March 2026: 1 vulnerability Mar April 2026: 0 vulnerabilities May 2026: 0 vulnerabilities June 2026: 0 vulnerabilities Jun July 2026: 0 vulnerabilities August 2026: 2 vulnerabilities September 2026: 0 vulnerabilities Sep October 2026: 0 vulnerabilities November 2026: 0 vulnerabilities
Show as table
MonthVulnerabilitiesCritical
Nov 202600
Oct 202600
Sep 202600
Aug 202620
Jul 202600
Jun 202600
May 202600
Apr 202600
Mar 202610
Feb 202600
Jan 202600
Dec 202500
Nov 202500
Oct 202500
Sep 202500
Aug 202500
Jul 202500
Jun 202500
May 202500
Apr 202500
Mar 202500
Feb 202500
Jan 202500
Dec 202400

Products

lean4 2 vscode-lean4 1
All Critical High Medium Low Exploited only Public exploit

3 results · Feed

  • Medium 6.3
    CVE-2026-72711 Public exploit

    Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable

    The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the loc…

    leanprover lean4
  • Medium 6.3
    CVE-2026-72844 Public exploit

    Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

    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 repla…

    leanprover lean4
  • None 0.0
    CVE-2026-32732

    XSS in @leanprover/unicode-input-component

    Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant. Projects that use @leanprover/unicode-input-component are vulnerable to an XSS exploit in 0.1.9 of the package and lower. The component re-inserted text in the input el…

    leanprover vscode-lean4 @leanprover/unicode-input-component npm