年末は帰省していたのですが、有休含めて1/8までお休みにしたこともあり時間ができました。そこでLean 4を勉強してみることにしました。 Lean 4は以前このブログで紹介したLean 3と呼ばれる定理証明支援システムの後継システムです。 Lean 4からは関数型プロ…