Formal BOOK

A collaborative, work-in-progress attempt to formalize Proofs from THE BOOK using Lean4.

Formal Proofs from THE BOOK

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

  1. ๐Ÿ’ฌ Six proofs of the infinity of primes
  2. ๐Ÿ’ฌ Bertrand's postulate
  3. ๐Ÿ’ฌ Binomial coefficients are (almost) never powers
  4. โŒ Representing numbers as sums of two squares
  5. ๐Ÿ’ญ The law of quadratic reciprocity
  6. ๐Ÿ’ญ Every finite division ring is a field
  7. ๐Ÿ’ญ The spectral theorem and Hadamard's determinant problem
  8. ๐Ÿ’ญ Some irrational numbers
  9. โŒ Four times

Geometry

  1. โŒ Hilbert's third problem: decomposing polyhedra
  2. โŒ Lines in the plane and decompositions of graphs
  3. โŒ The slope problem
  4. โŒ Three applications of Euler's formula
  5. โŒ Cauchy's rigidity theorem
  6. โŒ The Borromean rings don't exist
  7. โŒ Touching simplices
  8. โŒ Every large point set has an obtuse angle
  9. โŒ Borsuk's conjecture

Analysis

  1. โŒ Sets, functions, and the continuum hypothesis
  2. ๐Ÿ’ญ In praise of inequalities
  3. ๐Ÿ’ญ The fundamental theorem of algebra
  4. โŒ One square and an odd number of triangles
  5. โŒ A theorem of Pรณlya on polynomials
  6. โŒ Van der Waerden's permanent conjecture
  7. โŒ On a lemma of Littlewook and Offord
  8. โŒ Cotangent and the Herglotz trick
  9. โŒ Buffon's needle problem

Combinatorics

  1. โŒ Pigeon-hole and double counting
  2. โŒ Tiling rectangles
  3. โŒ Three famous theorems on finite sets
  4. โŒ Shuffling cards
  5. ๐Ÿ’ญ Lattice paths and determinants
  6. โŒ Cayley's formula for the number of trees
  7. โŒ Identities versus bijections
  8. โŒ The finite Kakeya problem
  9. โŒ Completing Latin squares

Graph Theory

  1. โŒ Permanents and the power of entropy
  2. โŒ The Dinitz problem
  3. โŒ Five-coloring plane graphs
  4. โŒ How to guard a museum
  5. โŒ Turรกn's graph theorem
  6. โŒ Communicating without errors
  7. โŒ The chromatic number of Kneser graphs
  8. ๐Ÿ’ฌ Of friends and politicians
  9. ๐Ÿ’ญ 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 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.

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.