Lean4: 偶数・奇数の性質を記述する(Paperproof の紹介を兼ねて)

ABC予想の形式化から Lean を学ぶという暴挙をしてます（笑）
$${a+b=c}$$ という単なる足し算の世界。何も難しいことはない。
小学生低学年から学ぶ内容。だからきっと簡単な問いに違いない（←待て）

よくわからないまま Lean に触れて半年以上。
真面目に始めて３ヶ月でしょうかね？

AI アシスタント無しでは習得不可能なレベルで難易度の高い言語です。
なんせ数学の知識が必要。それらを前提として眺めないと読めません。
今でも、そう感じています。そして解ってません…。😅

数学的に当たり前なこと（自明）も Lean ではバカ正直に、クソ真面目にちゃんと書かなければならない。
自然数$${\N}$$と整数$${\Z}$$と実数$${\R}$$は同じ数「３」であっても、そのままでは
$${3:\N\ne3:\R}$$で$${\N\to\R}$$へ変換が可能$${\uparrow3:\N=3:\R}$$だよ！という事を教え

$$
\Large
3:\N = 3:\R\\[4pt]
\normalsize
(3:\N = \uparrow3:\N=3:\R)
$$

けっこう、この「型」合わせの部分は疲れます。
$${\N}$$ 型の証明が書けたら、それを実数版$${\R}$$でも書いて、
「その２つは同じだ！」*_eq, *_iff と教える補題も書いて繋げておく必要がある。離散と連続を同一視しない世界。数学で「連続」というのを調べると極限視点でいろいろ考えるらしい。離散点とつながる方向が大事なのか。

（前置き長い！）

偶数・奇数

ということで、バカ正直、クソ真面目に Lean で偶数と奇数を書いていく。

偶数の定義 even

/-- 自然数 `n` が偶数であることを表す述語 `even n` の定義。 -/
def even (n : ℕ) : Prop := n % 2 = 0

奇数の定義 odd

/-- 自然数 `n` が奇数であることを表す述語 `odd n` の定義。 -/
def odd (n : ℕ) : Prop := n % 2 = 1

「２」

偶数か奇数か？を判別するのに「２」偶素数ぐうそすうが必須である。
n % 2 の合同演算で余りを見る。０ならば偶数。１ならば奇数という定義。

$$
\begin{array}{l}
n \mod 2 = 0 \quad \implies \text{even}\\
n \mod 2 = 1 \quad \implies \text{odd}
\end{array}
$$

偶素数「２」

偶数・奇数を分ける素数→偶素数「２」を証明していこう！
いきなり難易度あがりますが、最初に偶数・奇数を分ける要石の「２」が、素数であり、偶数であり、素数の中で唯一偶数である数だという補題です。

$$
\large
\text{even } p\; \land\; p \in \mathbb{P} \; \implies \; p =2
$$

p が偶数で、かつ、p が素数 $${\mathbb{P}}$$ ならば p = 2 である。

eq_two_of_even_prime

/--
`eq_two_of_even_prime` は、
自然数 `p` が素数かつ偶数である場合に `p = 2` であることを示す補題です。

数学的背景:
- 素数の定義より、`p` は 2 以上の自然数です。
- 2 より大きい素数は必ず奇数であり、偶数の素数は 2 のみです。
- `even p` より `p % 2 = 0` となるが、素数で 2 で割り切れるものは 2 しかありません。

証明の流れ:
1. `p` が偶数であることから `p % 2 = 0` または `p % 2 = 1` の場合分けをします。
2. `p % 2 = 0` の場合、`p` は 2 で割り切れる素数なので `p = 2` です。
3. `p % 2 = 1` の場合は `p` が偶数であることと矛盾します。

この補題は、偶数の素数が 2 のみであることを形式的に証明します。
-/

lemma eq_two_of_even_prime {p : ℕ} (hp : p.Prime) (heven : even p) : p = 2 := by
  -- 素数かつ偶数ならば p = 2 しかない
  rw [even] at heven
  -- 素数 p > 2 は必ず奇数なので、偶数素数は p = 2 のみ
  have hcases := Nat.mod_two_eq_zero_or_one p
  cases hcases with
  | inl h0 =>
    -- p % 2 = 0 かつ p は素数なので p = 2
    have hpos : 0 < p := hp.pos
    -- p ≠ 1 なので p ≥ 2
    have hge2 : 2 ≤ p := hp.two_le
    -- 2 で割り切れる素数は 2 のみ
    have hdiv : 2 ∣ p := Nat.dvd_of_mod_eq_zero h0
    rw [Nat.prime_dvd_prime_iff_eq Nat.prime_two hp] at hdiv
    exact Eq.symm hdiv
  | inr h1 =>
    -- p % 2 = 1 の場合は偶数ではないので矛盾
    exfalso
    rw [h1] at heven
    linarith

