内容・動機

Software Foundations vol. 1 Logical Foundationsという著名な本のサンプルコードを、主催である私YAMAMOTO Yujiと喋りながらCoqからLean 4に翻訳して、Lean 4を勉強します。 私はSoftware Foundations vol. 1の大半を読み終え、大雑把に内容を把握しましたが、まだ手を動かせていないので、みなさんからアドバイスを得ながらCoqをLean 4に翻訳することで、定理証明支援系の使い方などを学びたいと考えています。

今回は練習問題: ★★★, standard (list_exercises)の「app_assoc4」から始めます。

参加方法

このイベントに参加登録すると見える「参加者への情報」に、専用のDiscordサーバーへの招待リンクを作成しましたので、そちらからご登録ください。こちらのDiscordサーバーのボイスチャンネルで行う予定です。既にDiscordサーバーに登録済みの方はご登録頂かなくても結構です。

Lean開発環境の準備

「いっしょに進めたい！」という方は https://github.com/leanprover/lean4/blob/master/doc/quickstart.md に書かれている手順に従って、Lean 4のVS Code向け拡張をインストールすると、私と同じ方法でセットアップできるのでお勧めです。