AI 生成証明を Lean 4 の型検査と公理監査で検証する

AI が Lean のコードを生成しただけでは、証明が完了したとは扱えません。必要なのは、先に証明対象となる形式命題を固定し、生成された証明候補を AI とは別の検証系で受理または拒否することです。

2026 年 9 月、Anthropic は Claude が Lean を用いてフェルマーの最終定理の完全な機械検証可能な証明を構築したと発表しました。11 日間で 30,300 個の定理を証明し、約 1,300 万行の Lean コードを生成したと報告されています[1]。この規模では、人間が生成物を 1 行ずつ読んで正誤を確定する方式は現実的ではありません。

この記事ではフェルマーの最終定理そのものは扱いません。数行の Lean で、次の違いを実際に確認します。

• 有限個の例が通ること
• 任意の自然数について定理が成立すること
• 誤った証明候補が拒否されること
• lean が終了しただけでは検証条件として不足する場合があること
• AI 生成証明の信頼水準に応じて検証方法を変えること

結論を先に書くと、AI 生成証明の完了条件は単純な「生成済み」ではありません。少なくとも、固定した形式命題に対して Lean が証明を受理し、許可していない公理へ依存していないことを確認するところまでを分離した条件として持つ必要があります。未レビューの AI 生成コードを高い保証水準で扱う場合は、さらに独立した再検証が必要です。

検証環境を Lean 4.33.1 に固定する

以下は macOS または Linux のシェルを前提とします。Lean の公式インストール手順では、Lean のバージョン管理に elan を使用します[2]。2026 年 9 月 8 日時点の公式リリース一覧では、4.34 系はリリース候補であり、最新の非リリース候補として Lean 4.33.1 が掲載されています[3]。

作業用ディレクトリーを作成し、Lean 4.33.1 を固定します。

mkdir lean-ai-proof-check
cd lean-ai-proof-check

elan toolchain install leanprover/lean4:v4.33.1
elan override set leanprover/lean4:v4.33.1
lean --version

lean --version の出力に 4.33.1 が含まれることを確認します。

この記事の例では Mathlib を使いません。Lean 本体で扱える Nat と等式だけに限定し、「生成された証明候補を何に対して検証するのか」を確認します。

有限個の例だけを Lean に確認させる

最初に、自然数について 3 個の具体例を確認します。

finite_examples.lean を次の内容で作成します。

finite_examples.lean

example : (0 : Nat) + 0 = 0 := by
  rfl

example : (1 : Nat) + 0 = 1 := by
  rfl

example : (2 : Nat) + 0 = 2 := by
  rfl

実行します。

lean finite_examples.lean

エラーが出なければ、Lean が確認したのは次の 3 命題です。

0 + 0 = 0
1 + 0 = 1
2 + 0 = 2

ここから直接確認できるのは、この 3 個について等式が成立したことです。

一方、求めたい性質が「任意の自然数 n について n + 0 = n」であるなら、3 個の具体例を確認するだけでは対象が異なります。1,000 個や 100 万個へ増やしても、有限個の入力を列挙して確認することと、全ての自然数を量化した命題を証明することは同じではありません。

全ての自然数について同じ性質を証明する

次は、具体的な数値を並べる代わりに、任意の自然数 n を対象にします。

universal.lean を作成します。

universal.lean

theorem add_zero_all (n : Nat) : n + 0 = n := by
  rfl

#print axioms add_zero_all

実行します。

lean universal.lean

この定理では n に 0、1、2 のような具体値を指定していません。定理の型そのものが、任意の n : Nat に対して n + 0 = n が成立することを表しています。

Lean では命題を型として扱い、証明をその型を持つ項として扱います。theorem に書いた命題に対応する証明項を構成し、最終的にその型が成立するかを検査します[4]。

ここで使っている rfl は反射律による証明です。この例では n + 0 が定義に従って n へ簡約されるため、等式が成立します。

