証明らしい文章から、検査できる証明へ
AIが書いた数学の証明を採用したいとき、式が並んだ説明を読んだだけで、推論の抜けまで確認できるでしょうか。説明用の仮の例として、「ある性質がすべての自然数で成立する」という主張を考えます。AIが多くの具体例を計算したり、途中の条件を省いた式変形を示したりしても、その主張を証明したことにはなりません。これは本稿の例であり、特定のモデルを実験した結果ではありません。
2026年10月9日、Terence Tao氏のブログにThomas Hales氏の寄稿が掲載されました。扱うのは、定理証明支援系Leanの信頼性とAIの関わりです。定理証明支援系は、数学の命題と証明を機械が検査できる形で記述するソフトウェアです。Hales氏は、証明の検査に加え、人による監査も必要だと述べています [1]。形式化とは、命題や定義をLeanが検査できる形で記述することです。監査では、その記述が意図した数学に対応するかを確かめます。
Leanが検査するのは、入力された形式命題に対する証明です。元の文章の意味まで自動的に保証するわけではありません。人の読解を機械の検査と組み合わせる際には、この分担が出発点になります。
AIが組み立て、kernelが検査する
形式化とは、文章で書かれた命題や推論を、Leanが扱える定義・命題・証明へ翻訳することです。人のレビューは、対象や条件が適切かを読む役割を持ちます。数値を入れて確かめる方法も、反例を探す足掛かりになります。ただし、先ほどの例で有限個の自然数を調べることと、すべての自然数での成立を示すことは別です。この比較は本稿の整理です。
Leanでは命題を「型」、証明をその型を満たす「項（term）」として表します。証明項は、論理の検査に使う式です。kernelは中核の検査器で、証明項が型理論の規則に従うかを確かめます。型理論とは、型を基礎に命題や証明を表す体系です [4]。
AIはLeanの証明スクリプトの候補を作成できます。tacticは証明の作業手順を記述し、証明状態を操作する仕組みです。elaboratorは、読み書きしやすい表面構文を中核の表現へ変換する処理です。tacticの実行はelaborationの一部であり、その結果として構成された証明項をkernelが検査します [2]。
例えばFormalProofBenchという研究では、自然言語の問題とLeanの形式命題を与え、モデルにLean checkerが受理する証明を出力させます。生成器の文章の説得力に加え、機械で判定できる合否条件を設けた例です [3]。この合否は、その評価対象や前提の範囲での判定であり、AIやLean全体の正確性を百分率で保証するものではありません。
後輩AIが証明を作り、別の処理が検査するのですね。
先輩そうだね。ただし、何を証明する命題にしたかと、どの前提を受け入れたかも確認する必要があるよ。
命題と公理が違えば、通過の意味も変わる
AIに定理文の形式化も任せる場合、Leanのコンパイル成功だけでは元の文章への忠実さは分かりません。仮定の脱落、対象範囲の変更、内容のない主張になっていないかを別に確かめます。自然言語からLeanへの形式化を評価する研究も、コンパイルと意味の一致を分けて扱っています [5]。
もう一つの確認対象は公理です。公理は、証明せずに前提として置く命題です。Leanは新しく追加した公理の無矛盾性まで検査しません。受理された証明も、依存する公理を受け入れた上での証明です。この点は公式の公理の説明で確認できます。
#print axioms theoremName は、指定した定理とその依存先が使う公理を列挙します。theoremNameは点検する定理名に置き換えます。依存ライブラリ内の未完証明も監査でき、青い完了表示だけでは分からない依存を調べられます [6]。
sorryAxが出れば、その定理か依存先に未完証明やsorryによる省略があります。名前に_nativeを含む公理は、コンパイル済みコードで計算した結果を証明に取り込む仕組みへの依存を示します。標準公理のpropext、Classical.choice、Quot.soundと、予期しない追加公理を区別して判断します [7]。公理名の表示はLeanの版でも変わるため、古いLean.trustCompilerという名前だけを探す方法にはしません。
確認を四つの段階に分ける
日常的な証明の確認と、未レビューのAI生成物や敵対的な提出物の確認では、必要な保護が異なります。Lean公式の検証手順は、証明の妥当性と命題の意味を区別し、段階ごとの前提を説明しています。
| 段階 | 確認するもの | 残る条件 |
|---|---|---|
| 通常のビルド・完了表示 | 現在の環境でkernelが証明を受理したか | 命題の意味、依存先の未完証明や追加公理を別に読む |
#print axioms | 定理と依存先が使う公理 | 許容した公理の妥当性、元の問題との対応 |
lean4checker --fresh | 保存済みの宣言・証明を同じLean kernelで再検査 | 保存ファイルの構造が正しいこと。独立実装での照合とは別 |
| comparatorと外部検査器 | 信頼側の命題との一致、許容公理、指定した検査器での受理 | 信頼側の命題・定義、隔離の安全性、全検査器に共通する実装の欠陥 |
lean4checker --freshは、ビルドで保存された.oleanファイルの宣言をkernelへ再提示する追加確認です。.oleanはLeanのビルド成果物です。状態管理や検査の迂回に関する一部の問題を検出できますが、ファイルの構造が正しいことを前提に読みます。悪意あるファイルを安全に扱うための隔離そのものではありません。
高いリスクを想定する場合、comparatorは「challenge」と提出された証明を照合します。challengeは、信頼できる側で用意する、元の問題を表す定理文です。隔離した環境で証明をビルドして書き出し、その外側で形式・命題・許容公理と、設定した外部検査器による受理を確認します。Leanのビルド時には拡張コードが実行されるため、未レビューのAI生成コードを扱う隔離にも意味があります。構築から照合までの流れは公式の検証手順に説明されています [9]。
ここでのコマンドは概念的な手順です。使用するLean版、検査器、隔離環境を確認してから、対応する公式手順に従います。2026年10月10日の公式リリース一覧ではv4.34.1がLatest、v4.35.0-rc4がPre-releaseです。4.35の資料には、新しいLake統合や--paranoidが説明されています。RCは正式リリース前の版であり、これらを全環境で提供済みの手順とは扱いません。独立したcomparatorのREADMEも、実行環境や外部検査器の条件を確認する資料になります。
検査器自体にも信頼の前提がある
2026年8月の開発者報告では、Leanのkernelとruntimeに健全性の不具合が見つかりました。runtimeはプログラムの実行を支える仕組みです。開発元は8月21日にv4.33.1を公開し、調査で見つかった問題を修正したと報告しています [8]。証明を検査するソフトウェア自身の版と修正状況も、確認対象です。
異なる実装の検査器を組み合わせると、ある実装の欠陥を別の実装で見つける助けになります。しかし、comparatorの処理、隔離環境の安全性、全検査器に共通する実装の欠陥などの前提は残ります。信頼側のchallengeが誤った問題を表していれば、命題の照合だけでは直りません [10]。
Hales氏は、Leanの型理論について理論的な理解を深める必要があるとも評価しています [1]。これは本人の見解であり、検査器の実装バグとは分けて読む必要があります。本稿の実務的な整理は、元の問題・公理・証明項・検査器と実行環境を順に確認することです。形式検証を活用するときも、人が担う命題と前提の監査を残すことが、受理結果の意味を判断する土台になります。
