Reservoir

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

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

10. ❌ Hilbert's third problem: decomposing polyhedra
11. ❌ Lines in the plane and decompositions of graphs
12. ❌ The slope problem
13. ❌ Three applications of Euler's formula
14. ❌ Cauchy's rigidity theorem
15. ❌ The Borromean rings don't exist
16. ❌ Touching simplices
17. ❌ Every large point set has an obtuse angle
18. ❌ Borsuk's conjecture

Analysis

19. ❌ Sets, functions, and the continuum hypothesis
20. 💭 In praise of inequalities
21. 💭 The fundamental theorem of algebra
22. ❌ One square and an odd number of triangles
23. ❌ A theorem of Pólya on polynomials
24. ❌ Van der Waerden's permanent conjecture
25. ❌ On a lemma of Littlewook and Offord
26. ❌ Cotangent and the Herglotz trick
27. ❌ Buffon's needle problem

Combinatorics

28. ❌ Pigeon-hole and double counting
29. ❌ Tiling rectangles
30. ❌ Three famous theorems on finite sets
31. ❌ Shuffling cards
32. 💭 Lattice paths and determinants
33. ❌ Cayley's formula for the number of trees
34. ❌ Identities versus bijections
35. ❌ The finite Kakeya problem
36. ❌ Completing Latin squares

Graph Theory

37. ❌ Permanents and the power of entropy
38. ❌ The Dinitz problem
39. ❌ Five-coloring plane graphs
40. ❌ How to guard a museum
41. ❌ Turán's graph theorem
42. ❌ Communicating without errors
43. ❌ The chromatic number of Kneser graphs
44. 💬 Of friends and politicians
45. 💭 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.