Postmortem for Kernel Soundness Bug #14576

A soundness bug in the Lean kernel involving nested inductive types was reported and fixed within a week, allowing a false "disproof" of the Collatz conjecture. The bug only affects kernel-level metaprogramming and is not reachable through the frontend; it was an implementation error, not a theoretical flaw. Separately, the independent checker nanoda had a distinct bug that was fixed a week earlier, and the proof happened to exploit both.