望月新一のABC予想証明にギャップ：Leanで形式化不能と確認

Gap in Mochizuki's proof of ABC confirmed by Lean

加藤文元氏らによるLANAプロジェクトは、望月新一氏のIUT理論の核心部分（Theorem 3.11からCorollary 3.12への論証）が形式化不可能であると結論づけ、2026年7月17日の記者会見で発表した。ただし、望月氏自身の説明が進化しているため、最終判断は保留している。また、Scholze-Stixレポート（2018年）との比較も含む分析を公開し、外部の数学者にも理解可能な形でIUT理論の検証を進めている。