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 Quickstart 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.