# Lean による数学の形式化：型クラス・商・Rikai の定理と信頼の境界 > Lean 4 で群の公理系を型クラスの階層として定義して基本性質を証明し、商で整数を構成し、カントールの定理を形式化する。Mathlib の実数と測度論、バナッハの不動点定理と有限次元ハーン–バナッハの定理の形式化を Rikai の証明と対応させ、形式化が保証しないものを整理する。 > https://rikai.mugen-giken.com/mathematics/logic-and-type-theory/formalizing-in-lean ## 0. この記事の要点 数学の証明を、人間が読むだけでなく、計算機に最後まで検査させるにはどうすればよいでしょうか。この記事では、群の基本性質のような身近な題材を、証明支援系 Lean の言葉に書き直す手順を追います。読み終えると、Lean で群や整数がどう定義されるか、紙の証明がコードのどの部分に対応するか、そして「計算機が検査した」ことが何を保証し、何を保証しないかが分かります。 - **型クラス**は「構造をもつ型」を表す Lean の仕組みです。群の公理を `class` で書き、`extends` で「群はモノイドである」という階層を作ると、モノイドについて証明した定理がそのまま群に使えます。[群論入門](/mathematics/algebra/groups) の基本性質を、この方法で形式化します。 - **商**（`Quot`。同値な元を同じものとみなしてできる型）を使うと、[公理的集合論 ZFC](/mathematics/logic-and-type-theory/axiomatic-set-theory) で行った「対の同値類としての整数」の構成を、そのまま型として書けます。Mathlib の実数も、有理数のコーシー列の商として定義されています。 - Rikai の定理のうち、カントールの定理は標準ライブラリだけで完全に形式化して検査できます。バナッハの不動点定理とハーン–バナッハの定理は Mathlib に形式化があり、Rikai の証明の各段階と Mathlib の概念を対応させます。有限次元のハーン–バナッハの定理は、ここで選択公理を使わない証明を与えます（）。 - 形式化が保証するのは「書かれた主張が、使われた公理から導かれる」ことだけです。`5 / 0 = 0` のような規約、主張の書き違い、公理の使用は、人間が確かめる必要があります。これが**形式化の信頼境界**です。 - この記事のコードのうち、標準ライブラリだけのものは Lean 4（4.34 系）で動作を確認しました。Mathlib に依存する部分はコードとしては載せず、名前だけを挙げます（Mathlib の名前は版によって変わります）。 ## 1. 動機：Rikai の閉包と形式証明 Rikai では、定理の証明で使う事実を、記事内で証明するか既出の定理として参照するかのどちらかにしてきました。参照をたどると、数学の命題は ZFC の公理に行き着きます。これは人間が読む証明の網の目で、各リンクの正しさは書き手と監査者の目に頼っています。 形式証明は、同じ網の目を計算機が検査できる形で作るものです。[証明支援系 Lean の仕組み](/mathematics/logic-and-type-theory/lean-kernel) で見たように、Lean で受理された証明は小さなカーネルが一歩ずつ検査した項であり、依存する公理も `#print axioms` で正確に列挙されます。 この章では、実際に形式化するときに何が起こるかを、三つの観点から見ます。 1. **定義をどう書くか**。「群」「整数」「実数」を、型理論の中でどう表すか（§2、§3）。 2. **定理をどう証明するか**。Rikai の記事の証明が、形式証明ではどのような部品に分かれるか（§4）。 3. **何を信じているか**。形式化された定理が、人間の言葉で述べた定理と本当に同じものか（§5）。 ## 2. 型クラスと代数構造の階層 ### 2.1. 群を型クラスで定義する [群論入門](/mathematics/algebra/groups) の群の定義（）は「集合と演算の組で、結合法則・単位元・逆元の公理を満たすもの」でした。Lean では、これを型 $G$ に付随する**構造**として書きます。 ```lean class MyMonoid (M : Type) extends Mul M, One M where mul_assoc : ∀ a b c : M, a * b * c = a * (b * c) one_mul : ∀ a : M, 1 * a = a mul_one : ∀ a : M, a * 1 = a class MyGroup (G : Type) extends MyMonoid G, Inv G where inv_mul : ∀ a : G, a⁻¹ * a = 1 ``` `class` は、フィールド（演算と公理の証明）をまとめた構造体の宣言です。`extends Mul M, One M` は「`*` と `1` の記法をもつ」こと、`extends MyMonoid G, Inv G` は「群はモノイドであって、さらに逆元をもつ」ことを表します。群の公理として左逆元 `inv_mul` だけを要求しているのは、右逆元が定理として導けるからです（下の `mul_inv`）。 型クラスの要点は、`[MyGroup G]` と書いた引数（**インスタンス引数**）を、Lean が型から自動で探して埋めることです。定理を「任意の群 $G$ について」の形で書いておけば、具体的な群に使うときに構造を明示的に渡す必要がありません。たとえば §2.3 で整数の加法群を登録しておくと、その型に定理を使うときに、Lean が登録済みの構造を探して渡してくれます。 ### 2.2. 群の基本性質の形式化 の単位元の一意性・消約律・逆元の一意性・$(ab)^{-1}=b^{-1}a^{-1}$ を形式化します。 ```lean namespace MyMonoid variable {M : Type} [MyMonoid M] theorem one_unique (e : M) (h : ∀ a : M, e * a = a) : e = 1 := by have h1 := h 1 rw [mul_one] at h1 exact h1 end MyMonoid namespace MyGroup open MyMonoid variable {G : Type} [MyGroup G] theorem cancel_left (a x y : G) (h : a * x = a * y) : x = y := by calc x = 1 * x := (one_mul x).symm _ = a⁻¹ * a * x := by rw [inv_mul] _ = a⁻¹ * (a * x) := mul_assoc _ _ _ _ = a⁻¹ * (a * y) := by rw [h] _ = a⁻¹ * a * y := (mul_assoc _ _ _).symm _ = 1 * y := by rw [inv_mul] _ = y := one_mul y theorem mul_inv (a : G) : a * a⁻¹ = 1 := by apply cancel_left a⁻¹ rw [← mul_assoc, inv_mul, one_mul, mul_one] theorem inv_unique (a b : G) (h : b * a = 1) : b = a⁻¹ := by calc b = b * 1 := (mul_one b).symm _ = b * (a * a⁻¹) := by rw [mul_inv] _ = b * a * a⁻¹ := (mul_assoc b a a⁻¹).symm _ = 1 * a⁻¹ := by rw [h] _ = a⁻¹ := one_mul a⁻¹ theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by apply Eq.symm apply inv_unique rw [mul_assoc, ← mul_assoc a⁻¹, inv_mul, one_mul, inv_mul] end MyGroup ``` 読み方を補います。`variable {G : Type} [MyGroup G]` は「以下の定理はすべて、任意の型 $G$ とその上の群構造について述べる」という宣言です。`calc` は等式の連鎖で、紙の上の計算 $x=1x=(a^{-1}a)x=a^{-1}(ax)=\cdots$ をそのまま書いたものです。各段の `:=` の後ろが、その一段の根拠（公理の適用か、`rw` による書き換え）です。`rw [← mul_assoc]` は結合法則を右辺から左辺の向きに使う書き換えです。 `MyGroup` の中で `MyMonoid` の公理 `one_mul` や `mul_assoc` がそのまま使えていることに注意してください。`extends` によって、群構造から自動的にモノイド構造が取り出されています。`one_unique` は群でも使えます。 ### 2.3. 具体的な群とインスタンス 整数の加法群を、この型クラスのインスタンスとして登録してみます（`Int` の `*` と衝突しないように、新しい型 `AddInt` で包みます）。 ```lean structure AddInt where val : Int instance : MyGroup AddInt where mul a b := ⟨a.val + b.val⟩ one := ⟨0⟩ inv a := ⟨-a.val⟩ mul_assoc a b c := by show AddInt.mk (a.val + b.val + c.val) = AddInt.mk (a.val + (b.val + c.val)) rw [Int.add_assoc] one_mul a := by show AddInt.mk (0 + a.val) = a rw [Int.zero_add] mul_one a := by show AddInt.mk (a.val + 0) = a rw [Int.add_zero] inv_mul a := by show AddInt.mk (-a.val + a.val) = AddInt.mk 0 rw [Int.add_left_neg] #eval ((⟨3⟩ : AddInt) * ⟨4⟩).val -- 7 example (a b : AddInt) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := MyGroup.mul_inv_rev a b ``` インスタンスを作るときに、各公理の証明を義務として課されます（`show` で目標を定義に沿って書き直し、整数の性質で閉じています）。一度登録すれば、群について証明したすべての定理が `AddInt` に使えます。最後の行では、一般の群の定理 `mul_inv_rev` を `AddInt` に適用しています。 Mathlib はこの方法で、半群・モノイド・群・可換群・環・体・加群・ノルム空間・内積空間などの数百のクラスを階層にしています（`Monoid`、`Group`、`CommRing`、`Field`、`NormedSpace` などの名前で、版によって整理が変わります）。数学でいう「体は環である」「ノルム空間は距離空間である」が、すべて型クラスの継承として表されます。複数の道筋で同じ構造が得られるとき（たとえば実数の距離が「ノルムから」と「順序から」の二通りで得られるとき）、それらが**定義的に**一致するように設計する必要があり、これは形式化特有の難しさです（「ダイヤモンド問題」と呼ばれます）。 ## 3. 商による構成：整数から実数へ ### 3.1. 対の同値類としての整数 [公理的集合論 ZFC](/mathematics/logic-and-type-theory/axiomatic-set-theory) では、整数を $\omega\times\omega$ の対 $(a,b)$（「$a-b$」のつもり）の[同値類](/mathematics/foundations/equivalence-relations#def-class)として作りました（）。Lean では商型 `Quot` で同じことができます。 ```lean def IntRel (a b : Nat × Nat) : Prop := a.1 + b.2 = b.1 + a.2 def MyInt : Type := Quot IntRel def MyInt.mk (m n : Nat) : MyInt := Quot.mk IntRel (m, n) def MyInt.neg : MyInt → MyInt := Quot.lift (fun p => Quot.mk IntRel (p.2, p.1)) (by intro a b h apply Quot.sound show a.2 + b.1 = b.2 + a.1 unfold IntRel at h omega) theorem MyInt.mk_succ (m n : Nat) : MyInt.mk (m + 1) (n + 1) = MyInt.mk m n := by apply Quot.sound show m + 1 + n = m + (n + 1) omega theorem MyInt.neg_neg (x : MyInt) : x.neg.neg = x := by induction x using Quot.ind with | mk p => rfl ``` 上のコードの読み方を先に述べます。`Quot IntRel` は、自然数の対の型を関係 `IntRel` で割った商の型で、`Quot.mk IntRel (m, n)` が対 $(m,n)$ の属する類を表します。`Quot.sound` は「関係で結ばれた 2 つの対は、商の中で等しい」と述べる規則です。商の元は代表元の選び方に依らない形でしか扱えないので、商の上の関数は次のように定義します。 `Quot.lift` で商の上の関数を定義するときには、代表元によらないことの証明を必ず渡さなければなりません。紙の上では「well-defined であることは容易に確かめられる」と書き流しがちな部分が、形式化では証明義務として明示されます。 $(a_1,a_2)\sim(b_1,b_2)$、すなわち $a_1+b_2=b_1+a_2$ ならば、$(a_2,a_1)\sim(b_2,b_1)$、すなわち $a_2+b_1=b_2+a_1$。 自然数の加法の可換性から、仮定の等式の両辺を入れ替えて書き直すと $b_1+a_2=a_1+b_2$、さらに各辺の和の順序を入れ替えて $a_2+b_1=b_2+a_1$。 コードの `by intro a b h; …; omega` がこの証明です。`omega` は整数・自然数の線形算術の決定手続きで、この程度の等式変形を自動で行います。`neg_neg` は、`Quot.ind`（商の元についての帰納法）で代表元 `p` の場合に帰着させると、`(p.2, p.1)` を 2 回入れ替えたものが `p` に定義的に等しい（構造体 η）ので `rfl` で閉じます。なお `#print axioms MyInt.neg_neg` は `propext` と `Quot.sound` を表示します。`Quot.sound` は商を使ったため、`propext` は `omega` が内部で使うためです。 ### 3.2. Mathlib の実数 Mathlib の実数 `Real`（記号 `ℝ`）は、有理数のコーシー列の同値類として定義されています。本稿執筆時点では、`CauSeq.Completion.Cauchy (abs : ℚ → ℚ)`（絶対値に関する有理数の[コーシー列](/mathematics/real-analysis/completeness-and-cauchy#def-cauchy)を「差が 0 に収束する」で割った商）を包む構造体です。その上に四則・順序を定義し、**上限性質**（`sSup` が上に有界な空でない集合の最小上界であること）や完備性を定理として証明しています。 これは [数とは何か](/mathematics/foundations/what-is-a-number) で紹介したコーシー列による構成（）そのものです。[公理的集合論 ZFC](/mathematics/logic-and-type-theory/axiomatic-set-theory) ではデデキント切断を使いましたが、上限性質をもつ順序体はすべて同型なので（）、どちらの構成から出発しても同じ解析学が展開されます。形式化では、構成の詳細を一度証明した後は、`ℝ` を「完備な[順序体](/mathematics/foundations/what-is-a-number#def-ordered-field)」としてだけ扱い、構成に依存しない補題だけを使うのが普通です。 測度論も同じ方針で形式化されています。Mathlib の測度 `MeasureTheory.Measure` は外測度から Carathéodory の方法で作られ（[測度空間と Carathéodory の拡張定理](/mathematics/real-analysis/abstract-measures) と同じ道筋）、`ℝ` 上のルベーグ測度 `MeasureTheory.volume`、非負関数の積分 `MeasureTheory.lintegral`、ボホナー積分 `MeasureTheory.integral` などが定義されています（名前は本稿執筆時のもの）。 ## 4. Rikai の定理を形式化する ### 4.1. カントールの定理（標準ライブラリだけで完結） [濃度と無限](/mathematics/foundations/cardinality-and-infinity) のカントールの定理（）は、集合 $A$ から冪集合への全射が存在しないことでした。$A$ の部分集合を述語 $A\to\mathsf{Prop}$ で表すと、次のようになります。 ```lean theorem cantor {α : Type} (f : α → (α → Prop)) : ¬ Function.Surjective f := by intro hf obtain ⟨a, ha⟩ := hf (fun x => ¬ f x x) have h : f a a = ¬ f a a := congrFun ha a have hn : ¬ f a a := fun hfa => (Eq.mp h hfa) hfa exact hn (Eq.mpr h hn) #print axioms cantor -- 'cantor' does not depend on any axioms ``` 紙の証明との対応は一対一です。対角集合 $D=\{x\mid x\notin f(x)\}$ が `fun x => ¬ f x x`、全射性から $f(a)=D$ となる $a$ をとるのが `obtain`、「$a\in f(a)\iff a\notin f(a)$」が `h`（`congrFun` は関数の等式を点 $a$ で評価する合同）です。最後の 2 行は、$a\in f(a)$ と仮定すると $a\notin f(a)$ が出て矛盾する、だから $a\notin f(a)$、すると $a\in f(a)$ になって矛盾、という二段階の議論です。`#print axioms` が示すとおり、この証明は公理を一つも使わない純粋な λ 項で、排中律すら要りません。 ### 4.2. バナッハの不動点定理（Mathlib との対応） [距離空間](/mathematics/real-analysis/metric-spaces) の縮小写像の原理（）は Mathlib に形式化されています。本稿執筆時点の Mathlib では、定数 $K$ の縮小写像であることを `ContractingWith K f`（$K<1$ かつ $f$ が $K$-リプシッツ）で表し、完備距離空間（`CompleteSpace`）上で不動点 `ContractingWith.fixedPoint`、それが不動点であること `ContractingWith.fixedPoint_isFixedPt`、一意性 `ContractingWith.fixedPoint_unique` を提供しています（Mathlib への依存が必要で、この記事の環境では実行していません。名前は版によって変わりえます）。 Rikai の証明の各段階が、形式化ではどの部品になるかを対応させると次のようになります。 | Rikai の証明の段階 | 形式化での部品 | |---|---| | $x_{n+1}=T(x_n)$ と反復する | 反復 `f^[n] x`（`Nat.iterate`） | | $d(x_{n+1},x_n)\le k^nd(x_1,x_0)$ | 帰納法とリプシッツ性 | | 等比級数で $(x_n)$ がコーシー列 | 等比級数の和と、コーシー列の判定補題 | | 完備性で極限 $x^{*}$ が存在 | `CompleteSpace` の定義（コーシー列の収束） | | 連続性で $T(x^{*})=x^{*}$ | 極限と連続写像の交換 | | $d(x^{*},y^{*})\le k\,d(x^{*},y^{*})$ から一意性 | 実数の不等式 | 形式化の際に紙の証明と最も違うのは、「極限」「コーシー列」が Mathlib では[フィルター](/mathematics/topology/products-quotients-tychonoff#def-filter)という一般的な枠組みで定義されていることです。ε-N 論法の命題は、フィルターの言葉から取り出す補題を経由して使います。証明の骨組みは同じでも、どの一般性で定義するかという設計が、形式化の手間を大きく左右します。 ### 4.3. 有限次元のハーン–バナッハの定理 [Banach 空間の基本定理](/mathematics/functional-analysis/banach-spaces) のハーン–バナッハの拡張定理（）は、一般の場合には Zorn の補題を使いました。有限次元では[選択公理](/mathematics/foundations/axiom-of-choice-zorn#ax-choice)は要りません。ここで完全な証明を与えます。ねらいは次のとおりです。まず補題で、定義域を 1 次元だけ広げる 1 段の拡張を作ります。そこでは拡張の値 $c$ の候補が実数の上限と下限の間の幅として現れ、上限を選ぶ規則を決めておけば、選択の余地がなくなります。有限次元では、この 1 段を有限回繰り返せば全体に届きます。$p$ は劣線形汎関数（）とします。 $X$ を実ベクトル空間、$p$ を $X$ 上の劣線形汎関数、$M$ を部分空間、$f:M\to\mathbb{R}$ を $M$ 上で $f\le p$ を満たす線形汎関数、$x_0\in X\setminus M$ とする。このとき $M_1=M+\mathbb{R}x_0$ 上の線形汎関数 $F_1$ で、$F_1|_M=f$ かつ $M_1$ 上で $F_1\le p$ を満たすものが存在する。 $m,m'\in M$ について、$f$ の線形性、$M$ 上の $f\le p$、$p$ の劣加法性から $$ f(m)+f(m')=f(m+m')\le p(m+m')=p\bigl((m+x_0)+(m'-x_0)\bigr)\le p(m+x_0)+p(m'-x_0). $$ よって $f(m')-p(m'-x_0)\le p(m+x_0)-f(m)$。左辺の集合 $\{f(m')-p(m'-x_0)\mid m'\in M\}$ は空でなく（$0\in M$）、右辺の任意の値で上から抑えられるので、実数の上限性質（）により上限 $a$ が存在して、すべての $m$ について $a\le b_m:=p(m+x_0)-f(m)$。$c=a$ とおく。 $x_0\notin M$ なので、$M_1$ の元は $m+tx_0$（$m\in M$、$t\in\mathbb{R}$）とただ一通りに表される（$m+tx_0=m'+t'x_0$ で $t\ne t'$ なら $x_0=(m'-m)/(t-t')\in M$ となり矛盾）。$F_1(m+tx_0):=f(m)+tc$ は well-defined で線形、$M$ 上で $f$ に一致する。$F_1\le p$ を示す。$t=0$ は仮定。$t>0$ なら、$c\le b_{m/t}$ と $p$ の正斉次性から $$ f(m)+tc\le f(m)+t\bigl(p(m/t+x_0)-f(m/t)\bigr)=p(m+tx_0). $$ $t=-s<0$ なら、$c\ge f(m/s)-p(m/s-x_0)$ から $$ f(m)-sc\le f(m)-s\bigl(f(m/s)-p(m/s-x_0)\bigr)=p(m-sx_0). $$ $X$ を有限次元の実ベクトル空間とし、$p,M,f$ を と同じとする。このとき $X$ 上の線形汎関数 $F$ で、$F|_M=f$ かつ $X$ 上で $F\le p$ を満たすものが存在する。この証明は選択公理を使わない。 $X$ は有限個のベクトル $v_1,\ldots,v_n$ で張られている。$M_0=M$、$f_0=f$ とし、$i=1,\ldots,n$ について順に、$v_i\in M_{i-1}$ なら $M_i=M_{i-1}$、$f_i=f_{i-1}$、$v_i\notin M_{i-1}$ なら を $x_0=v_i$ に使って $M_i=M_{i-1}+\mathbb{R}v_i$ 上の拡張 $f_i\le p$ を作る。各段で $M_i\supseteq M_{i-1}$、$v_i\in M_i$ なので $M_n$ はすべての $v_i$ を含み、$M_n=X$。$F=f_n$ が求める汎関数である。手順は $n$ 段で終わり、各段の選択（ の $c$）は上限という一意に定まる値なので、選択公理は使っていない。 一般の場合（）は、この 1 段の拡張を Zorn の補題で「超限回」繰り返すことに相当します。Mathlib には一般の場合が形式化されており（本稿執筆時点では `exists_extension_of_le_sublinear` などの名前。未実行）、そちらは Zorn の補題を使うので `Classical.choice` に依存します。Lean の数学ライブラリでは、有限次元の場合も一般の定理の特殊化として得るのが普通で、「選択公理を使わない証明がある」という情報は `#print axioms` には現れません。どの公理が**本当に必要か**は、形式化された証明を見るだけでは分からないこともある、という教訓です。 ## 5. 形式化の信頼境界 ### 5.1. カーネルが保証すること、しないこと [証明支援系 Lean の仕組み](/mathematics/logic-and-type-theory/lean-kernel) の de Bruijn 基準の節（）で、信頼の境界を表にしました。形式化の現場で最も問題になるのは、その表の「定義と主張が意図どおりに書かれていること」です。カーネルが保証するのは > 書かれた主張（型）が、使われた公理と、書かれた定義から導かれる。 ということだけで、その主張が人間の意図した数学の命題と同じかどうかは、まったく保証しません。
人間が確かめる：定義と主張が意図した数学と一致しているか 使った公理（#print axioms で列挙。sorryAx がないこと） カーネルが検査する 項が主張の型をもつ（定義的同値を含む）
### 5.2. 規約による「ゴミ値」 型理論の関数は全域的でなければならないので、数学では「定義しない」値にも何かを割り当てます。Lean の標準ライブラリでは次のとおりです。 ```lean #eval (5 : Nat) / 0 -- 0 #eval (2 : Nat) - 3 -- 0（自然数の引き算は 0 で打ち切る） #eval (1 : Rat) / 0 -- 0 theorem not_div_cancel : ¬ ∀ a b : Nat, a / b * b = a := by intro h exact absurd (h 1 0) (by decide) ``` $x/0=0$ という規約は、[数とは何か](/mathematics/foundations/what-is-a-number) で論じたゼロ除算の問題（）とは矛盾しません。そこで示したのは「$0$ で割った結果に、乗法の逆元としての性質を要求すると壊れる」ことで、Lean の `/` は $b\ne0$ のときだけ逆元の性質をもつ、別の全域関数だからです。$x/0=0$ を定理の中で使っても矛盾は起きませんが、**主張の読み違い**の原因になります。たとえば「$a/b\cdot b=a$」を仮定 $b\ne0$ なしで形式化すると、上のとおり偽の主張になります（証明できないので、誤りは発見されます）。逆に、仮定の付け忘れで主張が**弱く**なる誤り（たとえば $\frac{1}{x}$ についての不等式が $x=0$ で自明に成り立ってしまう）は、証明が通ってしまうので発見されにくいのです。 ### 5.3. 主張の忠実さを確かめる方法 形式化の実践では、主張の忠実さを次のような方法で確かめます。 - **定義の健全性検査**：定義した概念について、既知の例と反例で期待どおりの結果になるかを証明してみる（「素数」を定義したら、$2$ が素数で $4$ が素数でないことを証明する）。 - **主張の否定の確認**：仮定を一つ外した主張の反例を形式化して、仮定が本当に効いていることを確かめる。 - **ブループリント**：形式化の前に、人間の言葉の証明を補題に分解した文書を作り、補題ごとに形式化の主張と人間の主張を並べて査読する。Liquid Tensor Experiment で使われ、大規模な形式化の標準的な方法になりました。 - **公理の確認**：最終的な定理に `#print axioms` を実行し、`sorryAx` や想定外の公理が混じっていないことを確かめる。 Rikai の記事は、まさにこの「ブループリント」に近い位置にあります。各定理の証明が、既出の定理への参照と記事内の補題に分解されていれば、それを形式化の作業単位にそのまま使えます。Rikai の閉包（ZFC までさかのぼれること）と、形式証明の閉包（カーネルと三つの公理までさかのぼれること）は、同じ考え方を人間の言葉と機械の言葉で実現したものだと言えます。 ## 6. 演習 §2.2 の `MyGroup` について、$(a^{-1})^{-1}=a$ を Lean で証明せよ。（ヒント：`inv_unique` と `mul_inv`。） $a\cdot a^{-1}=1$ は「$a$ が $a^{-1}$ の左逆元である」ことを意味するので、逆元の一意性から $a=(a^{-1})^{-1}$。 ```lean namespace MyGroup open MyMonoid variable {G : Type} [MyGroup G] theorem inv_inv (a : G) : (a⁻¹)⁻¹ = a := by apply Eq.symm apply inv_unique exact mul_inv a end MyGroup ``` `apply inv_unique` で目標 `a = a⁻¹⁻¹` が `a * a⁻¹ = 1` に変わり、`mul_inv a` がちょうどその証明です。§2.2 のコードに続けて書けば、そのまま通ります。 §3.1 の `MyInt` に加法 $[(a_1,a_2)]+[(b_1,b_2)]=[(a_1+b_1,\,a_2+b_2)]$ を定義するとき、`Quot.lift` に渡す必要のある証明義務を数式で書き、証明せよ。 2 変数なので、各変数について代表元によらないことを示す。第 1 変数については、$(a_1,a_2)\sim(a'_1,a'_2)$（$a_1+a'_2=a'_1+a_2$）ならば $(a_1+b_1,a_2+b_2)\sim(a'_1+b_1,a'_2+b_2)$、すなわち $(a_1+b_1)+(a'_2+b_2)=(a'_1+b_1)+(a_2+b_2)$。左辺は $(a_1+a'_2)+(b_1+b_2)$、右辺は $(a'_1+a_2)+(b_1+b_2)$ と並べ替えられ、仮定から等しい。第 2 変数も同様。Lean では、`Quot.lift` を 2 回入れ子にするか、2 変数版の補助関数を使い、それぞれの義務を `omega` で閉じることになります。紙の上の「同様に確かめられる」が、形式化では 2 つの独立した証明義務になります。 「自然数 $n$ について $n/n=1$」を Lean で `∀ n : Nat, n / n = 1` と形式化したとする。(1) この主張が偽であることを示せ。(2) 正しい形に直せ。(3) 逆に、仮定を付けすぎて主張が意図より弱くなる例を一つ考えよ。 (1) $n=0$ のとき $0/0=0\ne1$。Lean では `example : ¬ ∀ n : Nat, n / n = 1 := fun h => absurd (h 0) (by decide)` で確かめられる。(2) `∀ n : Nat, 0 < n → n / n = 1`。標準ライブラリの `Nat.div_self` がこの形の定理で、`fun _ hn => Nat.div_self hn` が証明になる。(3) たとえば「閉区間上の連続関数は有界である」を、「連続関数 `f` が `∀ x, |f x| ≤ 1` を満たすならば `∃ M, ∀ x, |f x| ≤ M`」と書いてしまうと、結論に必要な性質（有界性）が仮定に紛れ込んでおり、`M = 1` で自明に証明できるが、意図した定理とは無関係である。極端な場合、仮定が矛盾していれば（たとえば `0 < 0` を仮定に含めれば）どんな結論も証明できてしまう。仮定が充足可能であることを、具体例で確かめておくのが安全です。 の拡張が一意でない例を挙げよ。 $X=\mathbb{R}^2$、$p(x,y)=|x|+|y|$（劣線形）、$M=\{(x,0)\}$、$f(x,0)=0$ とする。任意の $c\in[-1,1]$ について $F_c(x,y)=cy$ は線形で、$M$ 上で $0$、$F_c(x,y)=cy\le|y|\le p(x,y)$。よって拡張は無数にある。 の証明では $c$ を上限 $a=\sup_m(f(m)-p(m-x_0))$ に選んだが、この例では $x_0=(0,1)$ として $a=\sup_x(-|x|-1)=-1$、$b=\inf_x(|x|+1)=1$ で、$[a,b]=[-1,1]$ のどの値を選んでもよい。一意に定まる値（上限）を選ぶ規則を決めたことが、選択公理を避けられた理由です。 ## 参考文献 - The mathlib Community, "The Lean Mathematical Library", in *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)*, ACM, 2020, 367–381. [doi:10.1145/3372885.3373824](https://doi.org/10.1145/3372885.3373824) - J. Avigad and P. Massot, *Mathematics in Lean* — [オンライン版](https://leanprover-community.github.io/mathematics_in_lean/)（型クラスによる代数構造、位相と解析の形式化）。 - K. Buzzard, J. Commelin and P. Massot, "Formalising perfectoid spaces", in *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)*, ACM, 2020, 299–312. - J. Avigad, L. de Moura, S. Kong and S. Ullrich, *Theorem Proving in Lean 4* — [オンライン版](https://lean-lang.org/theorem_proving_in_lean4/)（型クラス、商、公理の章）。 - W. Rudin, *Functional Analysis*, 2nd ed., McGraw-Hill, 1991 — 第 3 章（ハーン–バナッハの定理）。