Postmortem for Kernel Soundness Bug #14576

A soundness bug in the Lean kernel's handling of nested inductive types with phantom parameters was discovered on July 25 when an AI-assisted "disproof" of the Collatz conjecture exploited it, and was fixed within hours of being formally reported on July 28. The bug only affected direct kernel access through metaprogramming, not normal frontend usage, and remarkably required two separate unrelated bugs to manifest—one in Lean's official kernel and one in the independent nanoda checker—making both need updates for reliable verification.