Lean4: 入門 Lean 形式化 証明の世界へようこそ！

過去記事のサンプルをもう一度見直して入門レベルに落としてみる。

-- File: MathlibHello/Coprime.lean

import Mathlib

namespace MyMathlib

open Nat

/-- This theorem states that for any natural number n,
the greatest common divisor (gcd) of n and n + 1 is 1. -/

theorem coprime_self_succ (n : ℕ) : Nat.gcd n (n + 1) = 1 := by
  -- gcd(n, n+1) = gcd(n+1, n) = gcd(n, (n+1) % n)
  rw [Nat.gcd_comm]
  rw [Nat.gcd_rec]
  rw [Nat.mod_eq_of_lt (Nat.lt_succ_self n)]
  simp

#eval Nat.gcd 5 (5 + 1)  -- output should be 1
#eval Nat.gcd 0 (0 + 1)  -- output should be 1

end MyMathlib

この環境構築後に実行テストしてみるサンプルなのだけど、入門者からしてみたらだいぶ敷居が高いことが今なら解る。入門者が求める最初の一歩は、単一命令で事、済ませられる内容である。

入門者用サンプルコード

ということで書き直してみた。

import Mathlib

namespace sample1

/-- This theorem states that for any natural number n,
the greatest common divisor (gcd) of n and n + 1 is 1. -/
-- 自然数 n に対して、n と n+1 の最大公約数は 1 である。
-- つまり全ての n と n+1 は「互いに素」である。

example (n : ℕ) : Nat.gcd n (n + 1) = 1 := by

  -- 交換律とユークリッド互除法を使う。
  -- さらに n < n+1 より (n+1) % n = 1 であることを使う。
  -- 最後に gcd(1, n) = 1 であることを使う。
  -- つまり、以下のように書き換えていく。
  -- gcd(n, n+1) = gcd(n+1, n) = gcd(n, (n+1) % n) = gcd(n, 1) = 1
  -- これらの書き換えを `rw` タクティクで実行する。
  
  -- ⊢ n.gcd n (n + 1) = 1 を証明する。
  rw [Nat.gcd_comm]                       -- ⊢ (n + 1).gcd n = 1
  rw [Nat.gcd_rec]                        -- ⊢ (n % (n + 1)).gcd (n + 1) = 1
  have : n < n + 1 := Nat.lt_succ_self n  -- this : n < n + 1
  rw [Nat.mod_eq_of_lt this]              -- ⊢ n.gcd (n + 1) = 1
  rw [Nat.gcd_self_add_right]             -- ⊢ n.gcd 1 = 1
  rw [Nat.gcd_one_right]                  -- ⊢ 1 = 1

end sample1

import〈ライブラリ名〉

Mathlib という数学ライブラリを取り込んで使えるようにする。これにより、数学の定理や補題、定義が参照できるようになります。さらに「戦略」と呼ばれる Tactics が使えるようになり、数学の形式的証明が記述できるようになります。

namespace〈名前空間〉

これから定義する名前〈識別子〉が一意でなければなりませんが、名前が被ってしまうことがあります。この名前空間で、それを回避します。

コメント /-- … -/ /- … -/ --

/-- 定義用のコメント -/

/-
通常のコメント：
  コメントブロックなので
  複数行で書けます。

定期用のコメント：
  上記の定義用もコメントブロックです。
  見分け方は / の後に -- ２個が定義用 - １個が通常です。

違いは、
- 定義用は定義の前に書く１つだけ許されたコメント
- 通常は、どこでも書ける

特徴：
- Markdown も書いておける。
- 定義用はプログラム中から参照できる
-/

-- １行コメント
-- ← 開始は "--" ２個以上 ----------------- もコメント
-- コメント終了の指定は不要 →
-- 改行までがコメントです。
-- どこでも書ける。命令の後ろとか。

って感じです。

コメントは処理とは関係ないので無駄だと思われがち。しかし、現代においては AI がソースコードの真意を理解するのにコメントが重要。コメントまで読んで理解してコードを記述してくれる。AI 自身がコメントに未解決証明の手順を書き残して sorry を置いておく。理由は、そのコメントを書いた AI
の魂は消滅していて、次の質問では新しい魂がそれを読む。なのでコメントが残されていないと、次に読む AI は何のことだか解らない。となる。もうコードは人間が読むものではなく AI が読むもの。そういう観点で残そう。

コメントで実装したい内容を書いておけば、それに沿って書いてくれる。

theorem / lemma / def / axiom 〈定義名〉/ example

ここからが難しいところでしょうかね。
定義は、

• example : 例題

• axiom : 公理

• def : 定義

• lemma : 補題

• theorem : 定理

などがあり今回の例では example を使用しました。
識別名を省略して

