数学の記事では普通は環境について書かないのですが、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章 基本」の最後の練習問題である「距離関数は常にゼロ以上」の証明が終わったところが練習ファイルの160行目から表示されています。
というわけで無事に2章は全て終了しました。ここまで勉強してイマイチわかった気がしていないのはcalcモードです。わかりやすいcalcモードの説明を探しているのですが見つからず、、、calcモードは「3章 論理」でもそれなりに使われるようなので、そこで改めて理解したいと思います。
