AIエージェント能力アトラス › 仕事ごとの一覧 › 研究・問題解決 › 数学
定理証明・形式化(Lean/Isabelle)
Formal theorem proving and formalization (Lean/Isabelle)
2030年（予測）: 5/5 専門家超え
0 できない ／ 1 デモ止まり ／ 2 補助 ／ 3 実務品質（要確認） ／ 4 専門家並み ／ 5 専門家超え。「予」は予測。
専門家と比べて
素数定理(PNT)の強形の形式化は人間専門家が18ヶ月以上停滞していたところ、AI支援(Math Inc.)によりわずか3週間で完了。ジュニア形式化専門家に近い生産性向上が確認されているが、査読なしでの完全自律形式化はまだ限定的。
できること
既知の(証明済みの)数学的主張をLean/Isabelleコードへ翻訳し、コンパイラでの機械検証まで通せる。LeanMarathonのような長期ホライズンの自動形式化パイプラインや、AristotleのようなツールがErdős問題の一部を自動でLean証明化した実例がある。
まだできないこと
自然言語の数学的主張が持つ「暗黙の前提」を形式言語に正しく落とし込む意味的検証(informal-to-formal correspondence)は依然として未解決の根本課題。形式化された補題が本来意図した主張と微妙にずれていても気づけないことがある。
なぜそうなのか
自然言語数学は曖昧さ・省略された前提を含むため、形式化の際に「証明可能だが無意味な形式化」に陥るリスク(問題設定の意図しない抜け穴の悪用)が構造的に残る。信頼できる評価指標が不足している。
これからの予測の根拠
意味的検証の課題は技術的に根深いが、自動形式化ツールの生産性向上は年単位で継続しており、2028年ごろには専門家並みの自律形式化(要確認なし)に近づくと予測。完全な信頼性確立(2030年)は意味的検証問題の解決次第。
いま使える主な道具
Aristotle (Lean prover)、GPT-5.5 Pro、AlphaProof、LeanMarathon、LeanAtlas
根拠
- LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization 2026
長期ホライズンのLean自動形式化研究 - Major Breakthroughs in Lean 4-Based Auto-Formalized Mathematics 2026
PNT形式化が18ヶ月超→3週間に短縮された事例を含む - The story of Erdős problem #1026 2025-12
AristotleがLeanで自動証明、人間は別途エレガントな証明を独立発見
同じ分野のほかの仕事（数学）
- 競技数学(IMO/Putnam級)
- 競技プログラミング(ICPC/IOI級アルゴリズム設計)
- 未解決問題への貢献(Erdős問題・主要予想)
- 大規模計算実験・構成的探索(AlphaEvolve/FunSearch型)
- 数学論文の査読相当チェック(証明検証・誤り検出)
AIエージェント能力アトラス 2026（2026-09-06 時点・v1.0）の1マスです。レベルは公開された実験・ベンチマーク・報告から付けた目安で、2027年以降は予測です。全マスに根拠のリンクがあります。作者は個人で、AI（Claude）と一緒に調べて作っています。