LEANどうしよう

LEANのチュートリアルを読んだらなんとなく思い出して来た。

Theorem Proving in Lean — Theorem Proving in Lean 3.4.0 documentation

tacticとかまだよくわかってないけど、タームモードで処理できるうちはなんとかなりそう。まあ適宜参照しつつ不完全性定理を証明しよう。
不完全性定理の方は教科書があった方がやりやすいので数学ガールでもみながらやっていく。数学ガールの不完全性定理の証明はなんか追っていけなかった苦い記憶がある。今回はちゃんと追って克服したい。

が、眠い。とにかく眠いので今日のところは退散する。