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. From the book directory, run lake exe verso-serve
to view it.