p という自然数を受け取り、

• p は素数 Nat.Prime p であるという仮定（条件）
  これは Mathlib にて素数性を証明する

• p は偶数 even p であるという仮定（条件）
  先程定義した偶数の性質 p % 2 = 0 となる

これを２つのケースに分けて矛盾を示して
eq_two_of_even_prime : p = 2 を証明

奇数ならば偶数ではない

当然なことですが Lean はこれを知りません。
真面目に教えてあげなければなりません。
教えさえすれば次回からは、この補題を見て「そうだ！」と認めます。

$$
\large
\text{odd } n \iff \neg\; \text{even } n
$$

odd_iff_not_even

/--
`odd_iff_not_even` は、
自然数 `n` に対して「`n` が奇数であること」と「`n` が偶数でないこと」が同値である。
ということを示す補題です。

証明の概要:
- 奇数 (`odd n`) は `n % 2 = 1`、偶数 (`even n`) は `n % 2 = 0` で定義されています。
- まず、`n` が奇数ならば偶数ではないこと（`n % 2 = 1 → ¬ (n % 2 = 0)`）を示します。
  `n % 2 = 1` ならば `n % 2 = 0` とはならないので、矛盾します。
- 次に、`n` が偶数でないならば奇数であること（`¬ (n % 2 = 0) → n % 2 = 1`）を示します。
  `n % 2` は常に `0` または `1` なので、`0` でないなら必ず `1` です。

この補題は、偶奇判定の基本的な性質を形式的に証明しています。
-/

lemma odd_iff_not_even {n : ℕ} : odd n ↔ ¬ even n := by
  rw [even, odd]
  -- n % 2 = 1 ↔ ¬ (n % 2 = 0)
  constructor
  -- (→) odd n → ¬ even n
  intro h
  intro heven
  rw [h] at heven
  -- h : n % 2 = 1, heven : n % 2 = 0
  linarith
  -- (←) ¬ even n → odd n
  intro hne
  cases Nat.mod_two_eq_zero_or_one n with
  | inl h0 =>
    -- n % 2 = 0 の場合 even n なので ¬ even n は false
    exfalso
    apply hne
    exact h0
  | inr h1 =>
    -- n % 2 = 1 の場合 odd n
    exact h1

自然数 n が偶数ならば n + 1 は奇数

偶数に +1 したら奇数になる。
当たり前なことですが（以下略）

odd_add_one_of_even

/--
`odd_add_one_of_even` は、
自然数 `n` が偶数であるとき、`n + 1` が奇数であることを示す補題です。

数学的背景:
偶数とは、2で割り切れる整数（`n % 2 = 0`）です。
奇数とは、2で割った余りが1になる整数（`n % 2 = 1`）です。
この補題では、`n` が偶数である（`even n`）という仮定から、
`n + 1` が奇数（`odd (n + 1)`）であることを導きます。

証明の流れ:
1. `even n` の定義より、`n % 2 = 0` であることを仮定します。
2. `odd (n + 1)` の定義より、`(n + 1) % 2 = 1` を示します。
3. 加法の合同式 `Nat.add_mod` を用いて、
   `(n + 1) % 2 = (n % 2 + 1 % 2) % 2` であることを示します。
4. `n % 2 = 0` を代入し、`(0 + 1) % 2 = 1` となるため、`n + 1` は奇数です。

この補題は、偶数と奇数の性質に基づく基本的な事実を Lean で形式化したものです。
-/

lemma odd_add_one_of_even {n : ℕ} (heven : even n) : odd (n + 1) := by
  -- n が偶数ならば n + 1 は奇数
  rw [even] at heven
  rw [odd]
  -- (n + 1) % 2 = 1 を示す
  have hmod : (n + 1) % 2 = (n % 2 + 1 % 2) % 2 := by
    rw [Nat.add_mod]
  rw [hmod]
  rw [heven]

Nat.add_mod
⊢ ∀ (a b n : Nat), (a + b) % n = (a % n + b % n) % n

