Maxima で綴る数学の旅

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

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

-その他- macOSとbluetooth イヤフォンの現状と音質の改善方法

しばらく前のmacOSではbluetoothイヤフォンで音楽を楽しむ際、コーデック選択の問題で音質が悪い状況がありました。私もiMacとソニーのWF-1000MX4 の組み合わせでこの辺について色々と試してきています。 最近知ったのですが、この状況は少なくともmacOS Son…

-数学- Lean4のお勉強 集合を扱う

Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつ…

-数学- Lean4のお勉強 関数型言語が証明に顔をだす

Lean4を証明支援系として使っていても、型と証明の対応や関数型言語が突然現れることがあります。このことを知っていないと証明が読めないことがありました。 具体的には例えばある定理がこんな形だったとします。 def P (x:ℕ) : Prop := sorrytheorem theoA…

-数学- Lean4のお勉強 論理積∧ と 論理和∨

Lean4での論理記号の取り扱いの勉強も後半です。今回は論理積と論理和の扱いを見ていきます。この辺はあまり難しい話は出てきません。 ゴールが論理積A ∧ Bの形の場合にはconstructorタクティクを使うとAとBが両方ともゴールとなり両方証明するとA ∧ Bの証明…

-数学- Lean4のお勉強 否定

否定が論理式に含まれているとき使えるタクティクを勉強しました。 introタクティク:ゴールがある命題の否定¬ Aである場合、intro hとすると仮定h: Aが導入されて、ゴールがFalse (矛盾)に変わります。仮定の集まりの中で適当な命題Bについてhb:Bとhbn:¬ B…

-数学- Lean4のお勉強 タオ教授のブログより

現役で最高の数学者のお一人で情報発信にも熱心なテレンスタオ教授のブログがあります。 terrytao.wordpress.com 残念ながら難しすぎて普段はほとんど見ない数学ブログですが、Lean4の勉強をしていたら検索で記事が1つヒットしました! A slightly longer L…

-数学- Lean4のお勉強  存在量化子 ∃

ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by us…