AIが数学の反例発見を加速、Lean形式化も自動化
原題: Human mathematicians are being outcounterexampled
なぜ重要か
AIが未解決数学問題の反例発見から形式証明の完全自動化までを達成したことで、数学研究とその検証プロセスに根本的な変革が生じる可能性を示している。
2026年5月20日、ChatGPTが離散幾何学の未解決問題「Erdős単位距離予想」の反例を発見した。その後、OpenAIのモデル「Sol」が3週間で120万行のLeanコードを生成し、公理系のみを前提とした完全な形式化証明を達成。AIによる数学的発見と形式証明の自動化が現実のものとなった。
2026年5月20日、ChatGPTが「Erdős単位距離予想」（離散幾何学の長年の未解決問題）の反例を発見したと発表された。この反例は、1960年代にGolodとShafarevichが証明した整数論の深い定理を用いて構成されるもので、複数の数学者が内容を事前に確認し、証明の正しさを認めた。
Xena Projectを主宰するImperial College LondonのKevin Buzzard教授は、反例がLean（数学的証明を機械検証するための定理証明支援系）で形式化されているかどうかをすぐに確認した。当初は形式化されていなかったが、発表から1週間も経たない5月26日、Fields賞受賞者でLogical Intelligenceの最高科学責任者Mike Freedmanから連絡が入った。同社はTuring賞受賞者・AIの「名付け親」Yann LeCunが共同創業した企業で、ChatGPTが生成した論文全体をLeanに自動形式化したと報告した。ただしこの段階では、整数論の核心的定理（証明に100ページ以上を要し、大域的類体論の大部分を必要とする）は前提として扱われていた。
さらに1か月後の6月26日、OpenAI所属のBoris AlexeevがLean Zulipにて、OpenAIの新モデル「Sol」を用いて公理系のみを前提とするErdős反例の完全形式化に成功したと発表した。Solは約3週間で120万行のLeanコードを生成した。Buzzard教授によると、そのコードの中には大域的類体論の困難な定理に対する証明も含まれており、2025年時点ではその形式化は「夢のような話」と考えられていたものだという。なお、Leanの数学ライブラリ「mathlib」は約230万行であり、9年間かけて人間が構築してきた成果物である。
Buzzard教授はAI生成コードのセキュリティリスクを考慮し、サンドボックス環境で実行して検証を行ったとも記している。