の定理を使って (n + 1) % 2 = 1 のカタチに持っていき
odd n' = n' % 2 = 1 ならば n' = (n + 1) だから！という証明ですかね。

2 * n + 1 は奇数

別の書き方ですね。任意の n を２倍して偶数として＋１して奇数とする。
２倍を一般化して even * n + 1 is odd とも書けるでしょう。
任意の n に偶数を掛けると偶数になる補題は次で紹介します。

odd_of_form_two_n_plus_one

/--
`odd_of_form_two_n_plus_one` は、
任意の自然数 `n` に対して `2 * n + 1` の形の数が奇数であることを証明する補題です。

数学的には、`2n + 1` の形の数は常に奇数です。
これは、`2n` が偶数であり、そこに 1 を加えることで奇数になるためです。
証明では、`odd` の定義（`n % 2 = 1`）を用いて、`(2 * n + 1) % 2` を計算します。
加法の合同式 `Nat.add_mod` を使い、`2n % 2 = 0` と `1 % 2 = 1` を利用して、
最終的に `(0 + 1) % 2 = 1` となることを示しています。

この補題は、奇数の性質や合同式の計算の理解に役立ちます。
-/

lemma odd_of_form_two_n_plus_one (n : ℕ) : odd (2 * n + 1) := by
  -- 2n + 1 の形の数は奇数であることを示す
  rw [odd]
  -- (2n + 1) % 2 = 1 を示す
  have hmod : (2 * n + 1) % 2 = ((2 * n) % 2 + 1 % 2) % 2 := by
    rw [Nat.add_mod]
  rw [hmod]
  -- 2n % 2 = 0, 1 % 2 = 1 なので (0 + 1) % 2 = 1
  have h2n : (2 * n) % 2 = 0 := Nat.mul_mod_right _ _
  have h1 : 1 % 2 = 1 := by norm_num
  rw [h2n, h1]

偶数の掛け算は偶数

素因子に「２」が含まれている数 n はすべて偶数です。
偶数という条件で因子に「２」を持ってます。
掛け算（積）は因子を除去しませんのでずっと残ります。
奇数に「２」を掛けるとすべて偶数になります。
（その数は２で割れるようになるからです）

当たり前も、このように因子の原理を理解するとコラッツ予想の問題も中身が見えてくるようになります。あれは、偶数世界と奇数世界を行き来して数を収束させるゲームです。ABC予想はその逆の問題かもしれません。

even_mul_left

/--
`even_mul_left` 補題は、自然数 `a` が偶数であるとき、
任意の自然数 `b` に対して積 `a * b` も偶数であることを示します。

証明の流れ:
- `a` が偶数であることから、`a % 2 = 0` である。
- 積の剰余 `(a * b) % 2` は、`(a % 2) * (b % 2) % 2` と書ける（`Nat.mul_mod` より）。
- `a % 2 = 0` なので、`(a * b) % 2 = (0 * (b % 2)) % 2 = 0 % 2` となる。
- `0 % 2 = 0` であるため、`a * b` も偶数となる。

この補題は、偶数の性質を積に関して拡張する際に有用です。
-/

lemma even_mul_left {a b : ℕ} (heven : even a) : even (a * b) := by
  -- a が偶数ならば a * b も偶数
  rw [even] at heven
  rw [even]
  -- (a * b) % 2 = 0 を示す
  have hmod : (a * b) % 2 = ((a % 2) * (b % 2)) % 2 := by
    rw [Nat.mul_mod]
  rw [hmod]
  rw [heven]
  -- 0 * (b % 2) = 0
  rw [zero_mul]
  -- 0 % 2 = 0 を Nat.zero_mod で証明
  exact Nat.zero_mod 2

奇数同士の掛け算は奇数

偶数の世界は「２」の因子を持っている世界です。
基数の世界には「２」の因子が含まれていません。

これが偶数と奇数の世界を分ける最も明確な境界石キーストーンです。
「２」という石を持っているか否かで世界が分かれます。
「＋１」でその石を持つか捨てるか、偶奇世界の行き来を可能とし、どちらかの世界に属するかを左右します。

素数 p は「２」以外、すべて奇数です。
「２」を持たない奇数合成数は、奇数素因子のみを有する事がわかります。

odd_mul_odd

/--
`odd_mul_odd` 補題は、
2つの自然数 `n` と `m` がともに奇数であるとき、その積 `n * m` も奇数であることを示します。

