jurupapa https://blog.hatena.ne.jp/jurupapa/ Maxima で綴る数学の旅 https://maxima.hatenablog.jp/ Lean4を証明支援系として使っていても、型と証明の対応や関数型言語が突然現れることがあります。このことを知っていないと証明が読めないことがありました。 具体的には例えばある定理がこんな形だったとします。 def P (x:ℕ) : Prop := sorrytheorem theoA : ∀ x > 3, P x := sorry P xを命題としてxが3より大きい場合はP xが成り立つ、というのがtheoAという定理です。 当然P 4は4>3なので成り立つはずです。証明は普通はこんなふうにやると思うのです。 example : P 4 := by apply theoA -- ⊢ 4 > … 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmaxima.hatenablog.jp%2Fentry%2F2024%2F02%2F19%2F181244" title="-数学- Lean4のお勉強　関数型言語が証明に顔をだす - Maxima で綴る数学の旅" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> https://cdn-ak.f.st-hatena.com/images/fotolife/j/jurupapa/20240219/20240219175747.jpg Hatena Blog https://hatena.blog 2024-02-19 18:12:44 rich https://maxima.hatenablog.jp/entry/2024/02/19/181244 1.0 100%