続編の動画が上がっていた。
インストールは手間だから
https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fleanprover-community%2Ftutorials%2Fmaster%2Fsrc%2Fexercises%2F00_first_proofs.lean
このページでweb上で動かしても良いかもしれない。
感想
library_search で検索する。
出なかったら suggest という tactic を使っている。
使えそうな初手の一覧を示すものなのかな。上から順に試せば良いのかな。
import tactic.linarith して linarith という tactic も使っている。中身は良く分からない。
今回は、動画に沿って、自分でも実行できた。
この Lean + mathlib や、 Isabelle もそうだけど、
これからの定理証明は、上位層の場合分けは人の手でおこなって、
下位層は 自動証明tactic を使う、という流れになっていくのかもしれない。
