Tech News Daily

数学の未解決問題コラッツ予想を巡り、7月25日にRamana Kumar氏がAI支援による「反証」を公開したことが発端となった。3日後、Kiran Gopinathan氏がこの反証を検証したところ、証明全体を最小限のFalse証明にまで還元できることを発見し、定理証明系LeanのカーネルにIssue #14576として報告した。原因は、コンストラクタで実際には使われない「幽霊パラメータ」を持つ入れ子の帰納型をカーネルが処理する際、型検査の過程でこのパラメータの情報が失われ、本来型の合わない引数が検証をすり抜けてしまうという実装上のバグだった。開発チームは、これはLeanの基礎となるメタ理論そのものに欠陥があるわけではなく、あくまで実装レベルの見落としだと強調している。さらに調査の過程で、独立実装のRust製検証器nanodaも、射影ノードの型名を検証していないという別の欠陥を抱えており、同じ攻撃を素通りさせてしまうことが判明した。カーネルとnanodaの両方を修正して初めて、この攻撃経路は完全に塞がれたことになる。開発チームは報告からわずか1時間で修正版をデプロイし、その後AI支援によるセキュリティ解析を追加で実施した結果、無関係な脆弱性を5件発見・修正するという副産物も得た。今後の再発防止として回帰テストを追加し、nanodaを比較ツールとしてCIに組み込んだ。