LEANのチュートリアルを読んだらなんとなく思い出して来た。 Theorem Proving in Lean — Theorem Proving in Lean 3.4.0 documentation tacticとかまだよくわかってないけど、タームモードで処理できるうちはなんとかなりそう。まあ適宜参照しつつ不完全性定…