Lean 4 で補題の変更によって後続定理の証明が失敗する条件を検証する

補題が保証していた等式を不等式へ変更すると、補題そのものが正しくても、その結果を利用する後続定理の証明には再検証が必要です。等式は値の置換を許しますが、一方向の不等式から同じ置換は導けません。

自然数 x、y、z について、次の 3 つを区別します。

条件	y ≤ z の導出	判断根拠
x = y、x ≤ z	成立	y を x に置換できる
x ≤ y、x ≤ z	一般には不成立	x = 1、y = 3、z = 2 が反例になる
x ≤ y、y ≤ x、x ≤ z	成立	両方向の不等式から x = y を導ける

以下では、この依存関係を Lean 4 の小さな証明で確認します。補題を修正した後の判断基準は、変更後の前提から、後続定理が要求する結論を証明できるかです。

Lean 4.35.0 で検証するための環境

macOS または Linux のシェルを使用します。Lean 公式の手順ではバージョン管理に elan を利用します[1]。対象は 2026-10-12 に公開された Lean 4.35.0 に固定します[2]。

elan を導入済みの環境で、作業ディレクトリーを用意します。

mkdir lean-lemma-dependency
cd lean-lemma-dependency
elan toolchain install leanprover/lean4:v4.35.0
lean +leanprover/lean4:v4.35.0 --version

バージョン表示に 4.35.0 が含まれることを確認します。elan が未導入の場合は、先に公式インストール手順に沿って導入してください。以降の例では Mathlib や外部の Lean ライブラリーを使用せず、Lean 本体の Nat と標準の証明機能を使います。

ファイルごとに補題の定義を変更するため、4 つの .lean ファイルはそれぞれ独立して検査します。各節に記載する成功・失敗は、証明項と反例から予想される結果です。この記事の作成環境には Lean が導入されていないため、コマンドの実測ログとしては記載しません。

等式を前提とする補題と後続定理

変更前の補題 relation は、x = y という等式を受け取り、その等式を保証します。後続定理 downstream は、この補題を使用して x ≤ z から y ≤ z を導きます。まず Before.lean を作成します。

Before.lean

theorem relation (x y : Nat) (h : x = y) : x = y := by
  exact h

theorem downstream (x y z : Nat)
    (hXY : x = y) (hXZ : x ≤ z) : y ≤ z := by
  have hEq : x = y := relation x y hXY
  rw [← hEq]
  exact hXZ

#check downstream
#print axioms downstream

次のコマンドで検査します。

lean +leanprover/lean4:v4.35.0 Before.lean

rw [← hEq] は、結論の y を x に書き換えます。証明すべき条件が x ≤ z になり、既存の仮定 hXZ を使って証明を完了できます。#check downstream では定理の型、#print axioms downstream では推移的に依存する公理を確認します。公理監査の方法は Lean の公式検証ガイドで説明されています[3]。

補題を不等式に変更した場合

今度は、上流から得られる保証を x = y から x ≤ y に弱めます。この最小モデルでは、後続定理へ渡される前提も x ≤ y に変更し、元の結論 y ≤ z は維持します。これにより、以前の証明を同じ形で成立させられるかを検査できます。

After.lean を次のように作成します。

After.lean

theorem relation (x y : Nat) (h : x ≤ y) : x ≤ y := by
  exact h

theorem downstream (x y z : Nat)
    (hXY : x ≤ y) (hXZ : x ≤ z) : y ≤ z := by
  have hLE : x ≤ y := relation x y hXY
  rw [← hLE]
  exact hXZ

lean +leanprover/lean4:v4.35.0 After.lean

ここでは rw [← hLE] による書き換えでエラーが期待されます。hLE は x ≤ y の証明であり、等式の書き換え規則として利用できません。補題 relation の結論を弱めると、元の証明で利用していた y から x への置換を実行できなくなります。

この失敗は、記述した証明が新しい前提のもとで成立していないことを示します。ただし、個別の証明が失敗したことだけでは、その定理が偽であるとは確定しません。次に命題そのものへの反例を調べます。

反例によって結論を導けないことを確認する

x = 1、y = 3、z = 2 を代入します。1 ≤ 3 と 1 ≤ 2 は真ですが、3 ≤ 2 は偽です。この反例は、以下の全称命題を否定します。

\forall x,y,z\in\mathbb{N},\quad
(x\leq y\land x\leq z)\Rightarrow y\leq z

Counterexample.lean では、前提が成立する具体例から偽の結論を導けると仮定し、矛盾を示します。

Counterexample.lean

example : (1 : Nat) ≤ 3 := by
  decide

example : (1 : Nat) ≤ 2 := by
  decide

example : ¬ ((3 : Nat) ≤ 2) := by
  decide

theorem counterexample :
    ¬ (∀ x y z : Nat, x ≤ y → x ≤ z → y ≤ z) := by
  intro h
  have hYZ : (3 : Nat) ≤ 2 :=
    h 1 3 2 (by decide) (by decide)
  exact (by decide : ¬ ((3 : Nat) ≤ 2)) hYZ

