Mathematics in Lean 4で進めてきているLean4の勉強も第4章となり、初等整数論が扱えるところまで来ました。
最初の節では$\sqrt{2}$が無理数であることを示します。とはいってもこの段階で示すことは$\sqrt{2}$が有理数であるとして矛盾を導くことまでです。$\sqrt{2}$が実数の中に存在することまで示すわけではありません。
証明は古代ギリシャから知られているものです。$\sqrt{2}=\frac{m}{n}$となる互いに素な自然数$m,n$が存在するとします。すると
$$m^2=2\,n^2$$
です。ここから$m$が偶数であることがわかります。$m=2\,k$とかけてそれを左辺に代入すると、
$$4\,k^2=2\,n^2$$
従って
$$2\,k^2=n^2$$
となります。ここから$n$が偶数であることがわかります。これは$m,n$が互いに素であることに矛盾します。
Lean4で形式化する際のポイントは「$m,n$は互いに素($m,n$ are coprime)」は$gcd\, n\, m = 1$、「$m$は偶数(m is even)」は$ 2| m $などで表すことができる点です。
証明は以下のように進みます。
上記の言葉による証明で2回「ある自然数の二乗が偶数ならその自然数は偶数」を使いました。これを定理として形式化しておきます。こんな感じです。
theorem even_of_even_sqr {m : N} (h : 2 | m ^ 2) : 2 | m := by ...
証明したい事柄は以下のように形式化できます。
example {m n : N} (coprime_mn : m.Coprime n) : m ^ 2 ≠ 2 * n ^ 2 := by
ここから定理even_of_even_sqrを使いながら上記の証明を書き下せば証明は終了します。
ここで証明した事柄$m^2\neq 2\,n^2$は$2$を素数$p$に置き換えても証明はほとんど変わりません。$p$が素数であることはp.Primeと書けるので、次のように形式化できます。
example {m n p: N} (coprime_mn : m.Coprime n) (prime_p: p.Prime) : m ^ 2 ≠ p * n ^ 2 := by
その中では定理even_of_even_sqrの代わりに次のような定理を使います。
theorem p_of_p_sqr {m p: N}(prime_p: p.Prime) (h : p | m ^ 2) : p | m := by ...
$m^2 \neq p\,n^2$を示すのに素因数分解の一意性を使うこともできます。$m,n\neq 0$として左辺の素因数分解には$p$が偶数回現れるのに対して右辺では$p$は奇数回表れていますから矛盾です。以下にこの証明のために必要な定理の形式化を記載します。
以下でm.factorization pはmを素因数分解した時の素数pが現れる回数を表します。
theorem factorization_mul' {m n : N} (mnez : m ≠ 0) (nnez : n ≠ 0) (p : N) :
(m * n).factorization p = m.factorization p + n.factorization p := by ...
theorem factorization_pow' (n k p : N) :
(n ^ k).factorization p = k * n.factorization p := by ...
theorem Nat.Prime.factorization' {p : N} (prime_p : p.Prime) :
p.factorization p = 1 := by ...
いずれも素因数分解についての基本的な性質です。これらを使いながら両辺に$p$が現れる回数を数え、それらを2で割った余りが等しいとして矛盾を導きます。
証明を埋めるのは余り難しくありませんでした。せっかくなので次回は簡単な定理を自分で形式化して証明してみようと思います。
