Mathematics in Lean4の数論の章の３つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。
証明方法として３つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。
- ある自然数nに対して必ずnよりも大きな素数が存在する（作れる）ことを示す。
theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by... - 素数が有限個しかないとして、それらの積に1を足した数を考えるとその素因数が元の素数の集合に含まれることから矛盾を導く（ユークリッド）。
theorem primes_infinite' : ∀ s : Finset Nat, ∃ p, Nat.Prime p ∧ p ∉ s := by... - 4n+3型の自然数は必ず4n+3型の素因数を持つという事実と4n+3型の素数が有限個しかないという仮定を置いて矛盾を導く。
theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3 := by...
それぞれの証明では新しい道具が多少使われています。1, 2, 3では有限の総積とその性質が使われています。3では剰余記号%とその性質が使われています。この辺は都度新しい記号や性質が出てきた時に勉強が必要です。具体的にはその記号についてmathlib4ですでにどんな定理が証明されているかを知ることはとても重要です。基本的な性質は大抵定理として証明されていて使える状態にあります。少し例を挙げてみましょう。
有限集合sからその要素の１つbを取り除いた集合erase s bを考えてそこに含まれる要素をaとします。式で書けば h: a ∈ erase s b が成り立っています。ここで
rw [mem_erase] at h
とすればh: a ≠ b ∧ a ∈ sと書き換えられます。このように書き換えればここから等号(=)や集合の要素の関係(∈)、論理記号(∧)などに関して今まで勉強してきたことを使って証明を継続することができます。ちなみにmem_eraseは次のような定理です。
Finset.mem_erase.{u_1} {α : Type u_1} [inst✝ : DecidableEq α] {a b : α} {s : Finset α} :
a ∈ erase s b ↔ a ≠ b ∧ a ∈ simport Mathlib.Data.Finset.Basic
これを見れば同値関係の定理なのでrwタクティクに使えること、またeraseに関する他の定理もMathlib.Data.Finset.Basicにありそう、ということがわかります。
そんなことをしながら無事に数論のセクションも終了しました。