$$
\text{命題} := \text{by 証明}
$$

と書けます。

命題の記述

(n : ℕ) : Nat.gcd n (n + 1) = 1

〈パラメータ〉:〈式〉

ですね。

• パラメータと「型」
  あとに続く式がどのような入力パラメータを受け取るかを書きます。
  例は変数名 $${n}$$ が自然数$${\N}$$ で受け取る。という意味の書き方です。
  
  整数なら$${\Z}$$ 実数なら$${\R}$$です。他にも複素数$${\mathbb{C}}$$や有理数$${\mathbb{Q}}$$など。
  集合記号 (Set) が「型」となっている。
  $${\N \in \Z \in \mathbb{Q} \in \R \in \mathbb{C}}$$
  この「型」がこの言語の特徴であり型が合ってないと事が進みません。

  • 深堀り Nat.gdc で見る
    Nat.gdc も def 定義により記述されています。
    その受取るパラメータは
    　def gcd (m n : @& Nat)
    と書かれているので m, n を Nat 型(＝$${\N}$$)で受け取るという意味です。m n とスペースで区切り纏めて(…)書きで指定できます。
    Nat.gcd n (n + 1) と呼び出しているので、
    m ← n
    n' ← (n + 1)
    が代入されます。

  • 特殊修飾
    "@&" は参照渡しという意味です。値のコピーを作らない。実体の場所（ポインタ）を教えるだけ。そして見るだけ。書き換え不可。
    ちなみに書き換え可能は "@mut" です。
    デフォルトは値のコピー渡しです。→値渡し 解説詳細→Appendix
    
    なので gdc は、
    m → n
    n' → (n + 1)
    を見に行っている。という内部動作になります。

• 式
  等式でなくても不等式でも良いです。
  記号論理学の記述形式で書いていきます。

記号論理学とは何か（参考リンク）

型 - Type

定義記号

〈これ〉は〈コレ〉です。を

$$
\text{
これ $:=$ コレ
}
$$

と書きます。

証明

証明は〈コレ〉の部分で by ～ の後に書き連ねます。
命題と証明の区切り「:= by」をセットで覚えてしまってもいいですね。

戦略 (Tactic)

この記述をしていくのが Lean 形式化 証明 のメインとなります。
例を見てみましょう

  rw [Nat.gcd_comm]                       -- ⊢ (n + 1).gcd n = 1
  rw [Nat.gcd_rec]                        -- ⊢ (n % (n + 1)).gcd (n + 1) = 1
  have : n < n + 1 := Nat.lt_succ_self n  -- this : n < n + 1
  rw [Nat.mod_eq_of_lt this]              -- ⊢ n.gcd (n + 1) = 1
  rw [Nat.gcd_self_add_right]             -- ⊢ n.gcd 1 = 1
  rw [Nat.gcd_one_right]                  -- ⊢ 1 = 1

rw - Rewrite

rw [ … ] と、たくさん並べて書かれています。入門者は最初にこれを学び、仕組みを学びます。これを楽にしてくれるのが他の命令だと思えば良い。

命題が与えられた時、証明のゴール goal ⊢ が

⊢ n.gcd (n + 1)  1

として設定されます。これは命題のままですね。（※(n + 1) = m です。）
これを変形させていき、両辺が等しいことを示せば証明完了です。

rw [Nat.gcd_comm]

Nat.gcd_comm という定理を使って書き換えます。Mathlib Gcd.lean にあります。Lean の大変なところは、この数学的な定理をライブラリから探す。または、自分で証明し直す事です。

theorem gcd_comm (m n : Nat) : gcd m n = gcd n m

定理は gcd m n と gcd n m は等しい。となってます。つまり n と m は位置を交換できる。なので、この命令実行後、ゴールが、

⊢ n.gcd (n + 1) = 1
↓ m ⇔ n → [n' = n, m = (n + 1) ⇔ n' = (n + 1), m = n]
⊢ (n + 1).gcd n = 1

⊢ (n + 1).gcd n = 1

に書き換わる。

次は、Nat.gcd_rec で書き換え

theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m

gdc m n は gcd (n % m) m に書き換えられる。という定理。

                  -- ⊢ (n + 1).gcd n = 1
                  -- ↓
rw [Nat.gcd_rec]  -- ⊢ (n % (n + 1)).gcd (n + 1) = 1

見た目が複雑になりましたが、代入して展開した！と、納得してしまう。
Lean が書き換えたのだから正しい！という大前提があるから信用する！←

have

補助補題 have の登場です。

have : n < n + 1 := Nat.lt_succ_self n  -- this : n < n + 1

