A collaborative, work-in-progress attempt to formalize Proofs from THE BOOK using Lean4.
For each chapter in the book (we follow the latest, sixth edition), there is a lean source file containing as many formalized definitions, lemmas, theorems and proofs as we can reasonably currently formalize using Lean's mathlib4.
The goal is to make the formalizations of the proofs as close as possible to the proofs in the book, even if a different proof for a theorem might already be present in mathlib or is more suitable for formalization.
We follow the naming conventions and code style of mathlib4.
Checkout the project's blueprint!
This project uses Lean 4. You first need to install elan and lean and then run
lake exe cache get
lake build
code .The last step only opens vscode in case you want to use that.
Contributions are most welcome! Feel free to
- grab a chapter that is not yet formalized and formalize
- definitions, (if not yet in mathlib)
- statements and
- proofs
- partial proofs with new
sorryare also great! - fill in
sorrys in lean files - fill in 'TODO's in LaTeX files in the blueprint
- suggest improvements to proofs/code golf
- correct typos/formatting/linting
See CONTRIBUTING.md for details.
A list of contributors can be found here: AUTHORS or look at the github stats.
Apache 2.0; see LICENSE for details.
This project is not an official Google project. It is not supported by Google and Google specifically disclaims all warranties as to its quality, merchantability, or fitness for a particular purpose.