Lean が気になっているので Theorem Proving in Lean 4 の Propositions and Proofs にある演習問題を解いた。プログラムによる定理証明に触れるのは初なので、時々型を定理だと認識できなくなって迷走してしまうなど苦労した。 Lean4 が気になっている理由…