>>476-479
ホイヨ
https://xtech.nikkei.com/atcl/nxt/column/18/03572/040200002/
AIがもたらす「数学」の転換点 第1回
AIが数学の未解決問題を相次いで解決、証明の鍵は「形式化」
久富 早織 日経クロステック/日経コンピュータ記者 2026.04.06

　AI（人工知能）が数学界でも注目を集めている
AIの能力や影響を研究する非営利機関のEpoch AI（エポックAI）は2026年3月5日、米OpenAI（オープンAI）のGPT-5.4 Proが「ディオファントス方程式」において有限性問題の一部を解いたと公表した

今回の証明は「正しい」ものとして、発表直後から名だたる数学者からの称賛が相次いだ。なぜこうした反応が起きたのか。背景にあるのが、今の数学界を変える可能性がある「証明の形式化」だ。ZEN数学センターの所長を務める、ZEN大学の加藤文元教授に話を聞いた

「疑う余地なし」とされた鍵は「形式化」
　728番の証明が「正しい」とされたことについて、ポイントとなるのが、証明をコンピューターが自動で検証できる形に書き表す「形式化」だ。今回の証明に用いられたのは数学の証明支援ツールの1つである「Lean（リーン）」である。Leanによって形式化された証明は、自然言語による証明とは異なり、曖昧さや省略が一切ない。証明の過程や計算も省かずに表す必要があるという

　Leanは完全に形式的な推論規則に基づくため、証明が正しいか否かはシステムが自動でチェックする。「Leanで書かれた証明がエラーなく通れば、それは『正しい』ことを意味し、疑う余地はない」（加藤氏）

　加藤氏は、AIが形式化を活用できるようになった背景の1つとして、「Leanで使うライブラリーが蓄積してきたことが大きく貢献した」と見ている。728番の証明も、ライブラリーが少しずつ拡充してきたことが支えた

　数学が得意でも、形式化には全く別の知識を要する。表記が自然言語とは異なるため、Leanのコードを書ける数学者が必要だ。加藤氏は「形式化できる人間は世界的にも少なく、現在は20〜30人で形式化作業を担っている」と話す

「本当の意味でAIが数学問題を解いた」
　728番の解決には、もう1つ新しい点がある。「AIによる問題文自体の改良」だ。加藤氏によると、「そもそも数学の未解決証明問題の多くは問題文が不完全で、そのままでは解けない」という

加藤氏は今回の728番の解決について「ネット上の既存情報の寄せ集めとは異なり、AIが問題文自体を改良しながら解決まで進んだ。本当の意味でAIが問題を解いたと言ってよいのでは」と評価する。数学界のノーベル賞ともいわれるフィールズ賞を受賞したテレンス・タオ氏も、自身のSNSで「AIがほぼ自立的に問題を解いた」と評価した

　現在、加藤氏の研究室では、人間が自然言語で書いた数学論文をAIでLeanコードへ自動翻訳する研究を行っている。これは単なる翻訳ではなく、人間が省略した何百もの論理のステップを復元する作業であり、通常の言語翻訳とは全く違う難しさがあるという。加藤氏はライブラリーの蓄積とAIの組み合わせにより、「5年程度で数学は大きく前進する可能性がある」と見ている

　AIと数学の組み合わせにより、今後は「小学生でもゲーム感覚で難解な数学を楽しめるようになるかもしれない」（加藤氏）。AIによって、数学に触れる人の裾野が広がる可能性もある