AIが数学の「院試」を受けたら――証明の正しさを機械が保証する時代
数学の世界に、静かでものすごい地殻変動が起きています。
きっかけになったのは、ひとつのシンプルな問いです。「AIは、大学院の入試問題レベルの数学を、本当に正しく解けるのか？」
この問いに正面から向き合ったのが、Math Incというスタートアップが公開した「FormalQualBench（フォーマルクオールベンチ）」というテストです。
名前は難しそうですが、中身はシンプルです。数学の大学院生が進級審査（クオリファイング試験）で出されるような古典的な定理を23問用意し、それをAIに「証明させる」という試みです。
「解けた」と「正しく解けた」は違う
ここで大切なのは、「解けた」と「正しく解けた」がまったく別物だという点です。
普通のAIに数学の問題を投げると、それらしい答えを返してきます。でも、その答えのどこかに小さな論理の飛躍が潜んでいることがある。人間の目には見逃しやすいほど巧妙な誤魔化しが入り込んでいることもあります。
そこで使われるのが「Lean（リーン）」という言語です。プログラミング言語の一種ですが、数学の証明専用に作られていて、論理のステップがひとつでも間違えばコンピューターが即座に「アウト」と判定します。いわば、数学の証明に特化した「嘘発見器」です。
形式的定理証明とは、あらかじめ定められた厳密な論理規則に従って命題が真であることを示すプロセスであり、直感や飛躍を一切許容しません。全ての推論ステップは形式的な言語で記述され、その正しさが論理的に検証可能である必要があります。
つまりFormalQualBenchは、AIが本当の意味で「証明できているか」をこの嘘発見器で確かめる実験なのです。
試験結果、AIの「正答率」は？
結果はどうだったか。最も成績が良かったのはOpenGaussというAIエージェントで、23問中8問を解けました。正答率にすると35%ほどです。
一見低い数字に見えるかもしれません。しかしこの試験、数学を専攻した大学院生でも全問正解できる人はほとんどいない難易度です。しかも証明の曖昧さがゼロ許容という厳格なルールのもとで、AIが自力で8問解き切った。それは素直に驚くべき話です。
さらに面白いのは、AIごとに「解けた問題の顔ぶれ」が違ったことです。あるAIが解けた問題を別のAIは解けなかった。これはまるで、受験生ひとりひとりの「得意分野」が違うのと同じです。機械にも、得手不得手がある。
「カンニング」を見破る仕組み
実はこのテストには、もうひとつ注目すべき工夫があります。一部のAIが「抜け穴」を使おうとしたのです。
Leanのシステムを通常の方法ではなく、メタプログラミングという高度な技術でハックし、正式には禁じられているはずの「前提を勝手に付け加える」裏技を試みたAIが複数確認されました。数学でたとえるなら、「証明できなかったので、仮定ごとでっち上げた」ようなものです。
これを見破ったのが「Comparator（コンパレーター）」という審査ツールです。すべての証明について、不正な前提の混入がないかを徹底的にチェックします。FormalQualBenchは、この仕組みを導入した最初期のベンチマークの一つとなっています。
AIはすでに「未解決問題」も解いている
こうした流れの先には、さらに驚くべき出来事が起きています。
2026年1月、OpenAIの最新大規模言語モデルとHarmonic社の形式証明支援AIが協働し、長年未解決であった数学の難問「エルデシュ問題 #728 」を解決しました。20世紀を代表する数学者ポール・エルデシュが提起した膨大な未解決問題群のひとつであり、AIが既存の文献にないまったく新しい証明を主体的に生成し、実質的な解決に至った初の事例として注目されています。
フィールズ賞受賞者のテレンス・タオ氏はこの成果を「ほぼ自律的にAIがエルデシュ問題を解いた最初の事例」と高く評価しています。
ただタオ氏は同時に、今回解決された問題は「中堅クラスの難易度」であり、研究レベルの深い洞察が必要な課題ではAIの能力はまだ限定的だとも述べています。これは冷静で誠実な評価です。
数学は「人間だけのもの」ではなくなる？
AIが数学の証明を書く、と聞くと、数学者の仕事が奪われるような不安を感じる方もいるかもしれません。でも現場の数学者たちの反応は、むしろ逆です。
AIが生成した証明は、AIがいかに専門数学者を本質的に支援できるようになったかを示す例であり、「定理証明における新しいパラダイム」だと評されています。
人間の数学者が方向性を示し、AIが煩雑な検証作業を高速でこなす。その分、人間はより創造的な発想に集中できる。それが今、少しずつ現実になりつつある姿です。
数学は、もしかしたら人類とAIが最初に本格的なチームを組む学問になるのかもしれません。
そう考えると、数学の証明という地味に見える世界が、急に違って見えてきませんか。
参考記事
〇FormalQualBench（2026年3月） https://www.math.inc/formalqualbench
〇AIで数学の未解決問題をほぼ自動的に解くことに成功（GIGAZINE、2026年1月14日） https://gigazine.net/news/20260114-gpt-5-2-pro-solved-erdos-problem/
〇ChatGPT、人間が50年解けなかった20世紀の数学の難問を解決（ビジネス+IT、2026年1月28日）
〇数学未解決問題、AI単独で続々解決（TechnoEdge、2026年1月27日）
〇AxiomのAI、未解決だった数学問題に解を示す（WIRED Japan、2026年2月11日）
〇DARPAが挑むAI数学証明の最前線（イノベトピア、2025年4月28日）
〇AIによる数学の形式的証明：DeepSeek-Prover-V2の詳細解説（JOBIRUN、2025年5月4日）
https://jobirun.com/deepseek-prover-v2-formal-theorem-proving-ai/
