概要
- 近年、AIによる 反例発見 が数学界で注目を集めている。
- ChatGPTなどの LLM が未解決問題の反例を自動生成し、Lean等で形式化が進む現状。
- AIツールが 大規模な数学コード を生成し、従来の人間中心のアプローチを変革。
- ワークショップや研究現場でもAI活用が進み、 反例発見の低コスト化 が顕著。
- 人間の専門家の態度や、 今後の数理研究の方向性 についても考察。
反例発見とAIによる数学形式化の最前線
- 2026年5月20日、ChatGPTが ErdősのUnit Distance予想 の反例を発見した事例が発端。
- 人間数学者による証明確認、Golod・Shafarevichの定理の応用。
- 反例のLeanによる 自動形式化 がLogical Intelligence社によって実現。
- Fields賞受賞者Mike Freedman、Turing賞受賞者Yan LeCunらが関与。
- 形式化は 定理そのもの ではなく、定理から反例を導く部分に限定。
- グローバル類体論 の形式化は依然として困難だが、AIの進展で可能性が拡大。
- 2025年のClay Summer Schoolでの進捗、Edison Xieの研究。
- 2026年6月26日、OpenAIの Sol モデルによりグローバル類体論まで含めた完全な反例の形式化に成功。
- Boris Alexeevによる公開コード、120万行のLeanコード生成。
- mathlib（230万行、9年分）に匹敵する規模のAI生成コード。
- AI生成コードの 信頼性問題 により、サンドボックス環境での検証が必須。
フェルマーの最終定理ワークショップと有限平坦群スキーム
- Formalizing Fermatワークショップ（2026年7月6-10日）で AIツールの活用 を推進。
- Logos Research, Logical Intelligence, Harmonic, Axiom AI, Moonshot AI等のツール。
- Claude Max、Claude Fable、ChatGPT Pro、Solなどのサブスクリプション提供。
- 有限平坦群スキームの理論構築の過程で、AIが 誤った主張の反例 を自動発見。
- LLM生成のPDFの誤りをAIが指摘し、反例を提示。
- 人間が見逃した誤りをAIが発見する実例。
- Grothendieckの「任意の次数nの有限自由群スキームはnで消えるか」という古典的問題へのAIアプローチ。
- Claude FableとSolで反例生成、Leanで形式化、mathlibにPR。
- 反例自体はErdősのものよりも遥かに短いコードで実現。
数学者の反応とAI時代の研究環境
- Grothendieck反例発見後の 専門家の反応。
- 「簡単に見つかる反例はそもそも重要でない」という意見も。
- 筆者自身はかつて一週間真剣にこの問題に取り組んだ経験あり。
- 人間側の「否認」など、心理的な変化も観察。
- PhD学生によるAIツール活用の経済性。
- SolやFableへの投資（月額$200）を推奨。
- HarvardではPhD全員にFable無償提供の実例。
Jacobian予想とAIによる未解決問題の反例発見
- Akhil MathewとLevent Alpögeによる Jacobian予想の反例発見。
- 100年未解決だった代数幾何の大問題、2026年ワールドカップ決勝中にAIが解決。
- Paul Lezeauが手動で形式化し、DeepMindのFormal ConjecturesリポジトリにPR。
- 数学的主張の Lean形式化 の意義。
- 人間がLean文で主張の意味を合意できれば、AI生成の証明の妥当性確認は容易。
AIと数学の未来——反例発見の新時代
- 大規模言語モデル （LLM）による数学的反例の自動発見が現実化。
- 人間の読解・検証能力を超えるスケールでのコード生成。
- 形式化ツール（Lean等）の発展により、 AIと人間の協働 が加速。
- 形式化済みの主張・証明は、再現性・検証性が高い。
- 未解決問題へのアプローチ が「反例発見」という形で急速に低コスト化。
- これまで人間が長年挑戦してきた問題もAIが短期間で解決。
- 研究者の役割の変化。
- 問題設定、AI活用戦略、形式化の監督、倫理的・社会的インパクト評価などが重要に。
- 今後は AIが生成した新たな数学的知識 の信頼性・意義・発展への人間の関与が鍵。