Maxima で綴る数学の旅

紙と鉛筆の代わりに、数式処理システムMaxima / Macsyma を使って、数学を楽しみましょう

2024-04-01から1ヶ月間の記事一覧

-数学- Lean4のお勉強 素数は無限個ある!

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

-Lean4のお勉強 3の倍数の確認法(任意桁版)

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

-Lean4のお勉強 帰納法と再帰

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