米AI企業アンソロピックは、同社のAI「Claude（クロード）」が数学の難問「フェルマーの最終定理」の証明を、コンピューターで検証可能な形式に11日間でまとめ上げたと発表しました。AIが最先端の数学に踏み込む時代の到来を告げる成果です。
1,300万行のコードを自動生成
アンソロピックが9月4日に公表した研究によると、ClaudeはプログラミングされたAIエージェントを数十体展開し、証明支援言語「Lean（リーン）」で1,300万行のコードを書き、2万9,500もの中間定理を証明しながら作業を進めました。作業全体で生成された文章量は60億トークンにのぼります。
360年越しの難問を形式化
フェルマーの最終定理は、17世紀に提示されてから約360年間、数学者を悩ませ続けた難問です。1990年代に英数学者アンドリュー・ワイルズ氏が証明しましたが、その論理をコンピューターが逐一検証できる形に「形式化」する作業は、人手では膨大な時間を要するとされてきました。
ただし「自律的」という表現には注意も必要です。Claudeの最初の形式化は失敗し、成功には長時間の作業を最適化する第三者製ツール「Prove2Me」の導入が欠かせませんでした。またアンソロピックは、英インペリアル・カレッジ・ロンドンのケビン・バザード氏が率いるプロジェクトや数学ライブラリ「Mathlib」の成果106ファイルを土台として利用したことを明らかにしています。バザード氏はこの成果を「並外れた自動形式化の達成」と評価しました。
日本への影響
この成果は、日本の研究現場やソフトウェア産業にも大きな示唆を与えます。数学の証明を機械で検証する技術は、金融システムや自動運転、暗号といった「誤りが許されない」分野のプログラム検証に応用でき、ソニーグループや富士通など日本企業が力を入れるソフトウェアの品質保証にも波及する可能性があります。また、日本の大学や理化学研究所などの研究機関では、AIを研究の共同作業者として活用する動きが加速するとみられ、研究のあり方そのものが変わっていくでしょう。一方で、AIが高度な知的作業を担うようになれば、数学者や技術者に求められる役割も変化するため、教育の現場ではAIを使いこなす力の育成が一層重要になると考えられます。
まとめ：AIが人類最難関の数学に挑む時代、私たちはその力をどう活かすかが問われていますね。
出典：
Anthropic – Formalizing Fermat’s Last Theorem
SiliconANGLE – Anthropic uses Claude to formalize proof
