AIが数学の反例生成で人間を凌駕
원제: Human mathematicians are being outcounterexampled
왜 중요한가
AIが100年来未解決の難問を形式証明まで完遂したことで、数学研究におけるAIの役割が根本的に変わりつつある。
2026年5月20日、ChatGPTが離散幾何学のErdős単位距離予想を反証した。翌月6月26日にはOpenAIのモデル「Sol」がLean上で公理のみを前提とした完全な形式証明を生成。わずか3週間で120万行のLeanコードを自動生成し、数学界に衝撃を与えた。
2026年5月20日、ChatGPTがErdősの単位距離予想の反例を構築した。証明の核心は、1960年代にGolodとShafarevichが確立した数論の深い定理（証明に100ページ以上を要する大域的類体論を含む）を用いて反例を構成するというものだった。
その後5月26日、Fields賞受賞者でLogical IntelligenceのCSOであるMike Freedmanが、同社システムがChatGPT生成論文をLeanで自動形式化したと報告。同社はTuring賞受賞者・Yann LeCunが共同創業した企業だ。
6月26日には、OpenAI所属のBoris Alexeevが新モデル「Sol」を使い、数学の公理のみを前提とした完全な形式証明をLean上で構築したと発表。Solは3週間で120万行のLeanコードを生成した。比較として、コミュニティが9年かけて構築した数学ライブラリ「mathlib」は230万行である。
Xena ProjectのKevin Buzzard教授（Lean maintainer）は、AI生成コードを安全のためサンドボックス上で実行し、大域的類体論の難解な定理の証明が含まれていることを確認した。同教授は「AIによる大規模な数学の自動開発は不可避」と述べている。