2026-10-01 · chapter ヤン–ミルズと質量ギャップ付録Lean と機械検査

Lean と機械検査 — 札「Lean」が保証するのは前提から結論への矢印だけ

本書の文には五種類の札が付きます（0-01 の凡例）。Lean・紙・計算・既知・物理 です。このうち Lean の札は、最も強そうに見えて、最も誤読されやすい札です。

誤読の典型は「Lean で検査済み」を「正しいと確定した」と読むことです。Lean が確かめるのは、書かれた前提から書かれた結論が論理的に従うことです。前提が成り立つか、言明が意図した数学を言っているかは、Lean の外にあります。この付録はその境目を、実際に検査した小さな例で示します。

式で書くと、Lean の札が付いた文は次の形をしています。

札が保証するのは真ん中の矢印です。前提 $P_i$ に、未証明の仮定（例えば 10-03 の仮定 H）や、測った数値が入っていれば、結論 $Q$ も同じだけ条件つきです。本書は Lean の定理名を出すとき、前提を同じ行に書きます。

$C_P$（Poincaré 定数、第 10 部）・$m$（質量）・$\xi$（相関長）は第 10 部の量ですが、この付録ではただの実数として読めば足ります。

例。「$m \gt 0$、$C_P = 1/m^2$ かつ $C_P \le K\xi^2$ なら $1 \le K(m\xi)^2$」は、両辺に $m^2$ を掛けるだけの文で、Lean で確かめられます（§03 でこの端末が実際に検査します）。しかし $C_P \le K\xi^2$ が四次元のヤン–ミルズ理論で成り立つかどうかは、この矢印とは関係がありません。それは仮定です。

この付録と、このサイトの Lean の案内（十三ページ）との分担は次の通りです。案内は Lean そのものの入門で、導入の手順・具体的な証明の組み立て・よくある罠を扱います。この付録は、本書を読むのに要る最小限と、本書が札をどう決めているかに絞ります。個々の定理の前提と既知との対応は 10-07 に一覧があります。

Lean はプログラミング言語でもあり、証明を確かめる道具でもあります。両方を一つの仕組みで行えるのは、命題を型として、証明をその型の値（項）として扱うからです。

プログラムでは「3 は自然数の型 Nat の値だ」と書きます。Lean では同じ書き方で「p は命題 $P$ の証明だ」と書きます。

右の式は「$p$ は $P$ という型を持つ」と読み、それが「$p$ は $P$ の証明である」の意味になります。型の検査は機械的にできるので、証明の検査も機械的になります。

前提つきの命題は、関数の型になります。「$P_1$ と $P_2$ なら $Q$」の証明は、$P_1$ の証明と $P_2$ の証明を受け取って $Q$ の証明を返す関数です。

式 (1) の矢印の正体がこれです。Lean の定理の宣言で、コロンの左に並ぶ引数（(hm : 0 < m) のような括弧）が前提で、コロンの右が結論です。読むときに一番大事なのは、この括弧の列です（案内の「仮定の一覧を作る」）。

例。この端末で検査した最小の例は次の一行です。

theorem pos_nat (n : Nat) (h : 0 < n) : 0 < n := h

前提 h がそのまま結論の証明になっています。中身の無い定理ですが、「前提を受け取って結論を返す関数」という形がよく見えます。

もう一つの柱はカーネルです。人が書く証明は、tactic（証明の一手を指示する命令。§03）を並べた台本で、それを Lean が式 (2) の形の項に展開します。最後にその項を、小さく保たれた検査部であるカーネルが型検査します。tactic に誤りがあっても、カーネルが通さない項は定理になりません。信じる対象をカーネル一つに絞ることが、機械検査の信頼の出所です（案内の「kernel と tactic」・検証の仕組み）。

寄り道：命題と型の対応の呼び名

Lean で証明を書くとき、画面には常に「いま示すべきこと」が出ています。これをゴールと呼びます。ゴールは記号 $\vdash$ の右に書かれ、その上に使ってよい仮定が並びます。tactic を一つ打つたびに、仮定かゴールが書き換わり、ゴールが無くなれば証明は終わりです。

例として §01 の文を Lean で書いたものを使います。前提は三つ（変数の型を除く）です。10-07 の hup_is_gap_positivity と同じ言明で、変数の名前だけが違います。

紙の上では「$C_P$ を代入し、$m^2 \gt 0$ を両辺に掛け、整理する」の三行です。Lean では四手になり、二手目の have は $m^2$ を掛けるための下ごしらえです。対応は、代入が段 1、掛けるのが段 2・3、整理が段 4 です。Lean では各手が何を書き換えたかが機械的に記録されます。図 1 の数値（ゴールの文面）は、この端末の Lean 4.33.1 が証明の途中で出した状態を、そのまま写したものです。

計算この図の数値はこの端末で計算した（Lean 4.33.1 で trace_state を各手の後に挟んで検査し、出力をそのまま写した。図では trace_state の行を省く。段 4 の「No goals」は出力の写しではなく、エラー無しで終わったことで確かめた）。狭い画面では表 1 で同じ内容を読める。

