ChatGPTがエルデシュ予想を形式検証、数学証明の自動化が新段階へ
ChatGPTがエルデシュの単位距離予想を反証し、OpenAIの新モデルSolがその証明をLeanで形式検証。数学者とAIの協業に革命が起きている。
2026年5月、ChatGPTが離散幾何学の未解決問題であるエルデシュの単位距離予想を反証した。この成果は数学界に衝撃を与えたが、さらに注目すべき展開が続いている。OpenAIの新モデル「Sol」がその証明全体を形式検証システムLeanで自動形式化し、数学の公理だけに基づく完全な検証を実現したのである。
Lobstersのxenaproject.wordpress.com via sanxiynの報道によれば、形式検証の専門家であるxenaproject氏（以下、同氏）がこの出来事を「人間の数学者が反例で打ち負かされている」と評し、AIによる数学証明の自動化が新たな段階に入ったことを示唆している。
エルデシュ予想の反証
エルデシュの単位距離予想は、平面上の点集合において同じ距離（単位距離）を持つ点のペアの数が最大でどれだけになるかを問う問題である。この予想は長年にわたり未解決だった。
ChatGPTが生成した反証の核心は、1960年代にゴロドとシャファレヴィッチが証明した数論の深遠な定理を利用する点にある。この定理の証明は100ページ以上に及び、20世紀初頭に発展した大域類体論の広範な知識を必要とする。これまで短い証明は存在せず、圧縮が極めて困難とされてきた。
同氏の報告によれば、複数の人間の数学者がこの反証を検証し、その正当性を認めたという。同氏は「知っている数学者も何人かおり、そのうちの何人かは信頼していた。彼らは議論を理解したと述べていた」と記している。
形式検証への取り組み
同氏は以前からLeanによる定理証明の重要性を主張してきた人物である。ChatGPTの反証が発表された直後、同氏は最初に「反例はLeanで形式化されているのか」と疑問を抱いた。その答えは「いいえ」だった。
しかし状況は急速に変化した。2026年5月26日、フィールズ賞受賞者のマイク・フリードマンから電子メールが届く。フリードマンは論理知能（Logical Intelligence）社の最高科学責任者を務めており、同社のシステムがChatGPTが生成した論文全体をLeanで自動形式化したと連絡してきた。
同氏と博士研究員のトーマス・ブラウニングが確認したところ、論理知能社は数論の深遠な定理がエルデシュの反証を導くという命題を正確に形式化していた。LLMが生成した数学がリアルタイムで形式化されるという画期的な成果である。
Solによる完全形式化
大きな課題が残っていた。ゴロド・シャファレヴィッチの定理の証明全体を形式化することである。この定理の理解には大域類体論が必要であり、2025年の段階では大域類体論の形式化は「幻影のように思えた」と同氏は述懐する。
2026年6月26日、状況は一変した。OpenAIの研究者ボリス・アレクセーエフがLeanのZulipチャット上で、ChatGPTを新しいモデルSolで誘導し、エルデシュ反証の完全な形式化を達成したと発表した。同氏の博士研究員エジソン・シエが取り組んでいた局所類体論の形式化が完了したことも大きな進展だった。
アレクセーエフはコードを公開し、同氏もすぐにそれを確認した。数学の公理のみに基づく完全な形式化証明が、AIによって生成されたのである。
数学研究の変革
この成果は数学の研究手法に根本的な変革を迫るものだ。AIが生成した証明を人間が検証する従来の枠組みでは、証明の長さや複雑さが人間の理解限界を超える可能性がある。形式検証システムLeanによる自動検証は、この問題に対する現実的な解決策を提供する。
同氏は「2040年までに、Leanが重要な数学の証明を人間よりも上手く扱えるようになるだろう」と以前から予測していたが、現実は予想よりも速く進んでいる。AIによる証明生成と形式検証の組み合わせは、数学の研究プロセスを根本から変える可能性を秘めている。
編集部の見解
今回の成果はAIによる数学研究の自動化が理論的可能性から実用段階へ移行したことを示している。短期的には、Leanのような形式検証システムの導入が数学の主要な研究分野で加速し、AIが生成した証明の検証手段として標準化される可能性が高い。特に数論や代数幾何学のように証明が長大化する分野では、人間の検証に代わる手法として注目されるだろう。
長期的視点では、AIによる数学証明の自動生成と形式検証の完全統合が、数学者の役割を「証明を発見する者」から「AIの出力を監督・解釈する者」へと変化させる可能性がある。これは数学教育の内容や博士課程の研究スタイルにも影響を及ぼすだろう。
編集部としては、AIが生成した証明の「理解可能性」が今後の課題になると見る。形式検証が正しさを保証しても、人間がその証明を理解し、そこから新たな洞察を得られるかは別問題である。数学は単なる証明の集合ではなく、人間の理解と洞察によって発展してきた分野だ。AIと人間の協業が数学の文化的側面にどのような影響を与えるかが、今後問われることになる。
参考
- 「Human mathematicians are being outcounterexampled」, by xenaproject.wordpress.com via sanxiyn — Lobsters, 2026-07-20T22:16:00.000Z (ARR)
- 元記事URL: https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/
よくある質問
- エルデシュの単位距離予想とはどのような問題か
- 平面上の点集合において、同じ距離（特に単位距離）を持つ点のペアの最大数を求める問題。長年にわたり未解決だった離散幾何学の難問で、ChatGPTが反証を生成したことで注目を集めた。
- Lean形式検証システムとは何か
- マイクロソフトが開発した対話型定理証明システム。数学の証明をコンピュータ上で検証可能な形式に変換し、厳密な正しさを保証する。近年、数学の形式化プロジェクトで広く使われている。
- SolモデルはどのようなAIモデルか
- OpenAIが開発した新しいAIモデル。数学の証明や形式検証の自動化に特化した能力を持つ。ChatGPTが生成した証明をLeanで自動形式化するタスクでその能力が実証された。
コメント