Theorem Proving in Lean

by Jeremy Avigad, Leonardo de Moura, and Soonho Kong

Describes the Lean Theorem Prover.

167 pages, ebook

Published January 21, 2021

Reviews

[Satyaki · Rating 4 out of 5]

https://lean-lang.org/theorem_proving...

[John · Rating 4 out of 5]

I have read it once, but I do not understand it. I will keep at it until I have a much better grasp of the material. The online version of this book makes excellent use of browser technology to bring up functioning instances of Lean to execute examples. This is a rare example of a book that is best read online. As, it's not traditionally published, you can check it out here:

https://leanprover.github.io/theorem_...