Formal BOOK
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
lake exe cache get
lake build
code .
The last step only opens vscode in case you want to use that.
Chapters
Status of the chapters:
- โ chapter is just a stub
- ๐ญ work in progress, formalization of some statements still missing
- ๐ฌ work in progress, all statements formalized, some proofs still missing
- ๐ chapter is completely formalized (possibly excluding the Appendix)
Number Theory
- ๐ฌ Six proofs of the infinity of primes
- ๐ฌ Bertrand's postulate
- ๐ฌ Binomial coefficients are (almost) never powers
- โ Representing numbers as sums of two squares
- ๐ญ The law of quadratic reciprocity
- ๐ญ Every finite division ring is a field
- ๐ญ The spectral theorem and Hadamard's determinant problem
- ๐ญ Some irrational numbers
- โ Four times
Geometry
- โ Hilbert's third problem: decomposing polyhedra
- โ Lines in the plane and decompositions of graphs
- โ The slope problem
- โ Three applications of Euler's formula
- โ Cauchy's rigidity theorem
- โ The Borromean rings don't exist
- โ Touching simplices
- โ Every large point set has an obtuse angle
- โ Borsuk's conjecture
Analysis
- โ Sets, functions, and the continuum hypothesis
- ๐ญ In praise of inequalities
- ๐ญ The fundamental theorem of algebra
- โ One square and an odd number of triangles
- โ A theorem of Pรณlya on polynomials
- โ Van der Waerden's permanent conjecture
- โ On a lemma of Littlewook and Offord
- โ Cotangent and the Herglotz trick
- โ Buffon's needle problem
Combinatorics
- โ Pigeon-hole and double counting
- โ Tiling rectangles
- โ Three famous theorems on finite sets
- โ Shuffling cards
- ๐ญ Lattice paths and determinants
- โ Cayley's formula for the number of trees
- โ Identities versus bijections
- โ The finite Kakeya problem
- โ Completing Latin squares
Graph Theory
- โ Permanents and the power of entropy
- โ The Dinitz problem
- โ Five-coloring plane graphs
- โ How to guard a museum
- โ Turรกn's graph theorem
- โ Communicating without errors
- โ The chromatic number of Kneser graphs
- ๐ฌ Of friends and politicians
- ๐ญ Probability makes counting (sometimes) easy
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
- fill in
sorry
s 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.
Authors
A list of contributors can be found here: AUTHORS or look at the github stats.
License
Apache 2.0; see LICENSE
for details.
Disclaimer
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.