Lean カーネルの健全性バグ #14576：AI によるコラッツ予想の「反証」を許容した経緯

Postmortem for Kernel Soundness Bug #14576

Lean カーネルに存在したバグが、AI 支援で生成されたコラッツ予想の誤った反証を許容する事態を招きました。この問題は、独立したチェッカー nanoda にも別の欠陥があったため検出されませんでした。これは実装のバグであり、Lean のメタ理論の欠陥ではありません。現在は修正済みですが、メタプログラミングの制限は健全性の確保には効果的ではないと結論付けました。