CVE-2026-72844: Lean 4 kernel soundness bug — forging proofs via nested inductive projections (0 = 1 demonstrated)

Summary by Cyber Security News26 Oct 2026, 01:12 CET

About this summary. This is a short excerpt from the description that oss-security published with its article. Cyber Security News did not report or verify the underlying story. Read the original: https://seclists.org/oss-sec/2026/q4/379

Posted by Jonathan Brossard on Oct 25 1. Summary A soundness bug in the Lean 4 kernel allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1 — without axioms, sorry, unsafeCast, or modified .olean files. The kernel does not verify that the structure named in a projection expression matches the type of the value being projected.

Read the full article at oss-security →

Source attribution: headline and facts are from oss-security (seclists.org). Summary method: excerpt of the source description. See our source attribution policy.

Related coverage

Node.js security release pre-alert

Open-source file sync tool rsync 3.5.2 fixes a CPU exhaustion flaw

Ghostunnel: Open-source TLS proxy with mutual authentication

Rails security releases: 8.0.5.2 and 8.1.4.1

Fixed Detectors, Moving Code: How Well Do Static Security Analyzers Hold Up over a Decade of C/C++ Evolution?

When Debate Amplifies Risk: Social-Bias Vulnerabilities in Multi-Agent Safety Deliberation