Formal BOOK

🚀 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.

Structure

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.

Blueprint

Checkout the project's blueprint!

Installation

This project uses Lean 4. You first need to install elan and lean and then run

shellCopy
lake exe cache get
lake build
code .

The last step only opens vscode in case you want to use that.

Contributing

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 sorry are 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.

Update

To update the mathlib dependency, run the following two commands:
Download the latest lean-toolchain file from the Mathlib4 repository

bashCopy
curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

Update 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

Authors

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.

License

Apache 2.0; see LICENSE for details.