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 用のバージョンはこちらで入手できます.