ミニ証明を中で行って、こういう条件がある。と、示します。
n < (n + 1) の大小関係は常に真である。無名定理証明を行っています。
証明は Nat.lt_succ_self n でしてくれていますので、その結果を this で保持してます。（一時変数「これ」）

theorem Nat.lt_succ_self (n : Nat) : LT.lt n (succ n) := Nat.lt_add_one _

succ は後続。succ n で n の後続なので n + 1 です。それは Nat.lt_add_one で示されています。その証明を追ってくとそう単純な証明ではないですね。
１＋１＝２を真面目に証明しているようないちいちくどい感じです（笑）

protected theorem
Nat.lt_add_one (n : Nat) : LT.lt n (HAdd.hAdd n 1) := Nat.le_refl (succ n)

すこしそれました。ここで、
this : n < n + 1 が確定しました。

Nat.mod_eq_of_lt〈これ〉で、その不等式の前提（条件）を使います。

rw [Nat.mod_eq_of_lt this]  -- ⊢ n.gcd (n + 1) = 1

theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a

a b はそれぞれ次の前提条件の a < b が自動で割り当てられ mod_eq_of_lt の証明で使われる補助補題 h に前提条件 h := this : n < n + 1 が入ります。
a = n
b = n + 1
なので a が返ってくる。

a < b ならば a % b = a 合同演算（剰余演算）で除数が被除数より大きいなら割れないので、そのまま a が余りとして出てくる。

(n % (n + 1)) → n

これで複雑なゴールが、単純な

⊢ n.gcd (n + 1) = 1

に、なりました。

⊢ (n % (n + 1)).gcd (n + 1) = 1
↓ (n % (n + 1)) → n へと書き換えられた a = n, b = (n + 1) よって a % b = a = n
⊢ n.gcd (n + 1) = 1

続いて、Nat.gcd_self_add_right

rw [Nat.gcd_self_add_right]  -- ⊢ n.gcd 1 = 1

theorem gcd_self_add_right (m n : Nat) : gcd m (m + n) = gcd m n

gcd m (m + n) は gcd m n である。と、言ってます。ゴールの記述と違うので分かりにくいですが、m.gcd (m + n) = m.gcd n と、読み替えると、

⊢ n.gcd (n + 1) = 1
↓ ここでは n = m なので n = 1 ややこしい…。m.gcd (m + 1) → m.gcd 1
⊢ n.gcd 1 = 1

最後に Nat.gcd_one_right で gcd n 1 (n.gcd 1) は = 1 である。

theorem gcd_one_right (n : Nat) : gcd n 1 = 1

なのでゴールがついに

rw [Nat.gcd_one_right]  -- ⊢ 1 = 1

⊢ 1 = 1

両辺が等しくなったので証明完了です！

証明が完了した命題には✅️マークが付きます。これでゲームクリアです！

お疲れ様でした。

あれ？いつの間にかゲームになってる？🎮️

このゲームの醍醐味は、a = b としても b = a では証明されない。
a = a または b = b にしないといけない。具体的には、a → b の変換手順。
a → b = b という a → b になる過程を記述していくのです。
👨‍🌾 a さんを 👨‍🔧 b さんに変身させ 👨‍🔧 b ＝ 👨‍🔧 b と言わなければいけない。

未解決問題は 👨‍🌾 → 🛸 全く異なる物にまで変身…な難問かもしれない…✍️

あとがき

ゴールが単純化されてあとは自動で結果が導ける！となったら便利な命令
simp などの自動化命令で細かく書かなくても済みます。そういう事です。

複雑な式変換は calc で変換過程を示したり、場合分けしたり、分解したり
２つの結果から導き示したり、などの戦略が幾つかあるという世界です。

数学をゲームから学ぶ。みたいな言語だ。という事を聞きましたが、確かにそんな感じです。けど、こう細かく噛み砕かないと数学は学べません（笑）

Mathlib を読み解けば、形式化された数学定理の原理構造まで解るでしょう
（と言ってる私は何も解ってない😅）✍️

2025/10/08 20:14

D.

#Lean #Lean4 #Mathlib #Mathlib4 #数学 #形式証明 #ゲーム #入門 #入門書

Appendix

名前空間

ゴールの記号

rw 内を並べて記述

こうして一度に書くことも可能

namespace sample2

theorem coprime_self_succ (n : ℕ) : Nat.gcd n (n + 1) = 1 := by
  rw [Nat.gcd_comm, Nat.gcd_rec, Nat.mod_eq_of_lt (Nat.lt_succ_self n),
      Nat.gcd_self_add_right, Nat.gcd_one_right]

end sample2

別の証明方法

def Coprime (m n : Nat) : Prop := gcd m n = 1
を使っての証明（内部で gcd 使ってるので命題としては同じですけどね）