証明の概要:
- `odd n` および `odd m` の仮定から、それぞれ `n % 2 = 1` および `m % 2 = 1` が成り立ちます。
- 積の剰余 `(n * m) % 2` は、`(n % 2) * (m % 2) % 2` と等しいことを利用します。
- したがって、`(n * m) % 2 = (1 * 1) % 2 = 1` となり、`n * m` も奇数です。

この補題は、奇数の積が必ず奇数になるという基本的な性質を形式的に証明しています。
-/

lemma odd_mul_odd (n m : ℕ) (hn : odd n) (hm : odd m) : odd (n * m) := by
  -- n, m が奇数ならば n * m も奇数
  rw [odd] at hn hm
  rw [odd]
  -- (n * m) % 2 = 1 を示す
  have hmod : (n * m) % 2 = ((n % 2) * (m % 2)) % 2 := by
    rw [Nat.mul_mod]
  rw [hmod]
  rw [hn, hm]

コラッツ予想 3n+1

コラッツ予想の奇数操作 $${3n+1}$$ は奇数を偶数へと変換させる操作です。
それを Lean にて形式化する例を書いてみました。

odd_of_form_three_n_plus_one

/--
`odd_of_form_three_n_plus_one` は、
自然数 `n` に対して `3n + 1` の形の数が奇数であることと、
`n` が偶数であることが同値であることを示す補題です。

具体的には、`odd (3 * n + 1) ↔ even n` を証明しています。

証明の流れ：
- `odd` と `even` の定義から、`(3 * n + 1) % 2 = 1 ↔ n % 2 = 0` を示します。
- まず、`odd (3 * n + 1)` ならば `n` が偶数であることを示します。
  - 加法・乗法の合同式を用いて、`(3 * n + 1) % 2` を分解します。
  - `n % 2` が 0 か 1 かで場合分けし、1 の場合は矛盾が生じることを示します。
- 次に、`n` が偶数ならば `3n + 1` が奇数であることを示します。
  - 同様に合同式を用いて計算し、`n % 2 = 0` から `3n + 1` が奇数となることを導きます。

この補題は、数論的な性質の証明や、合同式を用いた場合分けの典型例として有用です。
-/

lemma odd_of_form_three_n_plus_one (n : ℕ) : odd (3 * n + 1) ↔ even n := by
  -- 3n + 1 の形の数が奇数であることと n が偶数であることは同値
  rw [odd, even]
  -- (3n + 1) % 2 = 1 ↔ n % 2 = 0 を示す
  constructor
  -- (→) odd (3n + 1) → even n
  intro h
  have hmod : (3 * n + 1) % 2 = ((3 * n) % 2 + 1 % 2) % 2 := by
    rw [Nat.add_mod]
  rw [hmod] at h
  -- (3n) % 2 + 1 % 2 ≡ 1 (mod 2)
  have h3n_mod : (3 * n) % 2 = (3 % 2 * (n % 2)) % 2 := by rw [Nat.mul_mod]
  rw [h3n_mod] at h
  -- (n % 2 * 1 + 1) % 2 = 1
  have h1 : 1 % 2 = 1 := by norm_num
  rw [h1] at h
  -- (n % 2 + 1) % 2 = 1
  -- h : (1 * (n % 2) % 2 + 1) % 2 = 1 から (n % 2 + 1) % 2 = 1 を導く
  have hsum : (n % 2 + 1) % 2 = 1 := by
    -- (1 * (n % 2) % 2 + 1) % 2 = ((n % 2) % 2 + 1) % 2
    rw [one_mul, Nat.mod_mod] at h
    exact h
  -- n % 2 = 0 を示す
  have hcases := Nat.mod_two_eq_zero_or_one n
  cases hcases with
  | inl h0 =>
    -- n % 2 = 0 の場合 even n
    exact h0
  | inr h1 =>
    -- n % 2 = 1 の場合は矛盾
    exfalso
    rw [h1] at hsum
    -- (1 + 1) % 2 = 0 ≠ 1 矛盾
    have hcontradict : (1 + 1) % 2 = 0 := by norm_num
    rw [hcontradict] at hsum
    linarith
  -- (←) even n → odd (3n + 1)
  intro h
  have hmod : (3 * n + 1) % 2 = ((3 * n) % 2 + 1 % 2) % 2 := by
    rw [Nat.add_mod]
  rw [hmod]
  -- (3n) % 2 = (n % 2 * 3 % 2) % 2
  have h3n_mod : (3 * n) % 2 = (3 % 2 * (n % 2)) % 2 := by
    rw [Nat.mul_mod]
  rw [h3n_mod]
  -- 3 % 2 = 1
  have h3 : 3 % 2 = 1 := by norm_num
  rw [h3]
  rw [h]