表 1 は図 1 と同じ内容です。

読み方。段 3 で hH はゴールとほぼ同じ形になり、違いは積の並べ方だけです。最後の ring がその並べ替えを恒等式として確かめます。紙の三行が Lean の四手に、下ごしらえの一手を足しただけで対応していることが分かります。Lean での手の選び方の詳しい例は 案内の「証明の骨」にあります。

この例で Lean が確かめたのは代数だけです。$C_P$ は Lean の中では名前の付いたただの実数で、それが Poincaré 定数であることは検査されていません。この点は §06 で本書の定理全体について見ます。

証明の途中を飛ばす方法が Lean には二つ用意されています。一つは sorry で、「ここは後で埋める」という印です。もう一つは公理で、証明なしに真と宣言する文です。どちらも書けば定理は通ります。だから「通った」ことだけでは、穴が無いことは分かりません。

穴を見つける道具が #print axioms です。定理の名前を渡すと、その定理が（言明と証明をたどって）最終的にどの公理に依存しているかを並べます。sorry は内部で sorryAx という公理に置き換えられるので、ここに現れます。Lean の参照マニュアルは、検査の手順として「標準の三つの公理 propext・Classical.choice・Quot.sound だけが出ることを確かめよ」と書いています。本書の Lean の札の条件は、この形です。

三つの意味は、順に「同値な命題は等しい」「存在の証明から元を一つ取り出せる（選択公理）」「同値な元は商の中で等しい」です。商とは、同値関係で同じとみなす元をひとまとめにした集合（同値類の集合）のことで、例えば整数を 7 で割った余りの類がそうです。数学の普段の推論（排中律を含む）は、この三つで足ります。詳しくは 10-07 の寄り道と 案内の「公理」に譲ります。

この端末で、七つの小さなファイルを検査しました。表 2 がその結果です。

秒は import Mathlib の読み込みを含む壁時計の時間（4 コアの機械・nice 19）。Mathlib を読む行は、読み込みだけで約 5 秒かかる。値は results.json の一回分で、実行ごとに 1 割ほど揺れる（終了コード・警告・公理の行は再実行でも同じ）。

読み方は三つです。第一に、sorry を含むファイルも終了コード 0 で通ります。出るのは警告だけです。検査の記録で「エラーなし」とだけ書かれていたら、sorry が無いことは保証されていません。第二に、native_decide は、その呼び出しのためだけの専用の公理を一つ作ります。Lean の参照マニュアルは、各公理が何を主張したかを個別に監査できるようにするためだと説明しています。版による違いがあり、4.28.0 以前は、どの呼び出しも共通の公理 Lean.ofReduceBool（その奥に Lean.trustCompiler）に依存する形で出ました。4.29.0 から、呼び出しごとの専用の公理（表 2 の …ax_1_1 の形）に変わりました。公理の名前は版で変わるので、本書は「標準の三つの部分集合か」で判定します。第三に、偽の文は decide では通りません。

寄り道：実数を使うと三つの公理が出る

穴が無く、公理が標準の三つだけでも、まだ確かめていないことがあります。それは言明が言いたいことを言っているかです。Lean の参照マニュアルは、検査の手順の冒頭で「定理に正しい証明があるか」という問いと「定理の言明が何を意味するか」という問いを区別することが重要だ、と書いています。後者は機械では確かめられません。

このサイトの 案内の第 8 ページは、この隙間を四つの型に分けています（表 3）。

②と③は、表 2 の最後の二行で実際に起きています。mass_gap_positive は質量ギャップという名前を持ちますが、言明は「正の数は正」です。名前は Lean にとってただの文字列で、内容を何も保証しません。本書が定理名を出すとき言明と前提を同じ行に書くのは、このためです。

③の例は次の文です。

前提が矛盾しているので、結論は何でもよく、Lean は linarith（線形の不等式を組み合わせる自動の手）一つで通します。前提が多い定理ほど、この危険は見えにくくなります。前提を全部満たす例（自由場など、答えが分かっている場合）を一つ置くのが確かめ方です。本書の第 10 部では、前提を全部満たす例の役は自由場での検算が担います（10-10）。陰性対照（10-07 の種別 N）は逆向きで、仮定を一つ外すと結論が崩れることを示し、仮定が飾りでないことを確かめます。

④は本書で最も重要です。仮定 H のような未証明の仮定から結論を出す定理は、仮定の側に中身があり、定理はその仮定を一歩も証明しません（10-07 の種別 C）。

Lean の定理は型の付いた対象についての文です。だから定理の引数の型を見ると、その文が実際に何について語っているかが分かります。10-07 の §02 は、本書が結論として引く四十六の定理を、言明に現れる型で五つの層に分けています。ちょうど半分の 23 個は実数の不等式か恒等式で、格子のゲージ場を型として持つ定理は 5-11 の 3 個です。

このことを式で書くと、本書の Lean の札の付いた文は二つの部分から成ります。

