AIが数学の反例生成でも人間を超越
मूल शीर्षक: Human mathematicians are being outcounterexampled
यह क्यों महत्वपूर्ण है
AIが未解決数学問題の反例発見から形式証明生成まで短期間で完結させ、数学研究における人間とAIの役割分担を根本的に問い直す事例となった。
2026年5月20日、ChatGPTが離散幾何学のErdős Unit Distance予想を反証。その後OpenAIのモデル「Sol」が6月26日までに数学の公理のみを前提とした完全なLean形式証明を生成。約120万行のコードを3週間で出力した。
Xena Projectを主宰する数学者が、2026年に起きた形式化・AI数学の急展開をまとめた。
2026年5月20日、ChatGPTがErdős Unit Distance予想（離散幾何学の長年の未解決問題）の反例を構築。証明の核心は、1960年代にGolodとShafarevichが示した数論の深い定理を用いるものだった。
同月26日、Turing賞受賞者Yann LeCun共同創業の企業「Logical Intelligence」のCSO（最高科学責任者）でFields賞受賞者のMike Freedmanが、同社システムがChatGPT生成の論文全体をLeanで自動形式化したと報告。ただしこの時点では、証明の核となる数論定理（100ページ超、大域的類体論を必要とする）は形式化の範囲外だった。
続く6月26日、OpenAI所属のBoris Alexeevが、同社の新モデル「Sol」を用いて数学の公理のみを前提とした完全なLean形式証明を達成したとLean Zulipで発表。Solは3週間で約120万行のLeanコードを生成。数学ライブラリ「mathlib」の総行数が約230万行であり、その構築に9年を要した事実と対比され、AI主導による大規模数学開発の実現可能性が現実として認識された。
著者はAI生成コードへのセキュリティ上の懸念からサンドボックス環境で検証を実施。コードの一部は品質に課題があるものの、大域的類体論の難解な定理の証明が含まれていることを確認した。