Mathematics in Lean4の数論の章の3つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。 証明方法として3つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。 ある自然数nに対して必ずnよりも大きな素数が存在する(作れる)ことを示す。theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by... 素数が有限個しかないとして、それらの積に1を足した数を考えるとその素因数が元の素数の集合に含まれることから矛盾を導く(ユークリッド)。theorem primes…