数学の記事では普通は環境について書かないのですが、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 …