お久しぶりになってしまいました。
暑い夏の間ちょっと数学系の話題から離れていたこともありこのブログもしばらく放置してしまいました。ぼちぼち復活していきたいと思います。
今回はすこしリハビリも兼ねて最近の私の開発環境の話です。Lean4をM1 iMac, VSCodeで使っています。M1 iMacにOSメジャーアップデートである macOS 15.0 Sequoia が降ってきましたのでそれに合わせて必要なソフトウェアを全て更新してみました。その環境でとりあえず目立った不具合はなくLean4が使えています。
アップデートした開発環境は以下のとおりです。
M1 iMac 16GB + 1TB
VSCode 1.93.1
homebrew 4.3.24-19
elan 3.1.1
Lake version 5.0.0
Lean version 4.11.0
Lean4の勉強は続けつつ、夏の間に購入した数学の本を読んで紹介したり、いくつかこのブログでも活動をしていこうと思います。
