Lean言語・形式証明系の普及を進めておられる北窓さんが執筆された本： ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 を購入して読み進めています。 扱っている言語はLean4です。Lean4は多くの数学者にも使われ始めているのですが…

Lean4+Mathlib4の組み合わせで証明が出来上がるとレポジトリをGithubで公開したくなります。この時にGithub Actionsを使ってCI (Continuous Integration)を設定しておくと、利用者がレポジトリをダウンロードしてから利用を開始する体験を向上できます。この…