AIは数学者になれるか 数学界に衝撃、証明検証ソフトLean登場

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

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

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

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

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

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

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

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

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

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

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

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

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

　ショルツ氏の求めに、20人…