namespace sample3

lemma coprime_self_succ (n : ℕ) : Nat.Coprime n (n + 1) := by
  rw [Nat.Coprime]
  have : ∀ d, d ∣ n → d ∣ n+1 → d = 1 := by
    intro d hdn hdn1
    have : d ∣ (n+1) - n := Nat.dvd_sub hdn1 hdn
    simp at this
    omega
  have h1 : n.gcd (n+1) ∣ n := Nat.gcd_dvd_left n (n+1)
  have h2 : n.gcd (n+1) ∣ n+1 := Nat.gcd_dvd_right n (n+1)
  exact this _ h1 h2

end sample3

答えはひとつでも、経路は複数。数学オタク系は、この経路の一番美しい道「エレガント」なルート、美しく合理的経路を含めての結果を探し、そこから真理の探求をしようとしている。答えに繋がる経路には他の結果に繋がる道にも伸びている。つまり、経路でさえも一本道ではなく、寄り道もある。

数学地図が描かれれば、そこに無い道を自ら開拓して別の答えに繋がる道を見つけられるかもしれない。道を勝手に作るのではなく、未だ誰も通った事の無い道を探し描き繋げる。ただひとつ教えられた道だけで満足してない？

用語：参照渡し、値渡し

プログラミングで言う参照渡しという用語

「参照渡し（pass by reference）」とは、プログラミング言語で関数に引数を渡す際に、変数そのものの“実体”ではなく、その参照（アドレス）を渡す方法のことじゃ。

たとえば、普通の「値渡し（pass by value）」ではこうなる：

• 関数に値を渡すとき、その値のコピーが関数内に渡される。  

• 関数の中で変更しても、元の変数には影響がない。

一方「参照渡し」では：

• 関数に変数の参照（メモリアドレスのようなもの）が渡される。

• 関数内でその変数を変更すると、呼び出し元の変数も変わる。

例（C++ の場合）

void addOne(int &x) {
    x = x + 1; // 参照を通して元の変数を書き換える
}

int main() {
    int n = 5;
    addOne(n);
    // n は 6 に変わっている
}

ここでは `int &x` が「参照渡し」を意味しておる。
`x` は `n` と同じメモリ領域を指しているから、`x` を変えると `n` も変わるんじゃ。

対比して「値渡し（pass by value）」

void addOne(int x) {
    x = x + 1; // コピーを変更しているだけ
}

int main() {
    int n = 5;
    addOne(n);
    // n は 5 のまま
}

他言語での扱い

• Python：すべて「参照渡し風の値渡し」。オブジェクトへの参照が渡されるが、再代入するとローカルだけが変わる。
  つまり「ミュータブルなオブジェクト（リスト、辞書）」は中身が変わるが、「イミュータブル（整数、文字列）」は変わらない。

• Java：厳密には「参照の値渡し（pass-by-value of reference）」。

• Rust：`&T` が「参照渡し」、`&mut T` が「可変参照渡し」。ただし所有権と借用規則によって安全に制御される。

• Lean：`@&` という注釈で「引数を読み取り専用参照として受け取る」最適化がある（コピーを避けるだけで、可変ではない）。

要するに参照渡しとは、「データそのものではなく、その場所を渡して操作する」ことじゃな。
古い言い方をすれば「手紙の写し」ではなく「宝箱の鍵」を渡すようなものじゃ。

補足、余談

🎁宝箱の鍵🔑の例だと、参照権限しか渡さないは→宝箱は開けられるが、中には丈夫なガラス張りの🔏鍵付きの箱があり中身🍎は見える。
それを塗り直して🍏にすることは出来ない。@&

参照鍵🔑と改変鍵🔐両方を渡した場合、見れる🍎し🍏にして相手に返すこともできる。&mut

※C言語には、この区別はなく const によって定数として改変阻止する。
※プログラミング各言語の設計思想によりこのへんは左右する。

最近の流行りは Rust 設計指向

ちなみに Lean は一旦 CLang にして LLVM → CPU機械語 という手順で翻訳されているらしい。InfoView インタプリタ処理は CLang に翻訳されたところで動いているらしい。exe 形式まではビルドしてない？そのうち必要になったら原理調べて紹介する記事を書くだろう。いま、詳しく書いても発展途上ゆえに変わる可能性があるので骨折り損かもしれない。

関連

ほぼ AI に理論だけ伝えて書かせたコード

Lean の答えがわからなければ AI に解かせる。そして解けない命題は「偽」である。と Lean も AI も教えてくれる。Lean は AI のための言語。正しくないと動かない。が実現できる。間違ったコードが減る。だが、まだ Lean も発展途上なので完璧ではない。となるとやはり人間も読めて書けないとダメである。