§03 の例で $C_P$ が名前の付いた実数だったのと同じく、本書の多くの定理で $C_P$・$\xi$・$m$ は実数の変数です。それを物理の量として読むのは本文で、その読みが正しいかは Lean の外にあります。読みの約束（$\beta$ の定義・tr の規格化・格子の計量）は 10-07 の §08 と A-01 記号表にあります。

なぜ Wilson 測度そのものについての定理が無いのか。理由の一つは在庫です。Lean の数学の標準ライブラリ Mathlib を、この端末にある版（版は §08 の表 7）のソースで語を数えると、表 4 のようになりました。

群の上の一様な測度（ハール測度）の基礎はありますが、格子ゲージ理論の語は現れません。語が無いことは定義が無いことの証明ではありませんが、少なくとも名前の付いた道具立てとしては、それを使う側が一から作ることになります。案内の 「mathlib に在庫が無い数学」は、こうした厳しさの出所を三つ（量・述べ方・在庫）に分けています。連続極限や四次元の場の理論の構成は、その先にあります（6-10）。

例。このサイトの論文（5-11）は、格子のゲージ場を型に持つ数少ない例です。そこでも Lean の札は段ごとに分かれ、作用からある下界までの鎖は Lean、その下界から格子の質量ギャップへの段は 紙（しかも概略）です（0-01）。

本書は札を文ごとに付けます。章ごとでも論文ごとでもありません。一本の論文の中でも、段によって札が違うからです（§06 の例）。どの札を付けるかは、文が受けている保証の種類で決まります。図 2 はその決め方を、上から順に問う形にしたものです。

問いの順には理由があります。Lean の札は前提から結論への矢印を保証し、既知の札は文献の証明を、紙の札は本書の側の証明を、計算の札は有限の範囲の確認を、物理の札は物理の水準での受け入れを指します。強い保証を先に問い、当てはまった最初の札を付けます。どれにも当たらない文は札を付けず、「仮定」か「問い」として書きます（10-13 の問いには札を付けません）。

文が鎖になっているときの読み方は次の通りです。

一つの段だけが 紙 なら、ほかの段が全部 Lean でも、結論は紙の水準です。始点 $A_0$ が仮定なら、結論も仮定つきです。式 (1) の前提 $P_i$ が、この始点に当たります。

この図は 0-01 の札の約束を問いの形にしたもの。数値は含まない。

読み方。表の一行目の Lean の前提 $C_P \le K\xi^2$ は、最後の行の仮定の帯の文 $\text{H}_{\rm band}$ の上の半分 H↑ です（10-03 の名前の約束）。一行目では前提として、最後の行では仮定の主張として。札が違うのは、文の中での役割が違うからです。

Lean の札は、読者が自分の機械で検査し直せることを前提にしています。Lean の参照マニュアルは、検査を四段の階段として説明しています（表 6）。下の段ほど手軽で、上の段ほど疑う範囲が広がります。

段 4 はマニュアル自身が、証明の市場・高額の賞金つきの競技・意図の揃っていない AI のような、危険の高い場面のためのものと位置づけています。マニュアルは段 1 について、sorry を含む依存先があっても検査の印は付く、と注意しています。表 2 の gap_from_bound' が終了コード 0 だったのと同じ事情で、だから段 2 が要ります。本書の Lean の札は、少なくとも段 2 までを済ませた定理に付けています。

具体的な手順は次の形です。導入と版の合わせ方は 案内の「入れる」と 「配布されている証明を手元で検査する」にあります。

lake build                      # 段 1：プロジェクト全体を検査
lake env lean File.lean         # 一つのファイルだけを検査
#print axioms gap_from_bound    # 段 2：ファイルの中に書く

このサイトの Lean の記録（定理の一覧と検査の記録）は Lean の記録にあります。同じ証明でも、Lean と Mathlib の版が違うと補題の名前が変わり、通らなくなることがあります。そのため本書は検査に使った版を記録します。

最後に、Lean の札の付いた文を受け取ったときに問うことを七つにまとめます。案内の「言明を読む手順」のチェックリストを、本書の読み方に合わせたものです。

1. 定理名が添えてあり、自分の手で検査し直せるか（段 1）。
2. sorry が無く、公理が式 (5) の三つの中に収まっているか（段 2）。
3. 言明に現れる定義を全部たどったか（§05 の①）。
4. 名前ではなく言明を読んだか（§05 の②）。
5. 前提を全部満たす例が一つ示されているか（§05 の③）。
6. 前提の一覧と、各前提の札が書かれているか（§05 の④・式 (8)）。
7. 実数の変数を物理の量として読む部分が、本文のどこで宣言されているか（§06・式 (7)）。

七つ目が本書に固有の問いです。本書の Lean の定理の多くは、ここで初めて質量ギャップの問題とつながり、そのつながりは Lean の札の外にあります。

この章が言えている範囲

出典と再現

次に読む章：A-05 この本の作り方 — 札を付ける前に、文と数値をどう確かめたか。

← A-03 文献案内目次A-05 この本の作り方 →