Mathematics in Lean4の数論の章の３つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。 証明方法として３つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。 ある自然数nに対して…

有限の場合の総和記号について勉強したことで任意桁数の場合の３の倍数の確認方法について形式化して証明することが出来そうです。ということでやってみました。 まず与えられた自然数が３の倍数かどうかの確認方法と普通の証明をざっと述べてみます。 ３の…

Mathmatics In Lean4の第5章 初等数論の２つ目の話題は帰納法と再帰です。自然数では定義が帰納的であること（自然数型は帰納型であること）を知ります。 inductive Nat | zero : Nat | succ (n : Nat) : Nat この意味は、0はNat型、Nat型の要素を１つとって…