Skip to the content.

Formal BOOK

formalizing "Proofs from THE BOOK" by Martin Aigner and Günter M. Ziegler

Blueprint (web) Dependency Graph Documentation GitHub

Useful links:

Zulip chat for Lean for coordination
Blueprint
Blueprint as pdf
Dependency graph
Doc pages for this repository

FormalBook is maintained by Moritz Firsching. Visit the GitHub repository for more information.