数学の超難問「ABC予想」をめぐる論争に、決着がつくかもしれない。コンピューターの力を借りて、証明の正否を検証する動きが出てきた。京都大の望月新一教授（56）も、この試みに肯定的だ。証明が正しいかどうかの決断を、数学者ではなく、コンピューターが下すことになるのか。

難解な理論、理解者は世界でも20人

　ABC予想は1985年に提案された超難問で、京大数理解析研究所の望月氏が2012年、証明論文を発表した。だが証明に用いた「宇宙際（うちゅうさい）タイヒミュラー理論（IUT理論）」が難解すぎて、理解できない人が続出。論文に「論理的な飛躍がある」と疑問の声も上がった。

　論文は21年、数学誌に掲載されて「証明」と認められたが、数学界の大半は認めていない状態だ。理解者は20人ほど。理解者側と懐疑派の溝は埋まらず、議論は膠着（こうちゃく）状態が続いている。見かねた実業家が「間違いの証明」に100万ドルの賞金をかけるなど、異常な状態が続いている。

望月氏「最良にして唯一の技術」

　打開策として、望月氏が示しているのが、定理証明支援ソフト「Lean（リーン）」の活用だ。

　Leanは、数学の証明の「正しさ」をコンピューターが判定するツールで、「証明チェッカー」とも呼ばれる。米マイクロソフトリサーチが開発した。証明を構成する定義や概念、論理の流れをすべてプログラムのコードとして記述し、コンピューターがその整合性を1行ずつ検証していく仕組みだ。

　望月氏は10月にHPで公開したリポートで、IUT理論をLeanのコードに翻訳する「形式化」を提案した。

　「形式化は根本的かつ戦略的に重要である」と評価し、ABC予想の証明をめぐる議論が停滞する現状を踏まえ、「数学的真理を社会的・政治的力学のくびきから解放する最良にしておそらく唯一の技術だ」と指摘している（https://www.kurims.kyoto-u.ac.jp/~motizuki/IUT-report-2025-10.pdf）。

　形式化を求める声は過去にもあったが、理論創始者の望月氏が推奨する考えを示したのは初めてだ。

証明の正しさをチェック、Leanとは？

　一般に、証明をコードとして…