$${2n + 1}$$は奇数や奇数ならば偶数でないと比べると結構な手間ですね。

あとがき

いかがでしたでしょうか？
偶数と奇数。
当たり前な数の交互な並びの世界に新しい視点を得ましたでしょうか？

コラッツ予想では 3n + 1 という操作が奇数に対して行われます。
これを行うと奇数は偶数へと変化します。＋１みたいな事です。
奇数だけでなく、偶数に対して行うと奇数になります。これも＋１です。

$$
３倍する必要あるのか？
$$

コラッツは単純に奇数になったら＋１して偶数にすれば収束する！て言ったら「当たり前じゃん！」って言われて終わるのがつまらない。と思ってか？

$$
\text{odd } 3\times \text{odd }n＝\text{odd} \; \implies \; \text{odd } m \times \text{odd }n+1 = \text{even}
$$

3 でなくとも 5,7,9,11, … 奇数倍なら何でも良い？

それでもコラッツ操作で収束するなら、コラッツ予想は真か？
だが、５では発散してしまう例があるらしい。３でないと駄目という問題。

「２」だけで割る操作では弱い（遅い）のか。

いや、それも違うなあ…。この問題って２進数の話だしなあ（笑）
２進数の偶数・奇数は最下位ビットの０，１状態でありこのビットの有無でビットシフトかビット構造膨張改変で膨張し過ぎたら駄目になる。
ビット並びの消したい「１」を適度に膨らませて１→０の連続パターンを得たい。

奇数素数すべて収束可能であるならば、他の奇数合成数も収束可能である。

みたいな命題が証明できたら良いのか？

$$
\forall p \in \text{odd primes},\ \exists k_p\ :\ T^{k_p}(p)=1
$$

偶数・奇数の性質の究極命題か？

初心者から中級レベルな Lean 話でした。

2025/11/12 12:31

D.

#Lean #Lean4 #Mathlib #Mathlib4
#偶数奇数 #形式化証明
#ABC予想 #コラッツ予想
#素数 #素因子 #素因数 #素因数分解
#数学

Appendix

Paperproof

Lean 4.22.0, 4.23.0 で使えてなかったのだけど、4.24.0 になってから動作するようになった。

これを使うと今記事で描いた証明図式を得ることが出来ます。

lakefile.toml

必要なライブラリに以下のように追記して lake update してください。
Lean のバージョンは "v4.24.0" に固定しておきます。rev = "v4.24.0"
これは mathlib に対して行う必要があるっぽい。

[[require]]
name = "mathlib"
scope = "leanprover-community"
git = "https://github.com/leanprover-community/mathlib4"
rev = "v4.24.0"

[[require]]
name = "Paperproof"
git = "https://github.com/Paper-Proof/paperproof.git"
subDir = "lean"
rev = "main"

Lean コード

import Mathlib
import Paperproof

としてライブラリを import してください。
Lean のコードのタブを開いている時に（紙をくしゃくしゃした）アイコン

補題にカーソルを合わせれば、その全容が描画されます。

-- Density version (proven version - replaces not_bad_of_union_bound)
-- 「素数和が ≤ 1」という仮定版（もう使わない）
lemma bad_set_density_bound_pv
    (ε : ℝ) (_hε : 0 < ε)
    (γ_values : ℕ → ℝ) (hγ_values : ∀ p, 0 < γ_values p)
    (hseries : ∀ N, ∑ p ∈ Finset.filter (fun (p : ℕ) => p.Prime ∧ p ≥ 3) (Finset.range (N + 1)),
            ((p : ℕ) : ℝ) ^ (-(Real.log 2 / (2 * Real.log 3)) * (γ_values p + 2)) ≤ 1) :
    ∃ C > 0, ∀ (X : ℕ), X ≥ const_X →
      ((Finset.filter (fun n
        => Bad_ε n γ_values) (Finset.Icc 0 X)).card : ℝ)
        ≤ C * (X : ℝ) := by
-- 以下、長いので省略

少々長めの証明を試してみた

長いと逆に分かりにくいのか？補題は短く簡潔に…か…。