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.
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.
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)
- 💬 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
- ❌ 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
- ❌ 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
- ❌ 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
- ❌ 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
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
sorrys - suggest improvements to proofs/code golf
- correct typos/formatting/linting
See CONTRIBUTING.md for details.
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.