AI が正しい文章やコードを生成できることと、その成果物が正しいと確定できることは別の問題である。生成結果がもっともらしく見えること、過去より正答率が高いこと、別の AI が正しいと評価したことは、いずれも成果物そのものの正しさを直接保証する条件ではない。生成する主体の能力をどれだけ高めても、その主体が誤る可能性を残す限り、生成結果をどの条件で「確定済み」と判断するかという問題は別に残る。
既稿では、ソフトウェアのテストは仕様そのものではなく、仕様から選び出した有限個の観測条件であり、テストがすべて通っても要求全体の充足までは保証しないことを論じた[1]。たとえば、ある関数について 100 個の入力と期待結果をテストしたとしても、そのテストから直接確認できるのは 100 個の条件について期待した結果が得られたことである。入力可能なすべての状態について同じ性質が成立することや、テストコード自体が要求を正確に表していることまで、自動的に導かれるわけではない。
また、長時間の仕事を AI に任せるには、モデルの推論能力だけでなく、現在何が完了し、何が未確定で、どの結果を後続処理が利用してよいかをモデルの外側で管理する必要があることを既稿で扱った[2]。作業が大規模になるほど、途中結果をすべて会話履歴やモデル内部の状態だけで保持することは難しくなる。そこで、未確定な状態を検証可能な単位へ分け、完了条件を満たしたものだけを後続が利用できる確定状態へ移すという考え方が必要になる[3]。
この問題を数学へ持ち込むと、検証条件をソフトウェアテストより強く定義できる場合がある。数学の命題を形式言語で記述し、その命題を導く証明も形式化すれば、「いくつかの例で正しい結果が出たか」ではなく、「指定された公理、定義、既証明定理から、その命題が論理的に導出できるか」を機械的に検査できる。生成を担当した AI 自身に正誤を判断させる必要はなく、AI とは別の検証器が証明を受理するかどうかを最終条件にできる。
2026 年 9 月、Anthropic はこの構造をフェルマーの最終定理へ適用した成果を発表した。Claude を用いた複数の AI エージェントが、既知の証明経路を Lean 4 上の定理と証明へ形式化し、11 日間で完全な機械検証可能な証明を構築したと報告している。最終工程では約 60 億の出力トークンを消費し、約 1,300 万行の Lean を生成し、30,300 個の定理を途中で証明し、そのうち約 29,500 個が最終成果物で使われた[4]。
1,300 万行という規模は、人間が生成結果を一行ずつ読み、内容を理解したうえで正誤を判断する方式が現実的でないことも示している。生成速度が上がれば、確認対象となる成果物も同じように増える。人間によるレビュー能力が一定のままで生成量だけが増えれば、最終的には検証が生産速度を制限する。その制約を避けるには、生成された大量の成果物を、人間が逐語的に読まなくても判定できる形式へ変える必要がある。
ただし、この成果の意味を「Claude が 11 日で Wiles の数学を再発見した」と捉えると、実際に行われた仕事とは異なる。フェルマーの最終定理に至る数学上の証明経路は既知であり、Mathlib、Imperial College London の FLT 形式化プロジェクト、flt-regular など既存の形式化資産も利用されている。AI がゼロから新しい証明原理を発見したのではなく、既知の巨大な数学を多数の形式命題へ分解し、証明済みの命題を次の命題の前提として積み上げた。
この違いは、成果の価値を小さくするものではない。むしろ、何が新しかったのかを明確にする。数万個の定理からなる依存関係を AI エージェントが処理し、それぞれについて Lean が受理できる証明を作り、最終的にフェルマーの最終定理まで途切れず接続した。さらに、生成を担当した Claude とは別に、Lean のカーネルや独立した検証系が最終成果物を検査した。生成能力そのものよりも、生成された候補を検証済みの状態へ変換し、その状態だけを次の推論へ渡す工程が成立したことに意味がある。
1. AI が作った結果を、AI 自身を信用せずに確定できるか
生成と検証を分ける構造を、まず単純な数理モデルとして表す。生成器を \(G\)、検証器を \(V\) とする。生成器は入力 \(x\) を受け取り、候補成果物 \(y\) を出力する。
\[
G : X \rightarrow Y
\]
\(X\) は入力として与えられる問題の集合、\(Y\) は生成可能な候補成果物の集合である。AI にプログラムを書かせる場合なら、\(x\) は仕様や既存コード、\(y\) は生成されたソースコードになる。形式証明なら、\(x\) は証明すべき定理と利用可能な定義・定理群、\(y\) は AI が生成した証明候補になる。
この時点では、\(y\) が正しいことは条件に含まれていない。生成器 \(G\) は正しい候補を返す場合もあれば、構文エラー、型エラー、論理的に成立しない証明、要求とは異なる成果物を返す場合もある。生成器の性能を高めれば誤った候補の割合を減らすことはできるが、誤りが完全に消えない限り、\(G(x)=y\) という事実だけから \(y\) の正しさを導くことはできない。
そこで、生成された \(y\) を別の検証器 \(V\) に渡す。検証器は候補成果物を受け取り、あらかじめ定めた検証条件に従って受理または拒否する。
\[
V : Y \rightarrow \{\mathrm{accept},\mathrm{reject}\}
\]
ここで確定条件を
\[
V(y)=\mathrm{accept}
\]
と定める。生成器が候補を返した時点では未確定であり、検証器が受理した結果だけを後続処理が利用できる状態へ移す。生成器が同じ問題について 10 回失敗して 11 回目に正しい候補を返したとしても、最初の 10 個が検証器によって拒否され、11 個目だけが受理されるなら、後続処理から見えるのは受理された成果物だけでよい。
| 段階 | 状態 | その時点で確定していること |
|---|---|---|
| 入力 | \(x\) | 解くべき問題や証明すべき命題が与えられている。 |
| 生成 | \(y=G(x)\) | 候補成果物が作られたことだけが確定しており、その正しさはまだ確定していない。 |
| 検証 | \(V(y)\) | 定義された検証条件を候補成果物が満たすかを判定する。 |
| 確定 | \(V(y)=\mathrm{accept}\) | 検証器が保証する範囲について、後続処理が利用できる成果物として扱える。 |
この構造では、生成器の信頼性と成果物の検証可能性を別々に扱える。生成器の性能が低ければ、受理される候補へ到達するまでの試行回数や計算量が増える。しかし、拒否された候補を確定済み成果へ混入させない限り、生成器の失敗率と最終成果物の正しさを同じ尺度で扱う必要はない。生成器には探索速度や候補生成能力を求め、検証器には受理条件の厳密さを求めるという役割分担が可能になる。
ソフトウェアテストにも、生成結果を別の処理で判定するという同じ外形がある。AI が関数を生成し、テストスイートがすべて成功した場合、生成器と検証器は一応分離されている。しかし、この場合に \(V(y)=\mathrm{accept}\) が意味するのは、「実行したすべてのテストについて期待結果と一致した」ということである。テストされなかった入力、状態遷移、異常系について同じ性質が成立することまでは含まれない。
たとえば、整数 \(x\) に対して常に正しい値を返すことが要求された関数を考える。テストが \(x=0,1,2\) の 3 ケースしか持たなければ、テスト通過から直接確認できるのは
\[
P(0)\land P(1)\land P(2)
\]
である。要求が
\[
\forall x\in\mathbb Z,\;P(x)
\]
である場合、前者から後者は一般には導けない。テストケースを 3 個から 3,000 個へ増やせば未確認領域を減らせるが、有限個の実行例を確認することと、全ての整数について命題を証明することは論理的に異なる。
形式証明では、この差を別の方法で扱う。検証したい性質そのものを量化を含む形式命題として記述し、その命題を導く証明項を検証する。整数 \(x\) の全てについて \(P(x)\) が成立することを証明したいなら、有限個の \(x\) を実行して確認するのではなく、
\[
\forall x\in\mathbb Z,\;P(x)
\]
そのものを証明対象とする。定理証明支援系の検証器は、提示された証明がその形式命題を導いているかを型検査する。この意味で、形式証明では「選択した観測点が正しかったか」ではなく、「形式化された一般命題が導出されたか」を直接検証できる。
Lean では、形式化された命題 \(P\) は型として表され、その証明は型 \(P\) を持つ項として表される。利用できる公理、定義、既証明定理をまとめて \(\Gamma\) とすると、検証したい関係は
\[
\Gamma \vdash P
\]
と書ける。これは「\(\Gamma\) に含まれる前提から \(P\) を導出できる」という意味である。AI がどのような思考過程で証明候補を作ったかは、この判定条件には含まれない。証明候補が長い推論の結果でも、偶然生成されたものでも、カーネルが確認するのは最終的な証明項が規則に従って型 \(P\) を持つかである。
ここで検証器が強くなったからといって、「正しい」という語の範囲が無制限に広がるわけではない。Lean が \(\Gamma\vdash P\) を確認したときに確定するのは、指定された形式体系の中で \(P\) が導出できることである。人間が「フェルマーの最終定理を証明したい」と考え、それを Lean の命題 \(P\) へ変換したとき、Lean は人間の頭の中にあった意図そのものを読むことはできない。
したがって、検証経路は実際には二つの異なる境界を持つ。
| 境界 | 確認したいこと | 機械検証で扱える範囲 |
|---|---|---|
| 仕様化 | 人間が意図した数学的主張と形式命題 \(P\) が一致しているか | 命題同士の形式的一致は比較できるが、人間の意図そのものは形式体系の外側にある。 |
| 証明 | 前提集合 \(\Gamma\) から \(P\) が導出できるか | 形式化された証明項をカーネルが規則に従って完全に検査できる。 |
この二つを区別すると、形式証明の役割を過大にも過小にも評価せずに済む。形式証明は、人間が意図したことを自動的に推測して保証する技術ではない。一方で、何を証明するかが形式命題として固定された後については、有限個のテストケースを確認する場合とは異なり、その命題を導く論理経路そのものを機械的に検査できる。
フェルマーの最終定理の形式化で確認すべきなのも、この二段階である。第一に、「フェルマーの最終定理」という人間向けの主張が Lean 上でどの命題として書かれているのかを確認する。第二に、その命題へ至る Frey 曲線、ガロア表現、モジュラー性、レベル降下といった巨大な証明経路が、どのような形式定理の依存関係として実装され、どの条件で検証済み状態へ変えられているのかを確認する。この二つを追うことで、Claude の能力を評価する話から、AI が生成した知的成果をどう確定できるかという構造へ議論を進められる。
2. フェルマーの最終定理を検証可能な数学的対象へ変換する
2.1 自然言語の定理名ではなく、量化された命題を固定する
フェルマーの最終定理は、正の整数 \(a,b,c\) と整数 \(n \ge 3\) に対して、
\[
a^n+b^n \neq c^n
\]
が成り立つという主張である。この一文には、形式化するときに固定しなければならない条件が複数含まれている。\(a,b,c,n\) がどの数の集合に属するのか、\(a,b,c\) が正であることをどう表すのか、指数 \(n\) の下限をどこに置くのか、そして結論が「解がない」ではなく「任意の \(a,b,c\) について等式が成立しない」という量化された命題であることまで明示する必要がある。
Mathlib では、この構造を一つの定義へ押し込まず、係数を取る型と指数を指定する FermatLastTheoremWith、自然数について特定の指数を扱う FermatLastTheoremFor、さらに \(n \ge 3\) の全指数を量化する FermatLastTheorem という段階に分けている[5]。この分割により、「指数 \(p\) の場合を証明する」「複数の指数に対する結果から一般の場合を導く」といった証明上の操作を、別々の定理として組み立てられる。
Anthropic の公開成果物で最終的に証明された定理は、自然数 \(n,a,b,c\) について、
\[
n\ge3,\quad
a>0,\quad
b>0,\quad
c>0
\]
を仮定したとき、
\[
a^n+b^n\neq c^n
\]
が成り立つという命題である。Lean では、この量化と仮定を定理の引数として明示し、最終的にこの不等式を証明する。
この宣言を通常の数学記法へ戻すと、\(n,a,b,c\) は自然数であり、仮定 \(3\le n\)、\(0<a\)、\(0<b\)、\(0<c\) の下で、\(a^n+b^n=c^n\) は成立しない、という命題になる。Lean では各条件が定理の引数として明示されているため、証明が暗黙に別の条件へ依存することはできない。
この点が自然言語による証明との大きな違いになる。人間同士の数学では、「非自明な整数解を考える」「正の場合だけ見ればよい」といった前提を文脈から補うことがある。Lean カーネルは文脈を推測しない。証明項が受理されるためには、結論で必要な型と、その導出に利用する全ての前提が形式的に接続されていなければならない。
最終的に検証される対象は「フェルマーの最終定理」という名前ではない。上記の定理宣言が表す型そのものであり、Lean が確認するのは、その型を持つ証明項が構成されているかどうかである。この段階で初めて、人間向けの数学的主張が機械的な検証対象になる。
2.2 全ての指数を直接証明せず、素数指数へ還元する
フェルマーの最終定理は全ての \(n\ge3\) を量化しているが、それぞれの指数について独立した証明を用意する必要はない。指数の因数分解を使うと、反例が存在する指数を、より基本的な指数へ還元できるからである。
たとえば、ある指数 \(n\) が奇素数 \(p\) を約数に持ち、
\[
n=pm
\]
と書けるとする。このとき仮に
\[
a^n+b^n=c^n
\]
という反例が存在すれば、
\[
A=a^m,\qquad B=b^m,\qquad C=c^m
\]
と置くことで、
\[
A^p+B^p=C^p
\]
という指数 \(p\) の反例が得られる。つまり、指数 \(n\) に反例があるなら、その奇素因数 \(p\) にも反例が存在する。逆に全ての奇素数指数について反例がないことを証明できれば、奇素因数を持つ合成数指数も同時に排除できる。
残るのは奇素因数を持たない指数、すなわち 2 の冪である。\(n\ge3\) なので、この場合は \(4\mid n\) となる。\(n=4m\) と書けば、同じ操作によって指数 4 の反例へ還元できる。
したがって、全ての \(n\ge3\) を扱うために必要なのは、大きく分ければ指数 4 と奇素数指数である。Mathlib の FermatLastTheorem.of_odd_primes は、この還元を形式化した部品になっている。Anthropic の証明経路では、指数 3 と指数 4 を既存の形式化で処理し、その後の巨大な証明を素数 \(p\ge5\) の場合へ集中させている[6]。
この還元には、単に計算量を減らす以上の意味がある。後に使う Frey 曲線、mod-\(p\) ガロア表現、Ribet のレベル降下などは、素数 \(p\) を固定した形で記述される。指数を素数へ還元することで、元の整数方程式を、有限体 \(\mathbf F_p\) 上の線形代数や mod-\(p\) 表現へ接続できるようになる。
証明全体を依存関係として見ると、この時点ですでに構造が現れている。
\[
\text{FLT for all } n\ge3
\longleftarrow
\begin{cases}
\text{exponent }4\\
\text{odd prime exponents}
\end{cases}
\]
巨大な一つの命題をそのまま解こうとしているのではない。上位命題を、より狭い条件を持つ下位命題へ分解し、それぞれを独立に確定できる形へ変えている。この数学上の分解は、後に Lean の定理の依存関係と Prove2Me の DAG にそのまま現れる。
2.3 反例を仮定し、Frey 曲線へ写す
ここから証明は反証法へ入る。素数 \(p\ge5\) に対してフェルマーの最終定理が偽であると仮定し、
\[
a^p+b^p=c^p
\]
を満たす 0 ではない整数 \(a,b,c\) が存在するとする。この仮定から、最終的に存在できない数学的対象を構成し、矛盾を導く。
最初に反例を扱いやすい形へ正規化する。共通因子があれば取り除くことができるので、
\[
\gcd(a,b)=1
\]
とできる。さらに \(a\) と \(b\) の交換や符号の調整を行い、
\[
a\equiv3\pmod4,\qquad 2\mid b
\]
という条件を持つ代表を選ぶ。Anthropic の形式化では、これらの条件と素数 \(p\)、反例の等式をまとめた構造を FreyPackage として扱う。Darmon、Diamond、Taylor の解説も、Frey、Serre、Ribet、Wiles、Taylor–Wiles による証明を、この反例から特殊な楕円曲線を構成する流れで整理している[7]。
反例から構成されるのが Frey 曲線である。よく知られた形では、
\[
y^2=x(x-a^p)(x+b^p)
\]
と書ける。右辺には元の反例に現れた \(a^p\) と \(b^p\) がそのまま埋め込まれている。つまり、整数方程式の解を、楕円曲線の係数へ移している。
Anthropic の形式化では、この曲線に対応する整係数モデルとして、
\[
E_P:\quad
y^2+xy
=
x^3+
\frac{b^p-1-a^p}{4}x^2
–
\frac{a^pb^p}{16}x
\]
を用いる[6]。ここで整係数モデルとは、楕円曲線を整数係数の Weierstrass 方程式として扱える形にしたものである。式だけを見ると \(4\) や \(16\) による除算が現れるが、先ほどの正規化条件がこれを整数にする。
まず \(a\equiv3\pmod4\) なので、奇数 \(p\) に対して
\[
a^p\equiv3\pmod4
\]
である。また \(b\) は偶数なので、
\[
b^p\equiv0\pmod4
\]
となる。このため、
\[
b^p-1-a^p\equiv0-1-3\equiv0\pmod4
\]
となり、\(x^2\) の係数は整数になる。
さらに \(p\ge5\) で \(2\mid b\) だから、\(b^p\) は少なくとも \(2^5=32\) で割り切れる。したがって \(a^pb^p\) は 16 で割り切れ、
\[
\frac{a^pb^p}{16}
\]
も整数になる。正規化条件は形式上の飾りではなく、この Frey 曲線を整数係数のモデルとして扱うための条件でもある。
整数係数の楕円曲線へ移すと、元の方程式には直接現れなかった算術的な情報を利用できる。楕円曲線には判別式 \(\Delta\) があり、各素数で曲線を還元したときに良い還元を持つか、乗法的還元を持つかといった局所的性質を調べられる。さらに \(p\)-捩れ、ガロア作用、導手といった構造も定義できる。
元の反例は消えたわけではない。\(a,b,c,p\) が持っていた情報が、Frey 曲線の判別式や各素数での振る舞いへ移されている。Ribet が整理した Frey 曲線と谷山–志村予想の関係では、この特殊な局所構造を持つ楕円曲線が、後のレベル降下と組み合わさることで存在不可能になる[8]。
ここまでの変換を並べると、整数論の反例が突然別分野へ飛んだわけではないことが分かる。
\[
(a,b,c,p)
\longrightarrow
E_P
\longrightarrow
\text{local arithmetic invariants}
\]
最初の四つ組が持つ合同式や因数分解の情報を、楕円曲線というより構造の豊富な対象へ埋め込んでいる。整数方程式そのものから矛盾を導くのが難しいため、反例が存在したときに必ず作られる楕円曲線を調べ、その楕円曲線に同時には成立し得ない性質を導く方向へ証明を移す。
3. Frey 曲線から、存在しないモジュラー形式へ進む
3.1 \(p\)-捩れ を 2 次元線形空間として見る
前章では、フェルマーの最終定理に反例があると仮定し、その反例 \((a,b,c,p)\) から Frey 曲線 \(E\) を構成した。次の段階では、この楕円曲線そのものを直接調べるのではなく、曲線上の特別な点を取り出し、数論の問題を有限体上の線形代数へ移す。
楕円曲線 \(E\) の点には加法が定義されている。ある点 \(P\) を \(p\) 回加えると単位元 \(O\) になる、
\[
[p]P=O
\]
という条件を満たす点を \(p\)-捩れ点 と呼ぶ。その全体を
\[
E[p]=\{P\in E(\overline{\mathbf Q})\mid [p]P=O\}
\]
と書く。ここで \(\overline{\mathbf Q}\) は有理数を含む代数閉包である。Frey 曲線は標数 0 の体上にあり、\(p\) は素数なので、\(E[p]\) は抽象的には
\[
E[p]\cong \mathbf Z/p\mathbf Z\times\mathbf Z/p\mathbf Z
\]
となる。有限体 \(\mathbf F_p=\mathbf Z/p\mathbf Z\) を使えば、
\[
E[p]\cong(\mathbf F_p)^2
\]
という 2 次元ベクトル空間として扱える。楕円曲線上の無限に広がる点集合のうち、\(p\)-捩れ だけを切り出すことで、問題が \(p^2\) 個の要素からなる有限な線形空間へ移る。
ただし、\(E[p]\) の各点の座標が有理数になるとは限らない。一般には代数的数を使わなければ座標を書けない。そこで、有理数を固定したまま代数的数を入れ替える全ての自己同型からなる絶対ガロア群
\[
G_{\mathbf Q}
=
\operatorname{Gal}(\overline{\mathbf Q}/\mathbf Q)
\]
を考える。ある \(\sigma\in G_{\mathbf Q}\) を \(p\)-捩れ点 \(P\) の座標へ作用させると、別の \(p\)-捩れ点 \(\sigma(P)\) が得られる。
この作用は楕円曲線の加法を保つ。つまり、
\[
\sigma(P+Q)=\sigma(P)+\sigma(Q)
\]
であり、さらに \(\mathbf F_p\) によるスカラー倍とも両立する。そのため、各 \(\sigma\) は \(E[p]\) 上の可逆な線形変換として表せる。基底を一つ選べば、その線形変換は \(2\times2\) 行列になる。
こうして得られる写像が mod-\(p\) ガロア表現である。
\[
\bar\rho_{E,p}:
G_{\mathbf Q}
\longrightarrow
\operatorname{GL}_2(\mathbf F_p)
\]
左辺には代数的数全体の対称性を記述する巨大なガロア群があり、右辺には有限体上の \(2\times2\) 可逆行列がある。この写像によって、楕円曲線の算術情報を有限体上の線形表現として観察できるようになる。Serre は、このような 2 次元 mod-\(p\) ガロア表現に対して、どのレベル、重さ、指標のモジュラー形式が対応するはずかを精密に定式化した[9]。
Frey 曲線について必要になる条件の一つが、この表現の既約性である。2 次元ベクトル空間 \(E[p]\) の中に 1 次元部分空間 \(V\) があり、全ての \(\sigma\in G_{\mathbf Q}\) について
\[
\bar\rho_{E,p}(\sigma)(V)\subseteq V
\]
となるなら、ガロア作用は \(V\) を壊さず、その内部だけで閉じている。この場合、2 次元の表現をより小さな表現へ分解できるので可約と呼ぶ。
逆に、
\[
\{0\}\subsetneq V\subsetneq E[p]
\]
を満たすガロア不変部分空間 \(V\) が一つも存在しなければ、表現は既約である。2 次元の場合、非自明な真部分空間は 1 次元しかないので、「ガロア作用によって保たれる直線が存在しない」と理解してよい。
Anthropic の Lean 実装では、この条件が GaloisRepIsIrreducible ℚ P.freyCurve P.p という述語で表され、FreyPackage.Mazur_Frey が Frey 曲線についてその既約性を証明する。
ここでも、一般の楕円曲線に対する既約性を全て証明しているわけではない。FLT の証明経路で必要な Frey 曲線に対象を限定している。\(p\ge17\) の範囲では Mazur の Eisenstein イデアルを用いる議論を Frey 曲線に必要な形で形式化している[10]。小さい素数については別の経路を使い、\(p=5\) は降下法、\(p=7,11,13\) は Kummer の正則素数に関する結果などを利用して、その指数の FLT 自体を先に閉じる[6]。
この段階で、証明の対象は次のように変わった。
\[
a^p+b^p=c^p
\longrightarrow
E
\longrightarrow
E[p]
\longrightarrow
\bar\rho_{E,p}
\]
3.2 楕円曲線とモジュラー形式をフロベニウスのトレースで結ぶ
モジュラー性を理解するには、「楕円曲線がモジュラー形式になる」と考えるより、両者から得られる算術データが一致すると見る方が分かりやすい。
まず、モジュラー形式の側を考える。複素上半平面
\[
\mathcal H=\{\tau\in\mathbf C\mid \operatorname{Im}\tau>0\}
\]
上の変数 \(\tau\) に対して、
\[
q=e^{2\pi i\tau}
\]
と置く。重さ 2 の正規化された Hecke 固有形式は、\(q\)-展開として
\[
f(q)=\sum_{n=1}^{\infty}a_n(f)q^n
\]
と書ける。ここで係数 \(a_n(f)\) は単なる Taylor 展開の係数ではなく、Hecke 演算子に関する固有値として数論的情報を持つ。
一方、楕円曲線 \(E\) を考える。ある素数 \(\ell\) で係数を \(\ell\) で割った有限体 \(\mathbf F_\ell\) 上へ還元し、その還元が特異点を持たない場合を良い還元と呼ぶ。このとき有限集合 \(E(\mathbf F_\ell)\) の点を数え、
\[
a_\ell(E)
=
\ell+1-\#E(\mathbf F_\ell)
\]
を定義する。\(\ell+1\) から実際の点数がどれだけずれているかを表す量であり、楕円曲線に作用する Frobenius の trace と一致する。
楕円曲線 \(E\) がモジュラーであるという主張は、適切な レベル \(N\) を持つ重さ 2 の正規化固有形式 \(f\) が存在し、少なくとも良い還元を持つ素数 \(\ell\) について、
\[
a_\ell(E)=a_\ell(f)
\]
という対応が成立することとして表せる。幾何学的な対象である楕円曲線と、解析的に定義されるモジュラー形式が、各素数で得られる算術データを通じて同じ情報を持つという主張である。
この対応は mod-\(p\) ガロア表現の側からも読める。楕円曲線の表現 \(\bar\rho_{E,p}\) とモジュラー形式から構成される mod-\(p\) ガロア表現が対応すれば、良い素数 \(\ell\) についてフロベニウスのトレースが \(p\) を法として一致する。
\[
a_\ell(E)\equiv a_\ell(f)\pmod p
\]
まず mod \(p\) の世界でモジュラー形式との対応を確立し、その情報を標数 0 の楕円曲線そのもののモジュラー性へ持ち上げる、というのが Wiles の証明で使われる基本的な流れになる。
最初の入口として使われるのが \(p=3\) である。mod 3 ガロア表現が既約であれば、その像は比較的小さく、Langlands–Tunnell の結果を利用できる。Tunnell は八面体型の 2 次元 Artin 表現について Artin 予想を証明し、対応する重さ 1 のモジュラー形式の存在へ接続した[11]。Wiles の議論では、そこから重さ 2 の剰余モジュラー性を得る。
Anthropic の形式化でも、この部分を「Langlands–Tunnell の一般理論を全て形式化する」という形にはしていない。Frey 曲線の証明経路で必要になる、全射的な mod 3 表現で、行列式が円分指標となる八面体型の場合を扱い、重さ 1 のモジュラー形式を経由して必要な剰余モジュラー性を得る。
ただし剰余モジュラー性だけでは、元の楕円曲線 \(E\) 自身がモジュラーであることまでは分からない。分かるのは、ガロア表現を mod \(p\) に落としたときにモジュラー形式由来の表現と一致するという情報である。
そこで必要になるのがモジュラー性持ち上げである。概念的には、
\[
\bar\rho
\text{ is modular}
\]
という mod-\(p\) の情報と、変形可能なガロア表現に対する局所条件から、
\[
\rho
\text{ is modular}
\]
という標数 0 の表現のモジュラー性を導く。
その背後にあるのが変形環と Hecke 代数の比較である。ある mod-\(p\) ガロア表現 \(\bar\rho\) を固定し、指定した局所条件を保ちながら標数 0 へ持ち上げる全ての変形を表す普遍変形環を \(R\) とする。一方、対応するモジュラー形式へ作用する Hecke 演算子から Hecke 代数 \(T\) を作る。
モジュラー形式からガロア表現を構成できるので、自然な環準同型
\[
R\longrightarrow T
\]
が得られる。ここで
\[
R\cong T
\]
を証明できれば、許された条件を満たすガロア表現の変形が Hecke 代数、すなわちモジュラー形式の側から生じることが分かる。Wiles の主論文は、このモジュラー性持ち上げを使って半安定楕円曲線のモジュラー性を FLT へ接続した[12]。証明の修正では Taylor と Wiles がパッチングを用いて必要な環論的性質を確立した[13]。Diamond は変形環と Hecke 環の議論をさらに整理・拡張しており、Anthropic の形式化もこの系統の定式化を利用している[14]。
ここで別の分岐がある。楕円曲線 \(E\) の mod 3 表現が既約なら、Langlands–Tunnell から剰余モジュラー性を得て、モジュラー性持ち上げを適用できる。しかし mod 3 表現が可約であれば、この経路はそのままでは使えない。
そこで Wiles は 3–5 スイッチを使う。対象の曲線 \(E\) と同じ mod 5 表現を持つ別の楕円曲線 \(E’\) を構成し、\(E’\) の mod 3 表現が既約になるように選ぶ。
\[
E'[5]\cong E[5]
\]
まず \(E’\) の mod 3 表現に Langlands–Tunnell とモジュラー性持ち上げを適用し、\(E’\) がモジュラーであることを示す。すると \(E'[5]\) はモジュラー形式由来なので、同型な \(E[5]\) も剰余モジュラー性を持つ。その mod 5 の情報にモジュラー性持ち上げを適用して、元の \(E\) のモジュラー性を得る。
流れを整理すると、
\[
\begin{cases}
\bar\rho_{E,3}\text{ irreducible}
&\Rightarrow
\text{modularity at }3
\\
\bar\rho_{E,3}\text{ reducible}
&\Rightarrow
E’
\Rightarrow
\text{modularity of }E’
\Rightarrow
\bar\rho_{E,5}\text{ modular}
\Rightarrow
\text{modularity of }E
\end{cases}
\]
となる。3–5 スイッチは証明上の技巧に見えるが、役割は明確である。直接使えない mod 3 表現に固執せず、同じ mod 5 情報を共有する別の曲線を経由して、モジュラー性持ち上げに必要な入口を作っている。
Anthropic の形式化では、この一連の結果が最終的に FreyPackage.frey_isModular へ集約される。上位の FLT 証明から見ると、内部に Langlands–Tunnell、3–5 スイッチ、変形理論、Taylor–Wiles パッチングが存在していても、必要な出力は「この Frey 曲線はモジュラーである」という一つの検証済み定理になる[6]。
3.3 レベル降下でレベル 2 まで落とす
Frey 曲線がモジュラーであることが分かっても、まだ矛盾にはならない。モジュラーな楕円曲線は多数存在するからである。FLT の反例から作った Frey 曲線が持つ特殊な局所的性質を使い、対応するモジュラー形式の レベル を極端に小さくする必要がある。
モジュラー形式の レベル \(N\) は、変換則を課す合同部分群 \(\Gamma_0(N)\) を指定する整数である。
\[
\Gamma_0(N)
=
\left\{
\begin{pmatrix}
a & b\\
c & d
\end{pmatrix}
\in
\operatorname{SL}_2(\mathbf Z)
\;\middle|\;
c\equiv0\pmod N
\right\}
\]
\(N\) が変われば、許されるモジュラー形式の空間も変わる。ガロア表現の側では、このレベルは表現が各素数でどの程度分岐しているかを記述する導手と密接に対応する。
分岐とは、ある素数 \(q\) の近くでガロア表現が非自明な局所的振る舞いをすることを意味する。どの素数で、どの程度分岐しているかをまとめた整数が導手であり、モジュラー形式に対応するガロア表現では、その導手と レベル が対応する。
Frey 曲線は任意の楕円曲線ではない。元の等式
\[
a^p+b^p=c^p
\]
と正規化条件によって、判別式や各素数での還元が非常に特殊になる。この特殊性から、mod-\(p\) ガロア表現について「ある素数は レベル に本質的には必要ない」という条件が得られる。
Ribet のレベル降下定理は、既約な mod-\(p\) ガロア表現がある レベル \(N\) のモジュラー形式から生じており、特定の素数 \(q\mid N\) について必要な局所条件を満たすとき、その \(q\) を取り除いた低い レベル のモジュラー形式からも同じ mod-\(p\) 表現が生じることを示す[15]。
模式的には、
\[
\bar\rho
\text{ modular of レベル }N
\]
から、条件を満たす素因数 \(q\) を除去して、
\[
\bar\rho
\text{ modular of レベル }\frac{N}{q}
\]
へ進む操作である。これを適用できる素数について一つずつ繰り返せば、レベル を小さくしていける。
ただし、「同じ表現」と言うと強すぎる場合がある。Anthropic の形式化で ModularRepOfLevel が保持するのは、必要な素数でフロベニウスのトレースが mod \(p\) で合同になるという情報であり、一般の表現そのものの同型を直接定義しているわけではない。公開された証明経路も、この点を明示している。
Frey 曲線については、まず \(abc\) を割る素数を中心とした平方因子を持たないレベルへ整理する。その後、奇素数 \(q\neq p\) を Ribet 型のレベル降下で取り除き、\(p\) 自身についても Mazur–Ribet 型の議論を適用する。こうして残る レベル は 1 または 2 まで縮小される。
レベル 1 の重さ 2 の尖点形式も存在しないため、最終的に必要になるのはレベル 2 の場合である。Anthropic の Lean 実装では、この一連の処理が FreyPackage.level_lowering_to_two にまとめられている[6]。その出力は、Frey 曲線のモジュラー性とガロア表現の既約性を仮定したとき、
\[
0\neq f\in S_2(\Gamma_0(2))
\]
を満たす尖点形式 \(f\) が存在するという命題である。
ここで \(S_2(\Gamma_0(2))\) は、合同部分群 \(\Gamma_0(2)\) に対する重さ 2 の尖点形式全体が作る複素ベクトル空間である。レベル降下が導くのは、単に「何らかのモジュラー形式がある」ことではない。非常に小さなレベル 2 に属する非零の尖点形式 が存在しなければならないという、強く限定された結論である。
証明の流れはこの時点で、
\[
\text{FLT counterexample}
\Rightarrow
\text{Frey curve}
\Rightarrow
\begin{cases}
\text{irreducible}\\
\text{modular}
\end{cases}
\Rightarrow
0\neq f\in S_2(\Gamma_0(2))
\]
まで進んでいる。最初の整数方程式の反例が、最終的には特定のモジュラー形式の存在を要求する命題へ変換されたことになる。
3.4 最後は「存在する」と「零空間」が衝突する
反証法の最後に必要なのは、レベル降下によって要求されたモジュラー形式が実際には存在しないことを示すことである。
レベル 2、重さ 2 の尖点形式の空間について、
\[
S_2(\Gamma_0(2))=\{0\}
\]
が成り立つ。これは、この空間の次元が 0 であり、含まれる尖点形式は零元だけであることを意味する。
一方、レベル降下は
\[
0\neq f\in S_2(\Gamma_0(2))
\]
を要求した。同じ空間について「全ての要素が 0 である」と「0 ではない要素が存在する」を同時に成立させることはできない。
\[
\left(
0\neq f\in S_2(\Gamma_0(2))
\right)
\land
\left(
S_2(\Gamma_0(2))=\{0\}
\right)
\Rightarrow
\bot
\]
ここで \(\bot\) は矛盾を表す。矛盾を引き起こした最初の仮定は、素数 \(p\ge5\) に対して
\[
a^p+b^p=c^p
\]
を満たす非零整数の反例が存在するという仮定だった。よって、そのような反例は存在しない。
全体を一本につなぐと、次のようになる。
\[
\begin{aligned}
a^p+b^p=c^p
&\Rightarrow
\text{Frey package}\\
&\Rightarrow
\text{Frey curve }E\\
&\Rightarrow
\bar\rho_{E,p}\text{ is irreducible}\\
&\Rightarrow
E\text{ is modular}\\
&\Rightarrow
\text{レベル降下 to }2\\
&\Rightarrow
0\neq f\in S_2(\Gamma_0(2))\\
&\Rightarrow
S_2(\Gamma_0(2))\neq\{0\}\\
&\Rightarrow
\bot
\end{aligned}
\]
この証明の特徴は、最初と最後だけを見ると大きく異なる数学を扱っている点にある。出発点は整数のべき乗方程式であり、途中で楕円曲線、有限体上の線形代数、ガロア表現、モジュラー形式、Hecke 代数、変形環を経由し、最後は特定の尖点形式空間の次元へ到達する。
それぞれの分野が無関係に並んでいるわけではない。前の対象から次の対象へ情報を保存した写像があり、その写像によって元の反例が持つ制約を別の数学的言語へ移している。
\[
\text{整数論}
\longrightarrow
\text{楕円曲線}
\longrightarrow
\text{ガロア表現}
\longrightarrow
\text{モジュラー形式}
\]
Frey 曲線は反例の算術情報を楕円曲線へ埋め込み、\(p\)-捩れ はその情報を有限体上のガロア表現へ変換する。モジュラー性はガロア表現をモジュラー形式側の算術情報へ接続し、レベル降下は Frey 曲線特有の局所条件を使って候補となるモジュラー形式の空間をレベル 2 まで狭める。そこで空間自体が零であることと衝突する。
人間の数学では、この巨大な証明を「Frey 曲線は既約かつモジュラーであり、Ribet の定理により矛盾する」と圧縮して参照できる。形式証明では、その圧縮された一文の内部にある各主張も、さらにその前提となる主張も、最終的には Lean が検査できる定理へ分解しなければならない。
Anthropic の形式化で興味深いのは、この数学上の依存関係が、そのままソフトウェア上の依存関係として露出していることである。FreyPackage.no_frey_package を閉じるために必要なのは、FreyPackage.Mazur_Frey、FreyPackage.frey_isModular、FreyPackage.level_lowering_to_two、ModularForm.S2_Gamma0_2_eq_zero という主要な定理である。
4. 数学上の依存関係を Lean の型と定理へ写す
4.1 Lean では命題が型になり、証明がその型を持つ項になる
前章では、フェルマーの最終定理の反例から Frey 曲線を作り、ガロア表現の既約性、モジュラー性、レベル降下を経て、最終的に存在しない尖点形式を要求するところまで数学上の依存関係を追った。形式化では、この各段階を自然言語の説明として保存するだけでは足りない。Lean が機械的に検査できる命題と証明へ変換する必要がある。
Lean の基礎にある依存型理論では、数学的命題は Prop に属する型として表され、その命題の証明は、その型を持つ項として表される。Theorem Proving in Lean 4 でも、依存型理論と命題を型として扱う考え方が論理体系の基礎として説明されている[16]。
命題を \(P\)、その証明を \(p\) とすると、Lean では
\[
p:P
\]
という型付けで表せる。左側の \(p\) が証明項、右側の \(P\) が証明すべき命題である。数学者が「\(P\) の証明を書いた」と表現するところを、Lean は「項 \(p\) が型 \(P\) を持つか」という型検査の問題として扱う。
単純な例として、命題 \(P\) を仮定して同じ \(P\) を結論とする命題を考える。
\[
P\rightarrow P
\]
Lean では、与えられた証明 \(h:P\) をそのまま返せばよい。
1 2 3 | theorem identity (P : Prop) : P → P := by intro h exact h |
人間から見れば自明な証明だが、Lean の内部では、P → P という型を持つ項が構成されている。intro h によって \(P\) の証明 \(h\) を仮定し、exact h によって同じ型 \(P\) を持つ項を返す。この小さな例と、フェルマーの最終定理の形式化は、規模こそ大きく異なるが、カーネルが最終的に判定する原理は同じである。
ここで、Lean のソースコードとカーネルが直接扱う証明項の間には elaborator が入る。人間や AI が書く Lean ソースコードには、省略された型、暗黙引数、型クラスによるインスタンス探索、tactic による証明手順などが含まれている。elaborator はそれらを解決し、より明示的な内部表現へ変換する。
処理を単純化すると、
\[
\text{Lean ソースコード}
\longrightarrow
\text{elaboration}
\longrightarrow
\text{証明項}
\longrightarrow
\text{カーネルによる型検査}
\]
という流れになる。AI が Lean ソースコードを生成した段階では、まだその証明は確定していない。構文として正しくても型が合わない場合があり、tactic が途中で失敗する場合もあり、必要な前提を証明できない場合もある。elaboration が成功し、最終的に構成された証明項をカーネルが型検査して初めて、その定理宣言が受理される。
この分離は、AI を使う場合に特に重要になる。Claude が証明を生成した過程を Lean カーネルが理解する必要はない。どのような自然言語による推論を行ったか、何回失敗したか、どの候補から最終コードへ到達したかもカーネルの判定条件には入らない。最終的に得られた項が要求された型を持つかだけを確認する。
前章の記法を使えば、利用可能な公理、定義、既証明定理の集合を \(\Gamma\)、証明対象を \(P\) としたとき、Lean が最終的に確認するのは
\[
\Gamma\vdash P
\]
である。Claude の生成能力は、左辺から右辺へ到達する候補を探索するために使われる。一方、到達したという事実を確定するのは Lean カーネルである。生成と検証が、ここで具体的なソフトウェア構成として分離される。
4.2 数学上の対象を Lean の定義、構造体、述語へ変換する
数学を Lean へ形式化する作業は、論文の文章を Lean の構文へ逐語的に翻訳する作業ではない。数学上で使われる対象を型や構造体として定義し、その対象が満たす性質を述語として表し、定理同士を明示的な依存関係で接続する必要がある。
Anthropic が公開したリポジトリでは、最終定理、証明経路、使用する公理、既存の Mathlib や FLT 形式化プロジェクトから利用した部分、検証方法が明示されている[17]。前章で追った数学と代表的な Lean 上の表現を対応させると、次のようになる。
| 数学上の対象 | Lean 上の主な表現 | 形式化によって固定される内容 | 証明経路での役割 |
|---|---|---|---|
| FLT の反例を正規化したデータ | FreyPackage | 素数 \(p\)、反例となる整数、互いに素であること、合同条件などを一つの対象として保持する。 | 反例の存在から Frey 曲線を構成するための入力になる。 |
| Frey 曲線 | P.freyCurve | FreyPackage に格納された整数から決まる Weierstrass 曲線を具体的な数学的対象として与える。 | 整数方程式の問題を楕円曲線とガロア表現の問題へ移す。 |
| mod-\(p\) ガロア表現の既約性 | GaloisRepIsIrreducible | \(E[p]\) に非自明なガロア不変部分空間が存在しないという条件を述語として固定する。 | Frey 曲線についてレベル降下などを適用するための前提になる。 |
| モジュラー性 | IsModular | 楕円曲線の \(a_\ell\) と適切な重さ 2 の固有形式の係数との対応を形式的な条件として持つ。 | Frey 曲線をモジュラー形式側へ接続する。 |
| レベル降下 | FreyPackage.level_lowering_to_two | 必要な仮定から レベル 2 の非零の尖点形式を得られることを定理として固定する。 | Frey 曲線の存在から \(S_2(\Gamma_0(2))\) の非零元を要求する。 |
| レベル 2、重さ 2 の尖点形式空間が零 | ModularForm.S2_Gamma0_2_eq_zero | 任意の \(f : CuspForm (\Gamma_0(2))\,2\) に対して \(f=0\) となることを証明する。 | レベル降下が要求した非零元と直接衝突する。 |
| Frey package は存在できない | FreyPackage.no_frey_package | 任意の FreyPackage を仮定すると False を導けることを定理として表す。 | FLT の反例から構成された FreyPackage 自体を排除する。 |
ここで FreyPackage のような構造体を設ける意味は、関連する値を一つの入れ物へまとめることだけではない。各値が満たすべき条件も同じ対象へ結び付けることで、後続定理が「正規化された FLT の反例」という前提を曖昧な自然言語ではなく、型として受け取れるようになる。
例えば後続定理が引数として P : FreyPackage を受け取れば、P に含まれる指数が素数であることや、反例が正規化条件を満たすことは、個々の定理が別々に「そう仮定する」必要がない。構造体の定義が、その時点で利用可能な情報の境界になる。
同じことが性質についても成立する。数学の文章では「Frey 曲線の mod-\(p\) 表現は既約である」と書けるが、Lean では「既約」という語の意味そのものを GaloisRepIsIrreducible という述語で固定し、その述語を満たす証明を構成する必要がある。
つまり、形式化では数学上の名詞と形容詞が、それぞれ
\[
\text{mathematical object}
\longrightarrow
\text{type / structure}
\]
および
\[
\text{mathematical property}
\longrightarrow
\text{predicate / proposition}
\]
へ変換される。その結果、「何を意味しているのか」が定理の型として機械可読になる。
前章の最後で現れた
\[
S_2(\Gamma_0(2))=\{0\}
\]
も同じである。Anthropic の形式化では、対応する定理は概念的には次の形になる。
1 2 3 | theorem ModularForm.S2_Gamma0_2_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 2) 2) : f = 0 |
数学では「このベクトル空間は零空間である」と集合全体について記述する。一方、この Lean 定理は、その空間の任意の要素 \(f\) を受け取り、\(f=0\) を返す形で同じ内容を表している。
\[
\forall f\in S_2(\Gamma_0(2)),\quad f=0
\]
という量化された命題が定理の引数と結論へ展開されているのである。
レベル降下側では、反対に非零の \(f\) が存在することを得る。そこで得た \(f\) を S2_Gamma0_2_eq_zero へ入力すれば \(f=0\) が返り、非零性と衝突する。人間向け証明で「しかし \(S_2(\Gamma_0(2))=0\) なので矛盾」と一行で済ませる箇所が、Lean では関数への引数と戻り値のように明示的に接続される。
4.3 数学上の証明グラフが Lean の定理の依存関係になる
この対応が最も直接見えるのが、FreyPackage.no_frey_package の周辺である。前章で確認した数学上の構造では、FreyPackage が存在すると仮定した後、主に四つの結果を組み合わせて矛盾へ到達した。
\[
\begin{aligned}
&\text{FreyPackage.Mazur\_Frey}\\
&\text{FreyPackage.frey\_isModular}\\
&\text{FreyPackage.level\_lowering\_to\_two}\\
&\text{ModularForm.S2\_Gamma0\_2\_eq\_zero}
\end{aligned}
\]
Anthropic のリポジトリでは、no_frey_package の証明ファイルが実際にこれらの定理ファイルを依存先として読み込んでいる。
1 2 3 4 | import Theorems.Thm_FreyPackage_Mazur_Frey import Theorems.Thm_FreyPackage_frey_isModular import Theorems.Thm_FreyPackage_level_lowering_to_two import Theorems.Thm_ModularForm_S2_Gamma0_2_eq_zero |
これは単なるファイル整理ではない。数学上の証明グラフとソフトウェア上の依存グラフが対応している。
\[
\begin{cases}
\text{Mazur\_Frey}\\
\text{frey\_isModular}\\
\text{level\_lowering\_to\_two}\\
\text{S2\_Gamma0\_2\_eq\_zero}
\end{cases}
\longrightarrow
\text{no\_frey\_package}
\]
Mazur_Frey が Frey 曲線の mod-\(p\) ガロア表現の既約性を与え、frey_isModular がモジュラー性を与える。その二つを レベル_lowering_to_two に渡すと、レベル 2 の非零の尖点形式 \(f\) が得られる。S2_Gamma0_2_eq_zero は同じ \(f\) が 0 であることを返す。非零性と \(f=0\) が衝突するため False が得られる。
論理構造だけを書けば、
\[
I(P)
\land
M(P)
\Rightarrow
\exists f,\,
f\in S_2(\Gamma_0(2))
\land
f\neq0
\]
と
\[
\forall f\in S_2(\Gamma_0(2)),\quad f=0
\]
を組み合わせて、
\[
P:\mathrm{FreyPackage}
\Rightarrow
\bot
\]
を得ている。ここで \(I(P)\) は既約性、\(M(P)\) はモジュラー性を表す。
形式証明では、この上位定理が成立するためには、依存先の定理がそれぞれ先に受理されている必要がある。もし Mazur_Frey の証明が未完成なら、そこへ依存する no_frey_package も確定できない。level_lowering_to_two の型が変更されれば、それを利用する証明も再検査が必要になる。
つまり、依存関係は文献上の参照ではなく、型検査に参加する実際の依存関係である。人間の論文では「Ribet の定理より」と書いた先の証明が正しいことを読者や査読者が外部知識として受け入れる場合がある。Lean では、最終成果物の依存閉包に含まれる定理が全てカーネルの検査対象へ入る。
これが大規模形式化で重要になる。最終定理を一つの巨大な証明項として一度に生成する必要はない。証明を定理 \(T_1,T_2,\ldots,T_n\) へ分解し、
\[
T_i
\leftarrow
\{T_{j_1},T_{j_2},\ldots,T_{j_k}\}
\]
という依存関係を持たせればよい。各 \(T_i\) は、必要な下位定理が確定した後に独立して証明できる。
ここで数学上の「補題を証明してから主定理へ進む」という構造が、AI エージェントに仕事を割り当てるための計算可能なグラフへ変わる。どの定理が未証明なのか、どの定理が別の未証明定理を待っているのか、どの定理は依存先が全て閉じて作業可能なのかを、自然言語の進捗報告ではなく依存グラフから判断できる。
4.4 定理文と証明を分離すると、定理を作業単位として扱える
Anthropic の成果物では、この依存関係を扱いやすくするために定理文と証明実装を分離している[6]。概念的には、
Theorems/Thm_X_y.lean
に公開される定理宣言を置き、
P2M/Sol/S_X_y.lean
にその定理を成立させる証明を置く構成である。
この分離は、通常のソフトウェアにおけるインターフェースと実装の関係に近い。後続定理が必要とするのは、「この命題が証明済みである」という論理的な契約であり、その証明が内部でどの補題や tactic を使って構築されたかを毎回知る必要はない。
例えば定理 \(T\) の型が
\[
A\rightarrow B
\]
で固定されているとする。後続定理から見れば、\(A\) の証明を与えれば \(B\) の証明を取得できることが契約になる。内部の証明実装を別の証明へ置き換えても、型 \(A\rightarrow B\) が維持されていれば、後続定理の論理的な利用方法は変わらない。
| 層 | 保持する内容 | 後続から見えるもの | 変更した場合の影響 |
|---|---|---|---|
| 定理文 | 入力となる前提と、出力となる結論の型を定義する。 | どの前提から何を利用できるかという論理的な契約が見える。 | 型を変更すると、それを利用する後続定理へ影響が伝播する。 |
| 証明 | 定理文で要求された型を持つ証明項を構成する。 | 受理済みであれば、内部の証明方法を知らなくても定理を利用できる。 | 定理文を維持したまま証明方法だけを変更できる。 |
| カーネル | 証明項が定理文の型を本当に持つかを検査する。 | 受理された宣言だけが確定済み定理になる。 | 証明候補が不正なら宣言自体が確定しない。 |
この構造は、大規模 AI エージェントで扱う作業単位を明確にする。エージェントに「フェルマーの最終定理を証明せよ」という一つの巨大な仕事を与えるのではなく、「この定理文を、現在利用可能な定理群から証明せよ」という局所的な仕事へ分割できる。
各作業単位は、概念的には
\[
T_i=
(S_i,D_i,P_i)
\]
と考えられる。\(S_i\) は証明すべき定理文、\(D_i\) は利用可能な依存定理の集合、\(P_i\) は生成された証明項である。
エージェントが担当するのは、
\[
(S_i,D_i)
\longrightarrow
P_i
\]
という探索である。しかし作業完了条件は「エージェントが答えを返した」ことではない。
\[
\operatorname{KernelCheck}(P_i,S_i)
=
\mathrm{accept}
\]
となった時点で初めて \(T_i\) が確定する。この定義によって、AI の作業状態と数学的な証明状態を同じ定理ノード上で管理できる。
この分離には計算資源上の意味もある。数万定理の巨大な証明実装全てを各エージェントが常に読み込む必要はない。現在証明しようとしている定理の定理文と必要な依存先を中心に扱えばよく、証明済み定理の内部を毎回再構成する必要もない。Anthropic が定理文と証明の分離を導入した理由の一つも、この大規模なコンパイルと協調作業を成立させることにある[17]。
ここまでで、前章の数学的な証明構造は次のようにソフトウェアへ写された。
| 数学上の構造 | Lean / 実行系での構造 |
|---|---|
| 数学的対象 | 型、構造体、定義として表現する。 |
| 数学的性質 | Prop に属する述語として表現する。 |
| 定理 | 要求する型を持つ定理宣言として表現する。 |
| 証明 | 定理の型を持つ証明項として表現する。 |
| 補題への依存 | 定理の依存関係と import 依存関係として表現する。 |
| 証明済み | カーネルが証明項を受理した状態として判定する。 |
この構造があるため、数万個の定理を一つの AI が最初から最後まで記憶し続ける必要はない。数学上の依存関係を外部グラフとして保持し、証明可能になったノードを別々のエージェントへ割り当て、カーネルが受理したノードだけを次の依存先として公開できる。
5. 3 万個の定理を一つのエージェントに覚えさせない
5.1 初期試行は、証明能力より状態管理で崩れた
前章までで、フェルマーの最終定理の形式化は、一つの巨大な証明をそのまま生成する作業ではなく、多数の定理文を依存関係に沿って一つずつ閉じる作業として表現できることを確認した。この構造なら、理論上は複数の AI エージェントへ定理を分担できる。しかし、定理を分割しただけでは大規模な協調作業は成立しない。
Anthropic は、初期の Claude エージェントが局所的には有用な証明を生成したものの、やがてプロジェクト全体の状態を追跡できなくなり、互いの成果を効果的に再利用できなくなったと報告している。最終成果物の非定型部分の約 7 % は、この初期試行で作られた成果に由来した[4]。
この失敗から分かるのは、一つの定理を証明できる能力と、数万定理からなる形式化を完遂できる能力が同じではないことである。局所的な作業だけを考えれば、エージェントに必要なのは現在の定理文、利用可能な補題、その周辺の定義である。しかしプロジェクト全体を進めるには、それとは別に、
- どの定理が既に証明されたか
- どの定理がまだ未証明か
- どの定理が別の定理の完了を待っているか
- どの定理は今すぐ証明可能か
- 既に同じ内容の定理が別名で存在していないか
という状態を継続的に管理しなければならない。
例えば、上位定理 \(T_4\) が \(T_1,T_2,T_3\) に依存するとする。
\[
T_1,T_2,T_3\longrightarrow T_4
\]
エージェントが \(T_4\) を担当した時点で \(T_1\) と \(T_2\) は証明済みだが \(T_3\) が未証明なら、\(T_4\) を完成させることはできない。ところが、その依存状態をエージェント自身の会話履歴だけに保持していると、コンテキストの更新や別エージェントとの作業分担によって「\(T_3\) が未完了である」という情報を失う可能性がある。
逆方向の問題も起こる。別のエージェントが既に \(T_3\) を証明したにもかかわらず、その成果を発見できなければ、同じ定理を再び証明しようとする。局所的にはどちらの作業も正しくても、プロジェクト全体では重複計算になり、並列化による効率向上が失われる。
つまり、大規模形式化には二種類の状態がある。
| 状態の種類 | 保持する内容 | 主な利用者 | 失われた場合の影響 |
|---|---|---|---|
| 局所作業状態 | 現在証明している定理、直前のエラー、試した証明方針、必要な定義などを保持する。 | 個々の AI エージェントが現在の証明を進めるために利用する。 | 現在の証明探索をやり直す必要が生じる。 |
| プロジェクト状態 | 全定理の依存関係、証明済み・未証明の区別、再利用可能な成果、作業可能な定理を保持する。 | 複数エージェントの作業割り当てと証明全体の進行管理に利用する。 | 重複作業、未解決依存への着手、証明済み成果の見落としが発生し、全体の進行が崩れる。 |
モデルのコンテキストを長くすれば、局所作業状態をより多く保持できる。しかし、数万定理の依存状態を毎回モデルへ読み込ませる方法では、プロジェクトが大きくなるほど入力も増え続ける。しかも必要なのは過去の全文ではなく、「現在どの定理が確定しているか」という最新状態である。
このため、大規模形式化では記憶容量そのものより、状態をどこに保持し、必要なときにどう再構成するかが制約になる。初期試行で不足していたのは、Claude が一つの証明を書く能力だけではなく、数万個の証明作業を一つの継続的な計算として成立させる外部状態管理だった。
5.2 Prove2Me は定理の状態を DAG として外部化する
この問題に対して使われたのが Prove2Me である。Prove2Me は Shuze Chen、Kunal Marwaha、Xiaoyang Lu、Henry Yuen、Tianyi Peng による大規模数学形式化の協調基盤で、AI エージェントが複数の定理を分担し、既に形式化された結果を再利用しながら大きな数学的課題を進める仕組みを提供する[18]。
Prove2Me の中心にあるのは、証明全体を定理の有向非巡回グラフ、DAG として扱う考え方である。ある定理 \(T_i\) が、
\[
D_i=
\{T_{i_1},T_{i_2},\ldots,T_{i_k}\}
\]
という定理群を前提として必要とするなら、その依存関係を
\[
T_{i_1},T_{i_2},\ldots,T_{i_k}
\longrightarrow
T_i
\]
という有向辺として記録する。
このとき定理 \(T_i\) が作業可能になる条件は、単純には依存先集合 \(D_i\) の全要素が証明済みであることである。証明済み定理の集合を \(C\) とすれば、
\[
D_i\subseteq C
\]
を満たす定理は、必要な前提が全て利用可能になっている。
この条件を使えば、「次に何を証明するか」をエージェント自身の記憶に任せる必要がない。DAG の状態から機械的に作業候補を列挙できる。
\[
R=
\{T_i\mid T_i\notin C\land D_i\subseteq C\}
\]
\(R\) は現在作業可能な定理の集合である。複数の定理が \(R\) に含まれていれば、それらは互いの完了を待たずに並列で処理できる。
例えば、
\[
T_1\longrightarrow T_3
\]
\[
T_2\longrightarrow T_4
\]
\[
T_3,T_4\longrightarrow T_5
\]
という DAG があるとする。最初に \(T_1\) と \(T_2\) が証明済みなら、\(T_3\) と \(T_4\) は同時に作業できる。両方がカーネルに受理された時点で初めて \(T_5\) が作業可能になる。
\[
\begin{array}{ccccc}
T_1 & \longrightarrow & T_3 & \searrow & \\
& & & & T_5 \\
T_2 & \longrightarrow & T_4 & \nearrow &
\end{array}
\]
ここで並列化可能かどうかを判断するために、各エージェントが他のエージェントの会話履歴を読む必要はない。必要な情報は「どのノードが閉じたか」という DAG 上の状態として外部に存在する。
Anthropic は、Prove2Me の導入によって定理の依存関係を外部状態として管理し、エージェントが証明可能な定理を選択しながら協調できるようになったと説明している。また定理文と証明を分離することで Lean のコンパイルの負荷を抑え、定理文に自然言語の説明を持たせることで検索と再利用を支援した[4]。
この設計では、過去の全作業履歴を保存することと、現在必要な状態を復元することを分けられる。ある定理を担当するエージェントに必要なのは、数万定理の全文ではない。現在の定理文と、その依存先として利用可能な定理、その証明に必要な周辺定義を取得できればよい。
既稿で扱った「モデルの外側を設計する」という考え方も、この構造と接続する[2]。AI が長期作業を継続するために必要なのは、過去の会話を無制限に保持することではなく、後から現在状態を再構成できる外部表現を持つことである。Prove2Me では、その状態表現が定理 DAG として具体化されている。
| 観点 | モデル内部だけで管理する場合 | DAG として外部管理する場合 |
|---|---|---|
| 証明済み定理の把握 | 証明済み定理を会話やコンテキストから思い出す必要がある。 | 証明済みノードの状態を外部から取得できる。 |
| 依存関係の追跡 | 未解決の依存関係をエージェント自身が追跡する必要がある。 | 依存辺から作業可能な定理を機械的に判定できる。 |
| 他エージェント成果の再利用 | 別エージェントの成果を発見できないと重複作業が発生する。 | 証明済み定理を共有資産として検索し、再利用できる。 |
| 必要コンテキスト量 | プロジェクトの拡大とともに必要なコンテキストも増え続ける。 | 各エージェントには現在の定理に必要な局所情報を渡せる。 |
長期エージェントの能力を「どれだけ長い文脈を保持できるか」だけで測ると、この違いを捉えにくい。数万定理の形式化で必要なのは、全履歴を常時保持することではなく、確定済み成果を再利用可能な状態として保存し、現在の作業に必要な依存だけを取り出せることである。
5.3 定理ノードは「後続が利用できる確定状態」になる
DAG を作っただけでは、どのノードを「完了」とみなすかはまだ決まらない。AI エージェントが定理に対する Lean ソースコードを生成した時点でノードを閉じてしまえば、その証明が誤っていた場合に、誤った前提が上位定理へ伝播する。
形式証明では、この完了条件を Lean カーネルの受理へ置ける。
定理 \(T_i\) の定理文を \(S_i\)、AI が生成した証明候補を \(P_i\) とする。ノードを確定済みに移す条件は、
\[
\operatorname{KernelCheck}(P_i,S_i)
=
\mathrm{accept}
\]
である。
エージェントが「証明できた」と報告したことではなく、カーネルが証明項を定理文の型として受理したことが状態遷移の条件になる。
一つの定理ノードの状態を単純化すると、次のように表せる。
\[
ext{定義済み}
\longrightarrow
ext{作業中}
\longrightarrow
\text{候補}
\longrightarrow
\begin{cases}
\text{検証済み}\\
ext{拒否}
\end{cases}
\]
rejected になった候補は修正して再度検証できるが、検証済みになるまでは後続定理の依存先へ加えない。この違いによって、生成器が誤ることと、証明グラフへ誤りが混入することを分離できる。
| 状態 | その時点で存在するもの | 正しさの扱い | 後続定理からの利用 |
|---|---|---|---|
| 定理文を定義 | 証明対象となる定理文が存在する。 | 何を証明するかは固定されたが、その命題の証明はまだ存在しない。 | 証明済み前提としては利用できない。 |
| 証明作業中 | AI が依存定理や定義を使って証明候補を探索している。 | 途中結果に正しさの保証はない。 | 利用できない。 |
| 候補証明を生成 | Lean ソースコードとして証明候補が存在する。 | AI が完成したと判断しただけで、カーネルによる型検査はまだ完了していない。 | 利用できない。 |
| カーネルが拒否 | 型不一致や未解決 goal などを含む候補がある。 | 証明として成立していないことが判明している。 | 利用できない。 |
| カーネルが受理 | 定理文の型を持つ証明項が存在する。 | 形式体系の範囲で定理が証明済みとして確定する。 | DAG 上の後続定理が依存先として利用できる。 |
この構造は、既稿で扱った「未確定な状態を一件ずつ閉じる」という考え方を、通常のソフトウェア開発より厳密な条件で実現している[3]。一般的な開発タスクでは、「実装完了」「レビュー済み」「テスト成功」といった複数の条件を人間が組み合わせて完了を判断する。形式証明では、少なくとも定理の論理的正当性についてはカーネル受理という明確な判定条件を置ける。
このとき、DAG のノードは作業項目であると同時に、検証済み知識の単位にもなる。ノード \(T_i\) が検証済みへ移れば、それは単に「担当エージェントの仕事が終わった」という意味ではない。上位定理が前提として利用できる新しい論理的事実が追加されたことを意味する。
証明済み定理の集合を \(C_t\) とし、時刻 \(t\) に新しく \(T_i\) がカーネルに受理されたとする。状態は、
\[
C_{t+1}=C_t\cup\{T_i\}
\]
と更新できる。その結果、それまで依存条件を満たしていなかった別の定理 \(T_j\) について、
\[
D_j\subseteq C_{t+1}
\]
が初めて成立すれば、\(T_j\) が新しく作業可能になる。
つまり、一件の証明完了は一件の進捗記録にとどまらない。依存グラフの状態を変化させ、新しい作業を解放するイベントになる。
この構造によって、複数エージェントの並列実行も安全に組み立てやすくなる。エージェント A と B が別々の定理を同時に証明していても、それぞれの出力はカーネルに受理されるまで DAG の確定状態へ入らない。どちらかが失敗しても、もう一方の検証済み定理は独立して利用できる。
\[
\text{AI エージェント}
\longrightarrow
\text{証明候補}
\longrightarrow
\text{Lean カーネル}
\longrightarrow
\text{検証済み定理 DAG}
\]
ここで AI エージェントは探索を並列化する層、Lean カーネルは各候補を確定する層、DAG は確定した成果を蓄積して次の作業へ接続する層として役割が分かれている。
5.4 11 日という期間は、モデル単体の速度では説明できない
Anthropic が報告した 11 日という期間だけを見ると、「Claude が人間より高速に数学を証明した」という比較へ向かいやすい。しかし、実際の工程で高速化されたのは一人の数学者に相当する直列作業だけではない。
第一に、証明対象が定理 DAG へ分解されたことで、依存しない定理を複数のエージェントが並列に処理できる。第二に、既に証明済みの定理は再利用可能な外部資産となり、各エージェントが同じ数学を最初から再構成する必要がない。第三に、候補証明の正しさを人間が逐一読んで判断するのではなく、Lean カーネルが機械的に判定できる。第四に、失敗した候補を確定状態へ入れないため、探索そのものは高い失敗率を許容できる。
この違いを、単一エージェントの直列処理と比較すると分かりやすい。
| 観点 | 単一エージェントへ全体を保持させる方式 | DAG と検証器を使う方式 |
|---|---|---|
| 状態管理 | エージェント自身が過去の証明と現在状態を保持する必要がある。 | 証明済み状態と依存関係を外部 DAG に保持できる。 |
| 並列化 | 一つの推論系列として扱うため、独立部分を同時に進めにくい。 | 依存関係のない定理を複数エージェントへ同時に割り当てられる。 |
| 再利用 | 過去の成果をコンテキストから再発見する必要がある。 | 検証済み定理を共有資産として検索・利用できる。 |
| 失敗処理 | 誤った途中状態が後続推論へ影響する可能性がある。 | カーネルに拒否された候補は検証済み DAG へ入らない。 |
| 完了条件 | モデル自身や人間が「終わった」と判断する必要がある。 | 定理単位ではカーネル受理を完了条件にできる。 |
最終工程では約 60 億の出力トークンが使われ、数十の Claude エージェントが協調したと Anthropic は報告している[4]。この計算量は、11 日という値が単純な「一つのモデルが一つの証明を高速に書いた時間」ではないことを示している。大量の探索を並列に行い、検証済み成果だけを共有状態へ蓄積する分散的な工程だった。
したがって、この成果から読み取るべき性能指標は、個々の定理を何秒で解いたかだけではない。大規模な依存グラフについて、
\[
ext{作業候補抽出}
\rightarrow
ext{割当}
\rightarrow
ext{候補生成}
\rightarrow
ext{検証}
\rightarrow
ext{共有}
\]
という循環をどれだけ継続できたかが重要になる。
モデルは generate の中心を担うが、全体を成立させるには discover と assign を行う状態管理、verify を行う Lean カーネル、検証済み定理を publish して後続へ渡す共有基盤が必要になる。どれか一つが欠ければ、数万定理の形式化は局所的な成功の集合にとどまり、最終定理まで接続しない。
フェルマーの最終定理の形式化で Prove2Me が示したのは、長期 AI エージェントの能力をモデル内部の記憶量だけで拡張する必要はないということである。現在状態を外部に持ち、作業を検証可能なノードへ分け、確定済みノードだけを次の仕事へ接続すれば、個々のエージェントは局所的な問題へ集中できる。
その結果、数万定理というプロジェクトの大きさと、一つのエージェントが一度に保持しなければならない情報量を切り離せる。プロジェクト全体は巨大でも、各エージェントの作業面は局所的に保てる。この分離が、長期・大規模な AI 作業を成立させるための構造になる。
ただし、DAG 上で定理が検証済みになったからといって、最終成果物全体の信頼性について全ての問題が解消するわけではない。個々の証明項を Lean カーネルが受理していても、最終定理が本来のフェルマーの最終定理と同じ定理文なのか、許可されていない公理へ依存していないか、Lean カーネル自体の実装だけへ信頼を集中させてよいかという別の検証境界が残る。
6. 1,300 万行を人間が読まずに何を検証したのか
6.1 Lean カーネルは、生成された証明の型付けを最終命題まで再確認する
前章までで、Claude が生成した Lean ソースコードは、そのまま確定済みの数学として扱われるのではなく、定理単位で Lean カーネルの検証を通過したものだけが依存グラフへ追加されることを確認した。しかし、約 1,300 万行という規模になると、別の疑問が生じる。人間が全てのソースコードを読んでいないのに、何を根拠として「証明全体が正しい」と判断できるのか。
Anthropic の公開リポジトリでは、Lean 4.33.1 と Mathlib v4.33.0 を固定し、依存する Mathlib を含めてソースコードからビルドしている。README に記載された検証では 60,475 モジュールがビルドされ、最終定理を含む全宣言が Lean カーネルの検査を通る[17]。
ここで重要なのは、Lean が 1,300 万行のソースコードを「人間のように読んで理解する」わけではないことである。前章で見たように、Lean ソースコードは elaborator によってより明示的な term へ変換される。カーネルが最終的に受け取るのは、その term と型の関係である。
\[
\text{ソースコード}
\longrightarrow
\text{elaborator}
\longrightarrow
\text{証明項}
\longrightarrow
\text{カーネル}
\]
カーネルの仕事は、各証明項が宣言された型を本当に持つかを、Lean の型理論の規則に従って確認することである。定理 \(T_i\) の証明項を \(p_i\)、定理文を表す型を \(P_i\) とすれば、各宣言について
\[
p_i:P_i
\]
が成立するかを確認する。上位定理が下位定理を利用している場合、その下位定理も既に型検査された宣言として参照される。最終定理だけを検査しているのではなく、その依存 closure に含まれる定義と定理が連鎖的にカーネルの検査対象になる。
この構造では、証明の長さと検証原理の複雑さを分離できる。1,300 万行の証明には数論、代数幾何、モジュラー形式、ガロア表現など極めて複雑な数学が含まれるが、カーネルが行う最終判定は、それぞれの宣言が少数の基本的な型付け規則に従っているかという検査へ還元される。
この考え方は定理証明支援系の信頼構造の中心にある。巨大な証明を生成した全てのプログラム、tactic、AI、検索処理を同じ強さで信用する必要はない。これらは誤った証明候補を生成してもよい。最終的に小さな信頼するカーネルが受理しなければ、その候補は定理にならない。
\[
\text{large untrusted generator}
\longrightarrow
\text{small trusted 検査器}
\]
Anthropic の成果では、この境界をさらに明確にするため、最終定理が依存する公理も確認している。公開された検査結果では、依存する標準公理は
- propext
- Classical.choice
- Quot.sound
の 3 つである[17]。これらはいずれも Lean が標準的に利用する公理であり、FLT を成立させるためだけに新しい数学的公理を追加したわけではない。
さらにリポジトリ内の証明モジュールについては、未証明部分を残す sorry、新しい axiom の追加、カーネルの通常の証明経路を迂回し得る native_decide、unsafe、extern、implemented_by、partial def などが存在しないことも検査されている[17]。
ここで sorry の意味は特に重要である。Lean では開発途中に証明を省略して定理を仮置きできるが、その場合は実質的に「この命題には証明があるものとして先へ進む」という未検証の前提が入る。最終成果物に sorry が残っていれば、依存グラフが全てつながって見えても、その途中に機械検証されていない穴が残る。
Anthropic の検証で確認しているのは、
\[
\text{最終定理}
\longleftarrow
\text{検証済み依存閉包}
\]
が途中の未証明仮定なしに閉じていることである。約 3 万個の定理を人間が一つずつ査読する代わりに、その全てを同じ型理論の判定規則へ落とすことで、証明量の増加と人間の読解量を切り離している。
| 対象 | 生成側で起こり得ること | Lean カーネルが確認すること |
|---|---|---|
| AI の推論 | 誤った数学、不要な探索、失敗した証明方針を含む可能性がある。 | 推論過程そのものは検査対象にしない。 |
| Lean ソースコード | 構文エラー、型エラー、誤った定理利用を含む可能性がある。 | elaboration 後の term が要求された型を持つかを検査する。 |
| 依存定理 | 数万個の補題へ連鎖的に依存する。 | 依存 closure に含まれる宣言の型付けを検査する。 |
| 未証明仮定 | sorry や追加 axiom を使えば見かけ上は証明を完成できる。 | 最終成果物が許可された公理以外へ依存していないことを確認できる。 |
この意味で、人間が読まなくてよくなったのは「数学の意味」ではなく、「1,300 万行の各行が形式体系の規則を守っているか」という機械的な検査である。人間は証明の意味や定理文の妥当性を読む必要があるが、個々の型変換が正しくつながっているかを全て手作業で追跡する必要はなくなる。
6.2 comparator は「正しく証明したが、証明した命題が違う」という抜け道を検査する
Lean カーネルが証明項を受理しただけでは、まだ一つの重要な問題が残る。カーネルが保証するのは、「与えられた定理文が証明された」ということである。その定理文自体を生成側が自由に変更できるなら、本来より弱い命題へ書き換えてから完全な証明を作ることもできる。
例えば、本来証明したい命題を
\[
P
\]
とする。AI が誤って、あるいは意図せず、より弱い命題
\[
P’
\]
を定義し、
\[
\Gamma\vdash P’
\]
を完全に証明したとしても、Lean カーネルにとっては何も問題がない。カーネルは \(P’\) が本来の課題 \(P\) と同じ意味かどうかを知らないからである。
この問題を確認するために使われたのが Lean FRO の comparator である[19]。comparator は、信頼する Challenge 側と、検査対象となる Solution 側を分離して比較する。
概念的には、
\[
P_{\mathrm{challenge}}
\stackrel{?}{=}
P_{\mathrm{solution}}
\]
を確認する仕組みである。
ただし、単に定理の表示文字列を比較しているわけではない。定理文が同一であることに加え、その定理文が参照する定数の内容、solution が利用する公理、Lean カーネルによる再検査まで確認する[19]。
FLT リポジトリでは、Mathlib だけに依存してフェルマーの最終定理を記述した Challenge.lean を基準として用意し、Anthropic が生成した solution 側の最終定理と比較している[17]。その結果、最終定理の定理文と参照する定数が challenge 側と一致し、許可された公理以外への依存がなく、証明全体を Lean カーネルが再検査できることを確認している。
この検査によって閉じようとしている抜け道を整理すると、次のようになる。
| 抜け道 | Lean カーネル単体 | comparator を加えた場合 |
|---|---|---|
| 弱い別定理を証明する | その定理自体が正しく証明されていれば受理する。 | Challenge と Solution の定理文の一致を確認する。 |
| 同じ名前の定義を別内容へ差し替える | その環境内で整合していれば受理し得る。 | 定理文が参照する定数も基準側と比較する。 |
| 追加公理を導入する | 追加された axiom を前提として定理を証明できる。 | 許可された axiom 以外への依存を検査する。 |
| 証明項が不正 | カーネルが拒否する。 | Solution 全体をカーネルで再検査するため同様に拒否される。 |
この構造を前章までの生成器と検証器のモデルへ加えると、単純な
\[
V(y)=\mathrm{accept}
\]
だけではなく、
\[
V(y,P_{\mathrm{trusted}})
=
\mathrm{accept}
\]
という形になる。候補証明 \(y\) が内部的に整合しているだけでなく、その証明対象が信頼された仕様 \(P_{\mathrm{trusted}}\) と一致しているかまで検査する。
ただし comparator を導入しても、信頼が完全に消えるわけではない。comparator 自身の README は、Challenge 側の import による依存関係全体、サンドボックス、Lean カーネルなどを信頼基盤として置いている[19]。
形式検証で実現しているのは、
\[
\text{何も信頼しない}
\]
ではなく、
\[
\text{信頼基盤を小さく明示する}
\]
という構造である。何を信頼しているのかを曖昧な「AI は十分賢い」という前提に置かず、Challenge、形式体系、カーネル、sandbox といった具体的な構成要素へ限定する。
6.3 nanoda は、Lean カーネルと別実装の検証器で同じ証明環境を再確認する
comparator を使っても、最終的な証明検査を Lean カーネル一つに依存している限り、そのカーネル実装に欠陥があった場合には同じ誤りを見逃す可能性がある。そこで Anthropic は、Lean 本体とは別に実装された型検査器である nanoda を使い、Lean から lean4export で書き出した環境を再検査している。
nanoda は Rust で実装された Lean 4 用の型検査器であり、エクスポートされた環境に含まれる宣言を別実装で検査する[20]。Anthropic の報告では、1,052,234 個の宣言を nanoda がエラーなしで受理した[17]。
検証経路を概念的に書くと、次のようになる。
\[
\text{Claude が生成した Lean ソースコード}
\longrightarrow
\text{Lean の elaboration}
\longrightarrow
\text{elaboration 済み環境}
\longrightarrow
\begin{cases}
\text{Lean カーネルによる検査}\\
\text{lean4export}\longrightarrow\text{nanoda による検査}
\end{cases}
\]
ここで独立しているのは型検査器の実装であり、Lean ソースコードの解析や elaboration までを nanoda が独立にやり直しているわけではない。Lean が構成した環境を一方では Lean カーネルが検査し、もう一方ではエクスポートした宣言を nanoda が別実装の型検査器として確認する。Lean カーネル固有の実装不具合が存在しても、nanoda が同じ不具合を独立に持っていなければ検出できる可能性がある。
これは、単純に同じ検査を二回実行することとは異なる。同じ Lean カーネルを二回起動した場合、決定的な同一実装は同じ入力に同じ判断を返す。カーネルに系統的な実装不具合があれば、二回とも同じ誤判定になる。
\[
K(y)=\mathrm{accept}
\]
を二回確認しても、信頼先は依然として \(K\) 一つである。
別実装 \(K_1\) と \(K_2\) を使えば、
\[
K_1(y)=\mathrm{accept}
\land
K_2(y)=\mathrm{accept}
\]
という条件へ変えられる。実装上の失敗原因が独立しているほど、片方だけの実装不具合による誤受理を検出しやすくなる。
| 検証方法 | 追加できる確認 | 残る共通前提 |
|---|---|---|
| Lean カーネルのみ | 証明項が Lean の型規則に従うことを検査する。 | Lean カーネル実装そのものを信頼する必要がある。 |
| 同じ Lean カーネルを複数回実行 | 一時的な実行失敗などは再確認できる。 | 同じ実装不具合は全実行で共有される。 |
| Lean カーネルと nanoda | 別実装でも同じ宣言が受理されることを確認できる。 | 両者が共有する形式仕様や入力定理の意味までは独立検査にならない。 |
ここでも「独立検証」という語を強く解釈しすぎるべきではない。nanoda が別実装であっても、検査対象となる Lean の型理論や宣言の意味そのものは共有している。形式体系自体の仕様が誤っていれば、二つの検査器が正確に同じ仕様を実装していても、その誤りは検出できない。
また Anthropic は nanoda をそのまま無変更で使ったわけではなく、今回の非常に大きな環境を処理するために 4 件のパッチを適用したと説明している[17]。一つは進捗表示、三つは定義的等価性の探索の性能改善であり、Anthropic は型付け規則を弱めたり削除したりする変更ではないとしている。
この情報は、独立検証の信頼性を評価するときに無視できない。別実装であることだけでなく、その実装へどの変更を加え、その変更が判定規則に影響するかまで確認する必要があるからである。形式検証では、検証器の名前よりも信頼基盤の具体的な範囲が重要になる。
ここまでの検証を重ねると、信頼構造は一段ずつ異なる問題を閉じている。
\[
\begin{aligned}
\text{Lean カーネル}
&:\quad \text{証明項の型付け}\\
\text{comparator}
&:\quad \text{証明対象と信頼する Challenge の一致}\\
\text{nanoda}
&:\quad \text{別実装による型検査の再確認}
\end{aligned}
\]
一つの巨大な検証器が全てを保証しているのではない。異なる失敗条件に対して別々の検査を重ねている。
6.4 それでも形式検証の外側には、仕様、意味、由来の境界が残る
ここまで見ると、フェルマーの最終定理が完全に「機械によって正しさを保証された」と言いたくなる。しかし、その表現には保証範囲を明示する必要がある。形式検証が非常に強いのは、形式化された命題と形式化された導出についてである。その外側には別の判断が残る。
第一の境界は、形式命題と人間が意図した数学との対応である。
公開リポジトリ自身も、機械生成された定理名や自然言語説明と、実際の Lean 定理文が食い違う場合には、Lean 定理文を正とすると明記している[17]。
例えば定理に
FreyPackage.Mazur_Frey
という名前が付いていたとしても、Lean カーネルが検査するのは「これは Mazur の定理を正しく表現しているか」という数学史的・意味論的な主張ではない。実際の定理文に書かれた型が証明されているかだけである。
人間が期待する命題を \(M\)、形式化された Lean 定理文を \(P\) とすると、カーネルが確認できるのは
\[
\Gamma\vdash P
\]
である。
一方、
\[
M\equiv P
\]
という意味上の対応は、形式化を設計した人間が確認しなければならない。最終的な FLT の定理では comparator によって標準 Mathlib 側の Challenge と照合することで、この境界をかなり狭めている。しかし 3 万個近い中間定理の名称や自然言語説明が、数学者の期待する既知定理と完全に同じ意味を持つことまで comparator が保証するわけではない。
第二の境界は、形式化された定理の強さである。Anthropic の成果は Mazur、Langlands–Tunnell、Ribet、Wiles などの名前を持つ結果を含むが、それぞれの一般定理を全文字通り形式化しているわけではない。FLT の証明経路で必要になる強さに限定した定理が多数存在する[17]。
例えば Mazur について形式化されている中心的な結果は Frey 曲線の \(E[p]\) の既約性であり、一般の楕円曲線について Mazur が証明した有理同種写像の分類全体をそのまま定理として再構成しているわけではない。同じように、Ribet のレベル降下も今回の Frey 曲線の表現に必要な条件に絞られている。
そのため、
\[
\text{定理 name}
\neq
\text{entire classical 定理}
\]
となる場合がある。形式化された定理文を正とするというリポジトリの注意は、この意味でも重要になる。
第三の境界は、成果物の由来である。Anthropic の形式化は、Claude が空のリポジトリから 11 日間で数学全体を構築したものではない。Mathlib に加え、Imperial College London の FLT 形式化プロジェクト、leanprover-community の flt-regular など、既存の人間主導の形式化資産を利用・適応している[17]。
Imperial College London のプロジェクトは長期的な人間主導の FLT 形式化であり、2026 年時点でも進行中である。現行リポジトリ自身が、最上位の証明経路に sorryAx が残っていることを確認できる[21]。
Anthropic の成果は、その未完成部分を含む既存の形式化資産を土台にしながら、必要な定理を追加・接続して 最終定理まで一貫した sorry のない証明環境を作ったものと位置付けるのが正確である。
この違いを整理すると、11 日という値が何を測っているのかも明確になる。
| 解釈 | 11 日という値が意味するか | 理由 |
|---|---|---|
| フェルマーの最終定理を数学史上初めて発見した時間 | 意味しない。 | 数学的証明経路は Frey、Serre、Ribet、Wiles、Taylor–Wiles らによって既に確立されている。 |
| 必要な数学を全てゼロから Lean へ形式化した時間 | 意味しない。 | Mathlib、Imperial College London の FLT プロジェクト、flt-regular など既存資産を利用している。 |
| 既存資産と既知証明経路を使い、残る大規模形式化を AI エージェントが接続して完全な機械検証可能成果物へした工程時間 | この意味で読むことができる。 | Anthropic が報告している最終 multi-agent formalization campaign の期間だからである。 |
第四の境界として、人間による数学的レビューと機械検証も区別する必要がある。証明検査器が全宣言を受理したことは、形式体系内での正しさについて非常に強い証拠になる。しかし、それは論文としての説明の分かりやすさ、既存数学との意味上の対応、形式化方針の妥当性まで自動的に査読したことを意味しない。
機械検証と人間のレビューは、同じものを二重に確認する関係ではなく、異なる失敗を検出する。
| 確認主体 | 主に確認できること | 確認しにくいこと |
|---|---|---|
| Lean カーネル | 形式的な証明項が定理文の型を持つか。 | 定理文が人間の意図した数学を表しているか。 |
| comparator | 最終定理文と信頼する Challenge が形式的に一致するか。 | 信頼する Challenge 自体が人間の意図を正しく形式化しているか。 |
| 独立型検査器 | 特定のカーネル実装だけに依存せず型検査が成立するか。 | 共有している型理論や形式仕様そのものの妥当性。 |
| 数学者 | 形式定理文と既知数学の意味対応、証明構成、説明の妥当性を評価できる。 | 1,300 万行の全証明項を人手で逐一型検査すること。 |
この分業によって、形式検証の役割が明確になる。人間を検証工程から排除するのではない。人間が担当する必要のない機械的な整合性確認をカーネルへ移し、人間は仕様、意味、形式化の射程、既存数学との対応といった上位の判断へ集中できる。
1,300 万行を人間が読まずに済むという事実は、「人間による理解が不要になった」という意味ではない。むしろ、人間が確認すべき対象を変えている。全証明項の局所的な型整合性を読む代わりに、
\[
\text{何を定理として固定したか}
\]
\[
\text{何を公理として許したか}
\]
\[
\text{どの既存数学と対応しているか}
\]
\[
\text{どこまでを独立した検証器で再確認したか}
\]
を読む。
ここまでの検証経路をまとめると、Anthropic の成果は単一の「AI が証明した」という矢印では表せない。
\[
\begin{aligned}
\text{human mathematical specification}
&\longrightarrow
\text{Lean 定理文}\\
&\longrightarrow
\text{Claude-generated 証明候補s}\\
&\longrightarrow
\text{Lean カーネル検証}\\
&\longrightarrow
\text{comparator verification}\\
&\longrightarrow
\text{independent nanoda による検査}
\end{aligned}
\]
各段階が別の種類の誤りを狭めている。Claude の誤生成はカーネルが拒否する。別の定理を証明する問題は comparator が検査する。一つのカーネル実装だけへの依存は nanoda によって緩和する。それでも、最初にどの数学的定理文を形式化するかという境界は人間側に残る。
この構造を見ると、「AI をどこまで信用できるか」という問いの置き方自体が変わる。Claude を数学者として全面的に信用する必要はない。Claude が作った候補を、どの仕様に対して、どの検証器が、どの信頼基盤の上で受理したかを確認すればよい。
7. AI の正しさを上げるだけでなく、正しさを確定する場所を設計する
フェルマーの最終定理の形式化で確認できたのは、Claude が一度も誤らない生成器になったということではない。Anthropic 自身が初期試行でエージェントがプロジェクト状態を追跡できなくなったことを報告している[4]。最終工程で成立したのは、誤りを発生させない仕組みではなく、候補証明を検証し、受理された定理だけを後続の依存先へ渡す仕組みである。
この仕組みでは、数学上の主要な定理依存を Lean の定理依存として明示し、Prove2Me がその依存関係を作業管理にも利用する。Claude エージェントは局所的な証明候補を生成し、Lean カーネルが受理した定理だけが確定済み状態になる。comparator は最終定理が信頼された課題文と一致するかを確認し、nanoda はエクスポートされた宣言を別実装の型検査器で再確認する。生成、状態管理、仕様照合、型検査が別の役割として分かれている。
これは既稿で扱った「AI がテストを通しても、『正しい』とは限らない」という問題に対して、形式証明がどこまで条件を強くできるかを示す例でもある[1]。通常のテストが選択した観測条件を確認するのに対し、Lean は形式化された命題について、その命題を導く証明項を検査できる。ただし、形式検証が確定するのは形式仕様の内側であり、人間が意図した数学をどの命題として固定するかという境界は残る。
したがって、この事例を「AI の出力は形式検証すれば全て安全になる」と一般化することはできない。自然言語の企画、経営判断、要件定義、研究上の仮説のように、完全な形式仕様や決定的な検証器を構成できない仕事もある。一方、型検査、静的解析、モデル検査、形式仕様、コンパイル、テストなどの受理条件を定義できる部分では、AI の生成結果をそのまま確定状態として扱わず、検証結果を工程の境界として利用できる。
このとき人間の役割は消えるのではなく、検証器が直接扱えない上流へ移る。何を仕様として固定するか、どの公理・定義・ライブラリーを信頼するか、形式化された定理が本来の意味と一致しているか、どの検証器を信頼基盤に含めるかは、人間が判断しなければならない。1,300 万行を人間が逐語的に読む必要を減らせても、数学的意味と信頼境界の判断まで自動化されたわけではない。
フェルマーの最終定理の形式化が示したのは、生成量が人間の逐語レビュー能力を超えても、対象を形式命題と検証可能な証明へ変換できるなら、生成量と人間の局所検査量を切り離せるということである。そのために必要だったのは、より強い Claude だけではなく、定理依存を保持する外部状態、候補と確定を分ける完了条件、Lean カーネル、comparator、nanoda を組み合わせた検証経路だった。
AI を信用することと、AI が作った成果を信頼可能な状態へ変えることは別の設計問題である。前者だけを追えば、評価指標はモデルの正答率や推論能力へ集中する。後者まで含めれば、形式仕様、外部状態、依存関係、完了条件、独立した検証器、信頼基盤までが設計対象になる。AI がより多くを生成する時代ほど、生成器の性能だけでなく、どこで正しさを確定するかを先に設計する必要がある。
参考文献
- id774, AI がテストを通しても、「正しい」とは限らない（2026-09-01）. https://blog.id774.net/entry/2026/09/01/5534/
- id774, AI に仕事を任せるには、モデルの外側を設計する（2026-08-21）. https://blog.id774.net/entry/2026/08/21/5544/
- id774, AI による大規模開発では、未確定な状態を一件ずつ閉じる（2026-08-15）. https://blog.id774.net/entry/2026/08/15/5503/
- Anthropic, Formalizing Fermat’s Last Theorem (2026-09-04). https://www.anthropic.com/research/formalizing-fermats-last-theorem
- Mathlib, Mathlib.NumberTheory.FLT.Basic. https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/FLT/Basic.html
- Anthropic, The route of the proof, PROOF-PATH.md (2026). https://github.com/anthropics/fermats-last-theorem/blob/main/PROOF-PATH.md
- Henri Darmon, Fred Diamond, Richard Taylor, Fermat’s Last Theorem, Current Developments in Mathematics 1 (1995). https://www.math.mcgill.ca/darmon/pub/Articles/Expository/05.DDT/paper.pdf
- Kenneth A. Ribet, From the Taniyama-Shimura conjecture to Fermat’s last theorem, Annales de la Faculté des sciences de Toulouse 11 (1990), 116–139. https://afst.centre-mersenne.org/articles/10.5802/afst.698/
- Jean-Pierre Serre, Sur les représentations modulaires de degré 2 de Gal(Q̄/Q), Duke Mathematical Journal 54 (1987), 179–230. https://www.college-de-france.fr/media/jean-pierre-serre/UPL5835292064138487263_Serre_Repr.modulaires_Galois.pdf
- Barry Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l’IHÉS 47 (1977), 33–186. https://pmihes.centre-mersenne.org/articles/10.1007/BF02684339/
- Jerrold Tunnell, Artin’s conjecture for representations of octahedral type, Bulletin of the American Mathematical Society 5 (1981), 173–175. https://doi.org/10.1090/S0273-0979-1981-14936-3
- Andrew Wiles, Modular elliptic curves and Fermat’s Last Theorem, Annals of Mathematics 141 (1995), 443–551. https://annals.math.princeton.edu/1995/141-3/p01
- Richard Taylor, Andrew Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572. https://annals.math.princeton.edu/1995/141-3/p02
- Fred Diamond, On deformation rings and Hecke rings, Annals of Mathematics 144 (1996), 137–166. https://annals.math.princeton.edu/articles/13301
- Kenneth A. Ribet, On modular representations of Gal(Q̄/Q) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476. https://eudml.org/doc/143793
- Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich, Theorem Proving in Lean 4. https://lean-lang.org/theorem_proving_in_lean4/
- Anthropic, Fermat’s Last Theorem in Lean 4 (2026). https://github.com/anthropics/fermats-last-theorem
- Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, Tianyi Peng, Prove2Me: An Open Collaborative Platform for Scaling Math Formalization (2026). https://arxiv.org/abs/2608.28433
- Lean FRO, Comparator. https://github.com/leanprover/comparator
- ammkrn, nanoda_lib. https://github.com/ammkrn/nanoda_lib
- Imperial College London, Fermat’s Last Theorem Lean formalisation project. https://github.com/ImperialCollegeLondon/FLT