#print axioms add_zero_all も重要です。この例では追加の公理を使っていないため、add_zero_all が公理へ依存していないことを確認できます。後で AI が生成した証明を検査するとき、この確認が別の意味を持ちます。

誤った証明候補を Lean に拒否させる

次に、成立しない命題へ同じ rfl を与えます。

invalid.lean を作成します。

invalid.lean

theorem add_one_wrong (n : Nat) : n + 1 = n := by
  rfl

実行します。

lean invalid.lean

このコードは受理されません。n + 1 と n は定義上同じ式にはならないため、rfl では証明できません。

この時点で、AI を証明候補の生成器として使う場合の最小構造を作れます。

固定した形式命題
        |
        v
AI が証明候補を生成
        |
        v
Lean が候補を検査
   |             |
   v             v
受理            拒否

AI がコードを返した時点では、まだ候補です。構文が正しくても、もっともらしい説明が付いていても、対象となる形式命題に対する証明として Lean が受理しなければ確定済みにはしません。

lean の終了ステータスだけを完了条件にしない

ここには重要な落とし穴があります。

次のコードは、数学的には誤った命題です。

sorry_example.lean

theorem add_one_fake (n : Nat) : n + 1 = n := by
  sorry

#print axioms add_one_fake

Lean の sorry は未完成の証明を一時的に通すための仕組みです。Lean の公式リファレンスでは、sorry は sorryAx という公理として追跡され、完成した証明では残すべきではないものとして説明されています[5]。

実行します。

lean sorry_example.lean

rfl を使った誤証明とは異なり、このファイルは sorry を使っているという警告を出しながら処理できます。そのため、単純に「lean コマンドが終了した」ことだけを完了条件にすると、未完成の証明を通す余地が残ります。

#print axioms add_one_fake を確認すると、依存公理として sorryAx が現れます。Lean は定理が推移的に依存する公理を追跡でき、sorryAx のほか、独自に宣言した公理も確認できます[5]。

AI 生成証明を通常の開発工程で受け入れるなら、少なくとも次を別々に確認します。

1. 証明対象の形式命題が期待した内容で固定されていること
2. Lean の検査がエラーや警告なしで完了すること
3. #print axioms で許可していない公理への依存がないこと

#print axioms で標準的に現れる可能性がある propext、Classical.choice、Quot.sound は Lean の標準公理です。一方、sorryAx は未完成の証明を示し、それ以外の独自公理が出た場合は、その公理を前提にして初めて定理が成立していることになります[5]。

AI 生成証明は信頼水準に応じて検証方法を変える

Lean の公式リファレンスは、証明の検証を 1 種類に固定していません。証明生成側をどこまで信頼するかに応じて、検証を段階的に強くしています[5]。

段階	確認方法	主に検出するもの
通常の対話的利用	Lean が定理を受理し、エラーや警告がないことを確認する	未完了ゴール、現在の定理内の sorry、型検査エラー
公理の監査	#print axioms theoremName	依存先に残った sorryAx、独自公理
再検証	lean4checker --fresh	.olean に保存された証明をカーネルで再検査し、処理系内部の一部の問題を切り離す
高リスクな検証	comparator と外部チェッカー	悪意ある証明コードや、定理文自体をすり替える攻撃まで含む強い検証

公式リファレンスでは、未レビューの AI 生成証明やプログラムを、悪意ある可能性を考慮すべき対象に含めています[5]。この点は、AI が意図的に攻撃するかどうかという人格的な話ではありません。生成された任意のコードを信頼せず、入力として扱うというセキュリティー上の境界です。

lean4checker を使う場合、公式手順ではプロジェクトを lake build した後、対象定理を含むモジュールに対して次のように再検査します[5]。

lean4checker --fresh ModuleName

さらに高い保証が必要な場合、Lean は comparator と外部チェッカーを使う方法を「Gold Standard」として説明しています。信頼できる環境側で定理文を検証対象として固定し、提案された証明を隔離環境で構築したうえで、証明項と定理文の一致を Lean のカーネルや独立した外部チェッカーで再確認します[5]。

