This repository contains the source code of the book Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich, with contributions from the Lean Community.

To build the book, change to the book directory and run lake exe tpil. After this, book/_out/html-multi contains a multi-page Web version of the book.