🚀 Pull Requests Welcome! 🎉
We warmly welcome contributions from everyone. No experience is necessary, and partial proofs help with LaTex are appreciated!
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.
To update the mathlib dependency, run the following two commands: Download the latest lean-toolchain file from the Mathlib4 repository
curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchainUpdate the Mathlib dependencies and ensure doc-gen is also updated
The -Kenv=dev flag ensures that the development environment is updated, including doc-gen
lake -Kenv=dev update
A list of contributors can be found here: AUTHORS or look at the github stats.
Some contributions come the repo FordUniver/thebook.lean, which also has a nice blog on the proofs formalized there.
Apache 2.0; see LICENSE for details.