本の中では J-Bob っていう定理証明支援系を使うように促されるんだけど J-Bob のインターフェースは結構つらかった(ミスがあると全部 `nil` って返ってくる)し、環境構築もなんか大変だった。
少し試してたところ Jupyter Notebook との相性が凄くいい、あとはエラーメッセージを親切にして環境構築をしやすいようにすれば普通に使ってもらえる気がする。
定理証明支援系 Vikalpa のテストコードはこんな感じ:https://git.tojo.tokyo/vikalpa.git/tree/tests/test-vikalpa.scm