数学の超難問「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とは？

　一般に、証明をコードとして形式化できると、あいまいな部分がなくなり、コンピューターがわずかな矛盾すら検出できるようになる。結果として、証明が正しいかどうか判定できる。

　正しさが論理で確認できるのが数学。コンピューターによる「正しさ」が保証されるのは、その検証プロセスが数理論理学によって裏付けられているためで、証明が複雑化している近年、Leanなどの証明チェッカーが注目を浴びている。

　決定的な役割を果たした例もある。

ケプラー予想、四色定理の検証でも活躍

　1611年にヨハネス・ケプラーが提案した「ケプラー予想」は、球を最も効率よく詰め込む方法は「八百屋がオレンジやトマトを積み上げる方法と同じか」という問題だ。1998年、300ページ近い証明論文が数学誌に投稿され、12人の数学者が4年かけて検証したが「証明の正しさは99%」としか確信が持てなかった。

　そこで証明チェッカーの検証が始まった。論文は約10年かけコードに形式化されて検証が完了。数学界が証明を認めるという経緯をたどった。

　どんな地図でも四色で塗り分けられるという「四色定理」の証明（1976年）も、計算機を用いた手法が本当に正しいのか議論が起きたが、その手法が証明チェッカーで検証され、批判は収まった。

　同じように、ABC予想の証明の正否も、検証されるのかが焦点となる。

　Lean研究の第一人者である英インペリアル・カレッジ・ロンドンのケビン・バザード教授（数論）は取材に対し、期待を示した。

　「IUT理論が正しいなら形式化を妨げる障害はない。非常に大きな成果につながる可能性はある。人工知能（AI）の技術も活用でき、挑戦の価値はあるだろう」

　AIは、人間では膨大な労力がかかる形式化の作業を自動化できる可能性があり、こうした技術がIUT理論の形式化に追い風になるとの見方もある。

「予想外の熱意に勇気づけられた」

　ただ、「理論は正しい」と考えている望月氏はなぜ、コンピューターに力を借りる必要があるのか。

　背景には、混乱が続く現状を従来の方法では打開できていないという事情があるとみられる。望月氏は、証明の正しさを評判や多数意見に委ねるのではなく、コンピューターによる論理的検証によって確かめることが、混乱を解消する手立てになるとみているようだ。リポートで次のように述べている。

　「IUT理論が公開されて以降、私や他の数学者がメールや対面、勉強会などで、他分野の数学者たちと議論を試みてきたが、その多くは成功しなかった。この理由から、Leanの形式化という目標が、IUT理論の数学的内容を明確化し、記録するという点において自然な次のステップとなる」

　リポートによると今年7月、望月氏は東京であったLeanの勉強会に出席し、IUT理論の形式化のメリットを確信したという。形式化に興味を持つ研究者たちに触れ「予想外の熱意に深く感銘を受け、勇気づけられた」とも書いている。

　ただ、自らがIUT理論の形式化に取り組むかどうか、望月氏はレポートで明言していない。

Leanの実力、懐疑派ショルツ氏も太鼓判

　では、懐疑派が納得するような決着がつくのか。

　ABC予想の証明を否定しているフィールズ賞受賞者、独ボン大のピーター・ショルツ教授（37）は、Leanの威力を身をもって実感している数学者だ。

　5年前、難解な定理の証明を一人で成し遂げたショルツ氏は、自信が持てずLeanの専門家に検証を依頼したことがある。20人以上が参加し、証明の最後の5行だけで、コード6万行が必要だったというが、1年半かけて証明の正しさが検証された、という経緯がある。

　ただ、道のりは平坦（へいたん）ではない。証明をコードに直す形式化は、概念や定理などの複雑な式をコードに翻訳する骨の折れる作業で、ケプラー予想の場合は数十人で10年かかった。

証明が真なら「数学界は謝罪することに」

　今回のIUT理論は、700ページ以上あり、「どこがわからないのかさえわからない」と言われた難しさだ。30年前に解決した「フェルマーの最終定理」も、証明を形式化する作業はまだ終わっていない。

　ショルツ氏の定理の検証を主導したヨハン・コメリン氏（オランダ・ユトレヒト大助教）は、方法はあると指摘する。IUT理論の中で、数学的に異論のない大部分を「ブラックボックス」として検証せず、理論の主要部分のみ検証する方法だ。「この方法なら5人ほどのチームで1～2年で大きく進展が見えるのではないか」と取材に答えた。

　ただ、IUT理論をコード化できても、その意味や解釈をめぐって新たな論争が起こる可能性もある。「IUT理論を記述したコードが、望月教授の意図した主張と正確に対応しているかを確認することは非常に難しいこともある」という。

　どのような結末を迎えるのか。

　バザード氏は、ABC予想の証明は「誤り」と判定される可能性や、作業量が膨大で検証が頓挫する可能性を上げている。そしてもう一つの可能性は、証明が「正しい」と検証されること。

　「そうなれば大きな驚きとなり、数学界は望月氏に謝罪することになるでしょう」

　望月氏にもメールで問い合わせたが、1週間以上たっても返事はなかった。