A soundness bug in the Lean kernel (#14576) was discovered and fixed, allowing an ill-typed argument to bypass type checking in nested inductive types with phantom parameters. The bug was exposed when an AI-generated 'disproof' of the Collatz conjecture was found to exploit it, though the independent nanoda checker also had a separate bug that failed to catch it.
Background
The Lean theorem prover is a widely used interactive theorem prover and programming language. The kernel is the core component responsible for checking the validity of proofs, making soundness bugs particularly critical.
- Source
- Lobsters
- Published
- Aug 2, 2026 at 05:51 AM
- Score
- 8.0 / 10