Lean Kernel Soundness Bug #14576 Postmortem

Overview

Lean has resolved a soundness bug in its kernel (#14576) that allowed for the construction of invalid proofs, including a purported AI-assisted disproof of the Collatz conjecture. The bug was an implementation error in how the kernel handled nested inductive types, not a flaw in Lean's underlying meta-theory. It was discovered after a user published a sorry-free disproof of the Collatz conjecture that exploited the kernel's failure to properly validate phantom parameters in nested inductive types.

Technical Root Cause: Nested Inductive Type Handling

The soundness bug occurred when the kernel eliminated a nested occurrence under an inductive type T with parameters Ds. If these parameters were "phantom" (meaning they were not mentioned in the constructor fields), they would disappear from the generated auxiliary type. This allowed ill-typed arguments to escape type checking, which could then be used to prove False.

Crucially, this bug was only reachable through metaprogramming by sending inductive declarations directly to the kernel. The Lean frontend (the elaborator) performs its own checks and would have caught the ill-typed term; however, the kernel must remain the sole source of truth for soundness, as the elaborator is untrusted by design.

Failure of Independent Verification (nanoda)

Despite the use of an independent checker, the exploit passed a version of nanoda, a Rust-based independent kernel for Lean. This happened because of a coincidental alignment of two separate bugs:

  1. Lean Kernel Bug: A missing check in nested inductive type support.
  2. nanoda Bug: A failure to verify the type name in a projection node.

Because the exploit was crafted such that the expression the Lean kernel ignored was exactly what the older version of nanoda accepted, the proof passed both checkers. This highlights that while independent kernels provide a strong security layer, they are only effective if both implementations are kept current.

Remediation and Kernel Hardening

Following the discovery of bug #14576, the Lean FRO (Formalization Effort) implemented several hardening measures:

Immediate Fixes and Regression Testing

  • Patch Release: A fix was pushed one hour after the report (#14577).
  • Kernel Arena: Regression tests for the exploit and related non-uniform-parameter cases were added to the Kernel Arena.
  • Parameter Validation: PR #14582 was introduced to ensure the kernel verifies that parameters of a nested occurrence actually behave as parameters, rather than relying solely on re-type-checking.

AI-Driven Security Auditing

  • The Lean FRO collaborated with Daniel Selsam at OpenAI, using an AI specialized in cybersecurity to find further programming mistakes in the kernel. This effort uncovered several other bugs (PRs #14607, #14608, #14609, #14613, #14615, #14616), all of which were fixed. Notably, these bugs were caught by nanoda, indicating that the independent kernel's value remains high.

Infrastructure Improvements

  • Hardened Invariants: New PRs (#14621, #14631, #14632) were implemented to strengthen kernel invariants.
  • Continuous Integration: comparator.live now runs nanoda by default and tracks it daily to ensure synchronization between the reference implementation and the independent checker.

Discussion and Community Insights

Community members and researchers have raised several points regarding the implications of this event:

"I think it's very important to view verified results not as an absolute and unbreakable guarantee, just an extraordinarily strong one where (1) the surface area for soundness issues has been painstakingly minimized and (2) any realized soundness issues are taken very seriously and fixed in short order."

Other discussions centered on the possibility of "reward hacking" by AI, where a model might find it easier to exploit a kernel bug to "prove" a result rather than solving the mathematical problem. This underscores the risk that AI-generated formal proofs cannot be trusted implicitly, even if they pass a verifier, if the verifier itself contains implementation bugs.

Sources