5 hours ago
- A soundness bug in the Lean kernel (#14576) was reported and fixed, involving nested inductive types.
- The bug allowed a proof of False via ill-typed arguments in phantom parameters, only reachable through metaprogramming.
- Two independent bugs in the official kernel and nanoda checker were needed for the exploit; both have been fixed.
- Practical consequence: independent kernel checking requires current versions of both checkers.