この記事の数行の例で comparator まで導入する必要はありません。ただし、AI が大規模な証明コードやメタプログラムを生成し、それを人間が十分にレビューしない運用へ移るなら、「Lean でコンパイルできた」という条件だけでは検証設計として不足します。

Lean が受理しても人間の意図まで証明したことにはならない

もう一つの境界は、証明コードではなく定理文です。

たとえば、本来確認したい条件が

任意の自然数 n について n + 0 = n

だったとします。

ところが、AI に定理文まで生成させて、誤って次だけを証明していた場合を考えます。

theorem wrong_scope : (0 : Nat) + 0 = 0 := by
  rfl

この定理自体は正しく、Lean も問題なく受理します。しかし、本来の要求である「任意の自然数」については証明していません。

Lean が確認するのは、形式化された定理文に対して証明が成立しているかです。人間が何を証明したかったのかを、Lean が形式体系の外側から推測するわけではありません。Lean の公式検証ガイドも、「定理に有効な証明があるか」と「その定理文が何を意味するか」を分けて扱っています[5]。

そのため、AI 生成証明を工程へ組み込むときは、少なくとも次の 2 つを別の境界として扱います。

• 仕様化の境界: 人間が意図した性質と、固定した Lean の定理文が一致しているか
• 証明の境界: その定理文に対する証明候補が、設定した検証条件を通過したか

フェルマーの最終定理の形式化でも、この区別は重要です。自然言語で「フェルマーの最終定理」と呼ぶだけではなく、対象となる数、指数の条件、正の整数という前提、不等式としての結論を形式命題として固定し、その命題へ至る証明を検査する必要があります。この仕様化と証明の境界については、元の記事で大規模な形式化の構造まで含めて整理しています[6]。

完了条件を「AI が生成した」から「定理と証明を独立に検証した」へ変える

最小例を通して、次の 3 状態を区別できました。

AI が証明候補を生成した
        |
        | まだ未確定
        v
Lean が固定済みの形式命題に対して証明を受理した
        |
        | 公理依存と信頼水準を確認
        v
設定した検証条件を満たした成果物として扱う

有限個の例を通すことと、全称的な定理を証明することは対象が異なります。また、Lean がファイルを処理できたことと、未完成の証明や独自公理へ依存していないことも別です。さらに、未レビューの AI 生成コードを高い保証水準で受け入れるなら、同じ Lean プロセスでの受理だけでなく、lean4checker や comparator のような独立した再検証まで検討対象になります。

AI が正しい証明候補へ到達するまでの試行回数と、最終成果物を何で確定するかという条件は別の問題です。

実務上の帰結は、AI 自身に「この証明は正しいか」と再質問することではありません。証明対象を先に固定し、AI を候補生成へ使い、その外側に機械判定可能な受理条件を置くことです。Lean を使う場合、その受理条件は必要な保証水準に応じて、通常の型検査、公理監査、カーネルでの再検査、外部チェッカーによる独立検証へ段階的に強められます。

参考文献

1. Anthropic, Formalizing Fermat's Last Theorem（2026-09-04）. https://www.anthropic.com/research/formalizing-fermats-last-theorem
2. Lean, Install（2026-09-08）. https://lean-lang.org/install/manual/
3. Lean, Lean 4.33.1（2026-08-21）. https://lean-lang.org/doc/reference/latest/releases/v4.33.1/
4. Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich and the Lean Community, Theorem Proving in Lean 4 — Propositions and Proofs（2026-09-08）. https://docs.lean-lang.org/theorem_proving_in_lean4/Propositions-and-Proofs/
5. Lean, Validating a Lean Proof（2026-09-08）. https://lean-lang.org/doc/reference/latest/ValidatingProofs/
6. id774, フェルマーの最終定理の形式化で、AI が生成した証明を Lean がどう検証したか（2026-09-07）. https://blog.id774.net/entry/2026/09/07/5616/