《前編》AIは数学者になれるか

　AIが数学の定理を理解し、証明し、自分で正しさをチェックする――。そんな時代が近づいている。これまで人間が担っていたひらめきや証明、検証にAIなどのコンピューターが挑み始めている。

　東京・銀座の歌舞伎座タワー。7月上旬、12階の一室に数学者30人が集まっていた。東京大や京都大の准教授らや、米国やカナダで活躍する数学者の姿もあった。

　モニターに映し出されていたのは、呪文のような文字列。「Lean（リーン）」と呼ばれるプログラミング言語だ。LeanはAIとは異なり、コンピューターの計算機プログラム。数学の定義や定理などがコードに翻訳されていた。

　目的は、数学の証明の正しさをコンピューターに検証させること。

　「AIと組み合わせれば、証明の道筋を自動化できるかもしれない。数学者の仕事のやり方を、根本的に変えていく可能性を秘めている」

　主催したZEN数学センター（ZEN大学）所長で数学者の加藤文元氏（57）は、そう語る。

　コンピューターの発展に、加藤氏が衝撃を受けたのは、ある画期的な「事件」を知ったことだった。

難解な証明、人ではなくコンピューターが検証

　2020年12月、ドイツ・ボン大のピーター・ショルツ教授（38）は、ネット上に4行のある定理を書き、呼びかけた。「この定理の証明を形式化（検証）してほしい」

　形式化とは、数学の証明の各ステップを、プログラミング言語に書き直すこと。当時、「凝縮数学」という革新理論を構想中のショルツ氏は、理論の中核をなす難解な定理に行き詰まった。半年ほどかけて証明したが、あまりの難しさに自信がなかった。

　ショルツ氏は、「数学のノーベル賞」と言われるフィールズ賞を30歳で受賞し、京都大の望月新一教授（56）が発表した難問ABC予想の証明に異を唱えている数学界のスターだ。

　そんな天才でも確信がもてない定理。「1年の大半は証明に没頭し、狂いそうになった。まだ小さな疑念を抱えている」と当時書き残している。

　証明の正しさを検証するのは本来、人間の仕事だ。数学に限らず、研究成果をまとめた論文は、匿名の専門家による「査読」により誤りがないか検証される。ただ、ショルツ氏は自身の定理は複雑で難しく、人間には不可能だと考えた。

　ショルツ氏の求めに、20人以上の数学者や計算機科学者が救いの手を差し伸べた。ショルツ氏の研究が「リキッドベクトル空間」という概念に基づくことから、検証プロジェクトは、米メタルバンド名をもじって「リキッド・テンサー・エクスペリメント」と名付けられた。

　検証チームは、コンピューターが正しさをチェックする「定理証明支援ソフトLean（リーン）」を使い、ショルツ氏の定理の「形式化」に取り組んだ。

　定理を構成する概念や定義、論理の流れをすべてプログラムのコードとして形式化。そのコードをLeanのコンピューターが機械的にチェックし、途中でエラーが起きなければ、「定理は正しい」と検証が完了する。

　ショルツ氏の定理はコードに徹底的に翻訳され、推論の一つ一つがチェックされた。1年半後の22年7月。Leanがすべての定理の正しさを確認した（https://leanprover-community.github.io/blog/posts/lte-final/）。

　難解な最先端の証明を、査読者に先んじて検証した――。画期的なこの出来事を、米クオンタマガジン誌は「Leanがトップレベルの数学に飛躍した」と報道。ショルツ氏も「驚くべきことだ。確信のなかった定理が検証され、大変興奮している」と絶賛した。

　Leanの「正しさ」が保証されるのは、その検証プロセスが数理論理学によって裏付けられているため。コンピューターによる検証の威力は数学者の中で広まり、4年に1度開かれる国際数学者会議のテーマになるほど注目されてきた。

膨大な時間がかかる形式化、AIが自動化

　では、どんな証明もコンピューターで検証すれば済むと思うかもしれないが、そう簡単ではない。証明をコードに翻訳する「形式化」がとても難しい。

　と言うのも、数学者の証明が「あいまい」なためだ。自明な定理を厳密に証明せず、省略する時もある。言わば、直感に任せて、階段を一気に飛び越えていく。

　このあいまいさがコンピューターの障壁となる。「論文に書かれていない行間を埋め、数学者に自明なことさえ、Leanが理解できるようコードに落とし込む膨大な作業が必要となる」と加藤さんは話す。

　ショルツ氏の定理の場合は、数行の証明に6万行のコードが必要だったと言われる。形式化にかかる時間は、数学者が行う通常の手証明の20～100倍かかるとの指摘もある。

　そのため、検証された証明はごく一部。球をできる限り多く詰め込む方法は「八百屋がオレンジやトマトを積み上げる方法と同じか」という「ケプラー予想」の場合、証明の形式化に費やされた労力は、数十人で10年かかったという。

　そこで登場するのが、AIだ。加藤氏らは、証明をコード化する膨大な作業をAIに担わせようとしている。

　抽象的であいまいな証明を解読して、精密にコード化する作業をAIに自動化させる。コードに誤りがあっても、Leanが正しいか検証するので、学習を繰り返せば精度は高くなっていくはずだ。

AI×Lean＝数学に革命？

　いま、このAIが数学研究のゲームチェンジャーになると言われている。

　生成AIは従来、計算や推論が得意とは言えず、「ハルシネーション（幻覚）」と呼ばれる誤りを生み出す。一方、Leanは誤りを確実に見つけ、正しい方向へ導いてくれる。

　ショルツ氏の定理の検証を主導したオランダ・ユトレヒト大助教のヨハン・コメリン氏は「Leanは、生成AIが作る幻覚の完璧な解毒剤となる。組み合わせることで数学研究に大革新をもたらすだろう」と取材に語った。

　別の専門家は「LeanとAIの融合は、新しい数学を生み出す『知の黒板』になるだろう」と指摘した。

　生成AIはひらめきや発想に強く、Leanは厳密な検証に強い。両者を融合させれば、「証明の完全自動化」も夢ではない。世界で数十以上のチームが研究を進めているとされる。

テレンス・タオ氏「AIは共著者になる」

　世界最高の数学者の一人、テレンス・タオ氏（米カリフォルニア大ロサンゼルス校教授）は、AIやLeanを積極的に使う研究者として知られる。

　2023年、「加法的組み合わせ論の聖杯」と呼ばれてきたPFR予想を証明し、その証明をLeanを用いて検証したことで世界を驚かせた（https://tinyurl.com/4jdxb4ca）。

　Leanから誤りを指摘され、論文を修正したこともあるとブログで明かし、こう述べている。

　「正しく使用すれば、AIは26年までに数学研究における信頼できる共著者になるだろう」