コンピュータ、数学の問題を解き始める

全体概要

本セミナーは2022年3月26日に開催されたマルレクの講義資料であり、「コンピュータが数学の問題を解き始める」という歴史的転換点を、二つの独立しつつも深く連関した視点から探求しています。

第一の視点は、OpenAIによるニューラル定理証明システム（Open-AI Theorem Prover）という、AIの最前線における挑戦的な取り組みです。このシステムは数学オリンピックレベルの問題を対象に、自然言語で与えられた数学の命題を形式言語Leanに翻訳し、形式的に証明することを試みます。Deep Learningが「広い見通しとシンボルに基いた推論」においてまだ限界を抱えているという率直な自己分析のもと、セルフ・プレイに代わるカリキュラム学習という新しいアプローチが提案されています。

第二の視点は、数学者自身がコンピュータを証明の道具として使い始めたという、数学コミュニティの内側からの変化です。連続体仮説の独立性証明、Feit–Thompson定理、ケプラー予想といった数学史に刻まれる難題が、Lean・Coq・HOL Lightなどの証明支援系を用いて形式的に検証されてきた過程が紹介されます。

そしてこの二つは単なる並列ではなく、深い結びつきを持っています。Open-AI Theorem Proverが学習した最重要データベース「mathlib」は、まさに後者の数学者たちによる形式的証明の蓄積から生まれたものだからです。論文タイトル「Formal Mathematics Statement Curriculum Learning」はそのことを端的に示しています。

さらに本セミナーは、Vladimir Voevodskyが提起した「数学的知の累積性への脅威」という哲学的問題意識を背景に、なぜ数学者が証明にコンピュータを使い始めなければならないのかという根本的な問いに向き合います。「計算＝証明＝プログラム」という三項同一性の認識を軸に、コンピュータ自身がすでに推論能力を持つという強い主張が展開され、数学・AI・哲学の交差点を照らし出す一作となっています。

講義のロードマップ

■ Part 1: Open-AI Theorem Prover

• この部の核心:

LeanのためのニューラルネットワークベースのTheoremProverが、AMC12・AIME・IMOといった数学オリンピックの問題を対象にどのような証明を生成するかを具体的に示します。自然言語の問題をLean形式に翻訳し、TacticsとよばれるLeanの証明ステップを生成することで、形式的に検証された証明を返すという仕組みが明らかにされます。また、Deep Learningが数学的証明において直面する「無限の動作空間」と「セルフ・プレイ設定の不在」という二つの根本的困難と、それへの対処としてのカリキュラム学習戦略が率直に論じられます [p.12]〜[p.60]。

• 論理展開:
• システムは自然言語→Lean形式への変換（Seq2Seq）を行い、Leanでの証明成功を返す構造を持つ [p.14]。
• 証明された問題（AMC12・AIME・IMO）のLeanコードを丁寧に読解し、`linarith`・`nlinarith`・`use`・`rw`などのTacticsが何をしているかを解説 [p.31]〜[p.46]。
• モデルの限界として「2〜3ステップ以上の非自明な推論連鎖が困難」であり、数学オリンピックの最優秀生徒とはまだ競争できない水準にある旨を論文著者自身が認める [p.58]〜[p.60]。
• セルフ・プレイに代わる解決策として、難易度が多様な補助問題群をカリキュラムとして提供する手法を提案し、miniF2Fベンチマークで最先端性能を達成したと報告 [p.55]〜[p.56]。

■ Part 2: Open-AI Theorem Proverは何を学習したのか？

• この部の核心:

Open-AI Theorem Proverに与えられた三種類の訓練データ——miniF2F-curriculum・synth-ineq・mathlib-train——の内容と意義を詳細に解説します。特に最大規模のmathlib-train（25,000件）は、Leanの数学ライブラリmathlibから抽出された証明付き定理集であり、代数・解析・位相・圏論など広大な数学領域をカバーしていることが示されます。これらのデータがAIの「学習対象」として機能するためには、事前に人間の数学者たちによる形式的証明の蓄積が必要だったという重要な事実が浮かび上がります [p.63]〜[p.99]。

• 論理展開:
• miniF2F-curriculumは「The Art of Problem Solving」から抽出された327問をLean形式に変換したもので、証明部分は`sorry`（省略）となっている [p.68]〜[p.73]。
• synth-ineqはAM-GM・Cauchy-Schwarzなどの不等式定理を組み合わせて自動生成された合成不等式問題5,600件 [p.74]〜[p.82]。
• mathlib-trainはmathlibライブラリからの証明付き定理25,000件で、algebra・topology・number_theoryなど27領域を網羅 [p.87]〜[p.99]。
• mathlibの各ファイル（例：`order/filter/basic.lean`の`comap_eq_of_inverse`）には複数の証明スタイルが並存しており、AIはそれを学習素材とする [p.95]〜[p.99]。

■ Part 3: 数学者、証明にコンピュータを使い始める

• この部の核心:

数学者が主体となってコンピュータを証明に活用した三つの歴史的事例——連続体仮説の独立性証明・Feit–Thompson定理・ケプラー予想——を詳細に紹介します。いずれも、証明の規模や複雑さが人間の検証能力の限界を超えており、コンピュータによる形式的証明の必要性を説得力をもって示す事例として機能しています [p.102]〜[p.141]。

• 論理展開:
• Jesse Michael Han・Floris van DoornによるLean実装の連続体仮説独立性証明（2020年）は、GitHubから`leanproject build`コマンドで実行可能であり、ZFCの公理群からCohenのForcing法まですべてLeanで記述されている [p.106]〜[p.125]。
• Georges GonthierはCoqでFeit–Thompson定理（奇数位数定理）の形式的証明を完成（2012年）。15,000の定義・4,300の定理・17万行・6年間の作業 [p.127]〜[p.132]。
• Thomas HalesのFlypspecプロジェクトはケプラー予想のHOL Light実装であり、`the_kepler_conjecture`の定義が`packing`・`ball`などで形式化されている [p.134]〜[p.141]。

■ Part 4: 形式的証明の背景と変化の意味を考える

• この部の核心:

なぜ数学者がコンピュータを証明に使い始めるのかという問いに対し、三つの理由——人の手にあまる巨大問題の存在・証明の正しさの検証必要性・数学者自身の誤り——を整理します。その中で最も根本的な動機として、Vladimir Voevodskyが「数学的知の累積性への脅威」として提起した問題意識を詳細に紹介し、Univalent Foundationという新しい数学の基礎づけへと議論を展開します [p.144]〜[p.168]。

• 論理展開:
• Voevodskyは自らの1993年の論文の重要補題が誤っていたことを後に発見し、また別の論文の正しさを確信できたのが2013年になってからだったという個人的体験を告白 [p.161]。
• 数学の二つの危機として「純粋数学と応用数学の分離」と「検出されないエラーの蓄積」を提起し、後者への唯一の解はコンピュータによる証明検証であると論じる [p.172]〜[p.175]。
• Homotopy Type TheoryとPer Martin-LöfのType Theoryを基盤にUnivalent Foundationを構築し、その実装UniMathをGitHubでプログラム形式で公開——論文ではなくコードで数学を記述するスタイルが21世紀の数学を特徴づけると主張 [p.166]〜[p.168]。
• 「計算＝証明＝プログラム」という三項同一性の認識により、コンピュータはAIによって「推論能力を与えられる」のではなく、もとより推論能力を持つと著者は主張する [p.9]。