定理証明支援系 Lean と生成AIを組み合わせて数学の定理を自動証明する試みが世界で活発に行われている．2026年の年明けには，Erdős問題をはじめとする未解決問題まで解決できるようになってきた．数学の形式化や機械化には100年以上の歴史があり，伝統的な計算複雑性理論によれば，定理証明は難しい問題であることが示されている．それにも関わらず，なぜ今日のAIは証明できるようになったのだろうか．明らかに，伝統理論と現実の間にはギャップがある．講演者らは，統計的学習理論の観点から現代的なAIによる定理証明技術の証明成功確率を評価する理論を開発した．本講演では，AI定理証明によって証明ができる仕組みを，証明完了状態に到達する確率「統計的証明可能性」に着目して解析する．形式的証明探索をMDPとしてモデル化し，学習済み証明器と最適証明器の差を理論的に評価することで，数学AIが機能する条件を調べる．