AIが数学の未解決問題を次々と反証
Judul asli: Human mathematicians are being outcounterexampled
Mengapa Ini Penting
AIが未解決数学問題の反証と形式検証を短期間で実現し、数学研究の手法が根本から変わりつつある。
2026年5月20日、ChatGPTが離散幾何学のErdős単位距離予想を反証。OpenAIのモデルSolが3週間で120万行のLeanコードを生成し、完全形式化を達成した。
2026年5月20日、ChatGPTがErdősの単位距離予想を反証した。証明の核心は、1960年代のGolodとShafarevichによる数論の定理を用いて反例を構築するというものだ。Fields賞受賞者のMike Freedman率いるLogical Intelligenceは、発表から1週間以内にChatGPT生成の論文をLeanで形式化し、数論定理からErdős反例が導かれることを検証した。
さらに6月26日、OpenAI研究者のBoris Alexeevが、OpenAIの新モデル「Sol」を活用し、数学の公理のみを前提とした完全な形式化を達成したと発表。Solは3週間で約120万行のLeanコードを生成した。これはLeanの数学ライブラリ「mathlib」（230万行・9年かけて開発）の約半分に相当する規模だ。
Xenaプロジェクト代表でLean開発者のKevin Buzzard氏は「大規模なAI生成数学の発展は避けられない」と述べた。ただし、AI生成コードの信頼性に懸念を示し、サンドボックス環境での検証を推奨している。