Lean 4 kernel accepts false proofs via opaque declarations (CVE-2026-72711)
A checked proof of False, including 0 = 1, passes the Lean 4 kernel at --trust=0 without axioms or unsafe features.
Stories per day · 30 days
1 stories, newest first · one card per story