注目★★★★★Lobsters
数学の難問を AI が次々と反証——人間の数学者が「出し抜かれる」時代へ
30秒で把握
- 1ChatGPT が Erdős 予想、Sol が大域類体論、Fable が群スキーム予想を次々と反証・形式化
- 2AI 生成の Lean コード (120 万行) が人間の 9 年分の成果と同等規模を数週間で達成
- 3自動形式化ツール (Logos / Logical Intelligence / OpenAI) の競争激化で数学査読の人間不要化が加速
要約
Lean 形式化の第一人者である Kevin Buzzard が、2026 年の数ヶ月間で AI が数学の難問を相次いで反証した経験を記録した。ChatGPT が Erdős の単位距離予想を反証し、その後 OpenAI の Sol が 120 万行の Lean コードを生成して大域類体論を形式化、さらに Grothendieck の有限平坦群スキーム予想まで反証した。AI が生成した数学的主張は Lean で検証可能な形で提示され、人間の数学者による査読が段階的に廃止される兆候を示している。この過程で Logical Intelligence や Logos Research などの自動形式化ツールが競争的に発展し、数学知識の形式化速度が人間の能力を明らかに上回るようになった。
あなたへの影響
数学の論文執筆・査読・反証が AI に占有される可能性が現実化した。Lean や Coq などの証明支援系言語の習得優先度が急速に上昇している。
推奨：日本の数学科や理論系研究室では、今後の研究テーマ選定や論文投稿戦略で「先制的な AI 活用」と「形式化検証スキル」の習得が競争上の差を決めるようになり得る。