#print axioms counterexample

lean +leanprover/lean4:v4.35.0 Counterexample.lean

decide は、この具体的な自然数の比較について真偽を計算し、成立する命題の証明を作ります。counterexample は、任意の自然数について成立すると仮定した命題が、1、3、2 において矛盾を生むことを証明します。

反例が否定する対象は、弱められた前提だけから y ≤ z を導くという全称命題です。等式 x = y を前提とした変更前の定理については、この反例の 1 = 3 が偽なので、反例には当たりません。

追加条件から後続定理を修復する

補題が返す x ≤ y に加え、y ≤ x が成立する場合には、自然数の順序の反対称性から x = y が得られます。この条件を後続定理へ追加した Repaired.lean を作成します。

Repaired.lean

theorem relation (x y : Nat) (h : x ≤ y) : x ≤ y := by
  exact h

theorem downstream_repaired (x y z : Nat)
    (hXY : x ≤ y) (hYX : y ≤ x) (hXZ : x ≤ z) : y ≤ z := by
  have hLE : x ≤ y := relation x y hXY
  have hEq : x = y := Nat.le_antisymm hLE hYX
  rw [← hEq]
  exact hXZ

#check downstream_repaired
#print axioms downstream_repaired

lean +leanprover/lean4:v4.35.0 Repaired.lean

Nat.le_antisymm は、x ≤ y と y ≤ x から x = y を導きます。得られた等式を使えば、変更前と同じ書き換えによって y ≤ z を証明できます。

ただし、修復後の定理には新しい仮定 hYX : y ≤ x が含まれています。そのため、呼び出し側がこの仮定を証明できる場合に限り downstream_repaired を適用できます。定理の型検査が成功することと、すべての使用箇所で追加条件を満たせることは、別の検証対象です。

補題変更後の検証結果を比較する

ファイル	期待結果	検査で確かめる内容	数学的な帰結
Before.lean	成功	等式を利用する証明が受理される	x = y と x ≤ z から y ≤ z が成立する
After.lean	意図的な失敗	不等式 hLE を用いた rw [← hLE] では等式による書き換えが成立しない	提示した後続証明は新しい前提に適合しない
Counterexample.lean	成功	弱めた前提のもとで全称命題が偽であることを証明する	x ≤ y と x ≤ z だけでは結論を保証できない
Repaired.lean	成功	反対向きの不等式を追加すると証明を構成できる	y ≤ x を満たす範囲で元の結論を導ける

Lean のコンパイルにおける失敗と、数学的な命題への反例を分ける必要があります。After.lean の書き換え失敗は特定の証明の失敗、Counterexample.lean は変更後の全称命題そのものが偽であることの証明です。修復では、追加仮定を含む新しい定理を証明したことになります。

証明の修復時に確認する条件

補題を変更した際には、変更した行に加えて、補題を利用する定理の型と各使用箇所の仮定を照合します。特に次の関係が判断基準になります。

確認対象	成立を確認する条件	条件が欠けた場合
補題の結論	利用側が必要とする性質を導ける	結論を使う推論の再構成が必要になる
補題の仮定	それぞれの使用箇所で仮定を証明できる	修復した補題をその箇所へ適用できない
後続定理の型	元の適用範囲と結論を維持できる	条件を追加した別の定理として扱う
公理への依存	#print axioms が許容する公理のみを示す	sorryAx や独自公理の根拠を確認する

#check では修復前後の定理文を比較し、#print axioms では未完成の証明を示す sorryAx などの依存関係を確認します。sorry を使って定理の型検査を通した場合には、その証明が完成したという評価を避ける必要があります。証明の検査と定理文の意味を区別する方法は、既稿「AI 生成証明を Lean 4 の型検査と公理監査で検証する」でも扱っています[4]。

今回の数値例は補題の保証が等式から不等式に変わる影響を抽出したものです。原典で扱った有限単純群の分類に関する形式化でも、中間的な等式を不等式へ変更した際に、後続の議論で使われていた性質を改めて確保する必要が生じています[5]。ここでの Lean コードは、その群論上の補題そのものを形式化したものではなく、論理的な依存関係を自然数で再現する例です。

補題を修正した後の完了条件は、補題単体の型検査が成功することだけではありません。後続定理の結論と適用範囲を確認し、追加条件を要求する場合は、その使用箇所で条件を満たす根拠まで接続することです。

参考文献

1. Lean Project, Install. https://lean-lang.org/install/manual/
2. Lean Project, Lean 4.35.0（2026-10-12）. https://lean-lang.org/doc/reference/latest/releases/v4.35.0/
3. Lean Project, Validating a Lean Proof. https://lean-lang.org/doc/reference/latest/ValidatingProofs/
4. id774, AI 生成証明を Lean 4 の型検査と公理監査で検証する（2026-09-08）. https://qiita.com/ynakayama/items/82d955c49be465d623f8
5. id774, 証明の誤りは、結論まで届くのか（2026-11-01）. https://blog.id774.net/entry/2026/11/01/5834/