Theorem Proving in Lean 4

by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community

このバージョンのテキストは，Lean 4 を使用していることを前提としています．Lean をインストールするには， Lean 4 マニュアルのセットアップのセクションを参照してください．本書の最初のバージョンは Lean 2 用に書かれていました．Lean 3 用のバージョンはこちらで入手できます．