Theorem Proving in Lean 4

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

This version of the text assumes you’re using Lean 4. See the Setting Up Lean section of the Lean 4 Manual to install Lean. The first version of this book was written for Lean 2, and the Lean 3 version is available here.