jurupapa https://blog.hatena.ne.jp/jurupapa/ Maxima で綴る数学の旅 https://maxima.hatenablog.jp/ 数学の記事では普通は環境について書かないのですが、Lean4はプログラミング環境でもあるし、一応概要を記しておきます。 パソコン：M1 iMac (主記憶16GB), macOS 14.2.1 Lean (version 4.5.0-rc1) VS Code バージョン1.85.1 VS Code機能拡張Lean4 v0.0.124 起動中のVSCodeの様子はこんな感じです。縦分割の左から、フォルダ階層、Mathematics In Lean、練習ファイル、証明ゴール が表示されています。 MILの「2章 基本」の最後の練習問題である「距離関数は常にゼロ以上」の証明が終わったところが練習ファ… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmaxima.hatenablog.jp%2Fentry%2F2024%2F01%2F24%2F010709" 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/20240121/20240121175955.jpg Hatena Blog https://hatena.blog 2024-01-24 01:07:09 rich https://maxima.hatenablog.jp/entry/2024/01/24/010709 1.0 100%