Theorem Proving in Lean 4

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

This is a copy of the wonderful Theorem Proving in Lean 4. This copy includes some additional things, such as solutions to exercises, and webpages where you can walk through the proof state in the browser.