From d3dc53e36cca085106c592e04d7dddb7db638fa0 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Mon, 15 Apr 2024 18:01:36 +0200
Subject: [PATCH 01/10] bump mathlib

---
 ..._Six_proofs_of_the_infinity_of_primes.lean | 18 +-------
 FormalBook/Ch02_Bertrand's_postulate.lean     |  5 ++-
 ...Ch05_The_law_of_quadratic_reciprocity.lean |  6 +--
 ...Every_finite_division_ring_is_a_field.lean | 42 +++++++------------
 .../Ch44_Of_friends_and_politicians.lean      |  4 +-
 lake-manifest.json                            | 16 +++----
 lean-toolchain                                |  2 +-
 7 files changed, 32 insertions(+), 61 deletions(-)

diff --git a/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean b/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
index 0d0f449..df6dfb7 100644
--- a/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
+++ b/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
@@ -15,23 +15,9 @@ limitations under the License.
 
 Authors: Moritz Firsching
 -/
-import Mathlib.Algebra.BigOperators.Basic
-import Mathlib.Algebra.BigOperators.Order
-import Mathlib.Analysis.SpecialFunctions.Pow.Real
-import Mathlib.Analysis.Asymptotics.Asymptotics
-import Mathlib.Tactic
-import Mathlib.Data.Nat.Prime
-import Mathlib.Data.Nat.Pow
-import Mathlib.Data.ZMod.Basic
-import Mathlib.Data.Nat.Parity
-import Mathlib.FieldTheory.Finite.Basic
-import Mathlib.GroupTheory.OrderOfElement
-import Mathlib.GroupTheory.Coset
 import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.NumberTheory.PrimeCounting
-import Mathlib.Order.Filter.AtTopBot
-import Mathlib.Topology.Instances.ENNReal
-import Mathlib.Topology.Basic
+import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 open Finset Nat
 open BigOperators
@@ -146,8 +132,6 @@ lemma ZMod.two_ne_one (q : ℕ)  [Fact (1 < q)] : (2 : ZMod q) ≠ 1 := by
   intro h1
   have h : (2 - 1 : ZMod q) = 0 := by exact Iff.mpr sub_eq_zero h1
   norm_num at h
-  have := ZMod.one_ne_zero q
-  exact this h
 
 
 theorem infinity_of_primes₃:
diff --git a/FormalBook/Ch02_Bertrand's_postulate.lean b/FormalBook/Ch02_Bertrand's_postulate.lean
index 60988a7..1dca995 100644
--- a/FormalBook/Ch02_Bertrand's_postulate.lean
+++ b/FormalBook/Ch02_Bertrand's_postulate.lean
@@ -125,7 +125,7 @@ theorem centralBinom_factorization_small (n : ℕ) (n_large : 2 < n)
   apply Finset.prod_subset
   · exact Finset.range_subset.2 (add_le_add_right (Nat.div_le_self _ _) _)
   intro x hx h2x
-  rw [Finset.mem_range, lt_succ_iff] at hx h2x
+  rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x
   rw [not_le, div_lt_iff_lt_mul' three_pos, mul_comm x] at h2x
   replace no_prime := not_exists.mp no_prime x
   rw [← and_assoc, not_and', not_and_or, not_lt] at no_prime
@@ -150,7 +150,8 @@ theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_big : 2 < n)
   let f x := x ^ n.centralBinom.factorization x
   have : ∏ x : ℕ in S, f x = ∏ x : ℕ in Finset.range (2 * n / 3 + 1), f x := by
     refine' Finset.prod_filter_of_ne fun p _ h => _
-    contrapose! h; dsimp only
+    contrapose! h
+    dsimp [f]
     rw [factorization_eq_zero_of_non_prime n.centralBinom h, _root_.pow_zero]
   rw [centralBinom_factorization_small n n_big no_prime, ← this, ←
     Finset.prod_filter_mul_prod_filter_not S (· ≤ Nat.sqrt (2 * n))]
diff --git a/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean b/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean
index 2ddf7d2..4952ada 100644
--- a/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean
+++ b/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean
@@ -15,12 +15,8 @@ limitations under the License.
 
 Authors: Moritz Firsching, Nikolas Kuhn
 -/
-import Mathlib.Tactic
+import Mathlib.Algebra.Polynomial.Basic
 import Mathlib.Data.ZMod.Basic
-import Mathlib.Data.Finset.Card
-import Mathlib.Data.Polynomial.Basic
-import Mathlib.Order.LocallyFinite
-
 
 open ZMod Finset
 open Polynomial (X)
diff --git a/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean b/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean
index 7b67e3b..5234661 100644
--- a/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean
+++ b/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean
@@ -15,20 +15,10 @@ limitations under the License.
 
 Authors: Moritz Firsching, Nick Kuhn
 -/
-import Mathlib.Tactic
-import Mathlib.Data.Set.Basic
-import Mathlib.Data.Fintype.Card
-import Mathlib.RingTheory.IntegralDomain
-import Mathlib.RingTheory.Subring.Basic
-import Mathlib.RingTheory.RootsOfUnity.Complex
-import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
-import Mathlib.Data.Polynomial.RingDivision
-import Mathlib.Algebra.Group.Conj
-import Mathlib.LinearAlgebra.FiniteDimensional
-import Mathlib.LinearAlgebra.Basis
-import Mathlib.Data.Polynomial.Basic
-import Mathlib.Data.Complex.Basic
-import Mathlib.GroupTheory.ClassEquation
+import Mathlib.RingTheory.Henselian
+import Mathlib.RingTheory.HopfAlgebra
+import Mathlib.RingTheory.LittleWedderburn
+import Mathlib.Algebra.Lie.OfAssociative
 
 open Finset Subring Polynomial Complex BigOperators Nat
 /-!
@@ -112,8 +102,9 @@ theorem h_lamb_gt_q_sub_one (q n : ℕ) (lamb : ℂ):
   have g := (Real.sqrt_lt_sqrt_iff this).mpr (h_ineq)
   have : Real.sqrt (((q:ℝ) - 1) ^ 2) = ((q : ℝ) - 1) := by sorry
   rw [this] at g
-  simp only [norm_eq_abs, map_nonneg, Real.sqrt_sq] at g
-  exact g
+  rw [norm_eq_abs, Real.sqrt_sq] at g
+  · exact g
+  · aesop
 
 lemma div_of_qpoly_div (k n q : ℕ) (hq : 1 < q) (hk : 0 < k) (hn : 0 < n)
     (H : q ^ k - 1 ∣ q ^ n - 1) : k ∣ n := by
@@ -131,14 +122,14 @@ lemma div_of_qpoly_div (k n q : ℕ) (hq : 1 < q) (hk : 0 < k) (hn : 0 < n)
         calc
           _ < q := hq
           _ = q^1 := (Nat.pow_one q).symm
-          _ ≤ q ^ m := (pow_le_pow_iff hq).mpr hm
+          _ ≤ q ^ m := (pow_le_pow_iff_right hq).mpr hm
       exact Nat.sub_pos_of_lt this
     have : q ^ k - 1 ≤ q ^ m - 1 := Nat.le_of_dvd this H
     have :  q ^ k ≤ q ^ m  := by
       zify at this
       simp at this
       simpa [Nat.sub_add_cancel <| one_le_pow m q hq'] using this
-    exact (pow_le_pow_iff hq).mp this
+    exact (pow_le_pow_iff_right hq).mp this
 
   have : q ^ m - 1 = q^(m - k)*(q ^ k - 1) + (q^(m - k) - 1) := by
     zify
@@ -310,10 +301,8 @@ theorem wedderburn (h: Fintype R): IsField R := by
       intro hs
       apply(Int.dvd_div_of_mul_dvd _)
       have h_one_neq: 1 ≠ n_k A := by
-        dsimp only
         sorry
       have h_k_n_lt_n: n_k A < n := by
-        dsimp only
         sorry
       have h_noneval := phi_div_2 n (n_k A) h_one_neq (h_n_k_A_dvd A) h_k_n_lt_n
       have := @eval_dvd ℤ _ _ _ q h_noneval
@@ -330,14 +319,15 @@ theorem wedderburn (h: Fintype R): IsField R := by
       rw [cast_add] at this
       rw [← this]
       simp [hq_pow_pos n]
-    simp [hq] at h1'
+    --rw [hq] at h1'
+    norm_num at h1'
     simp [h1'] at h₁_dvd
-    rw [← hq] at h₁_dvd
-    exact (Int.dvd_add_left h₂_dvd).mp h₁_dvd
+    refine (Int.dvd_add_left h₂_dvd).mp ?_
+    convert h₁_dvd
 
   by_contra
 
-  have g : map (Int.castRingHom ℂ) (phi n) = ∏ lamb in (primitiveRoots n ℂ), (X - C lamb) := by
+  have g : Polynomial.map (Int.castRingHom ℂ) (phi n) = ∏ lamb in (primitiveRoots n ℂ), (X - C lamb) := by
     dsimp only [phi]
     simp only [map_cyclotomic]
     have := isPrimitiveRoot_exp n h_n
@@ -378,10 +368,10 @@ theorem wedderburn (h: Fintype R): IsField R := by
 
   refine' not_le_of_gt h_gt _
   have : (q - 1 : ℕ) = (q : ℤ) - 1 := by
-    exact Int.coe_pred_of_pos this
+    exact Int.natCast_pred_of_pos this
   rw [← this] at h_norm
   have : Int.natAbs (eval (↑q) (cyclotomic n ℤ)) = |eval (↑q) (phi n)| := by
-    simp only [Int.coe_natAbs]
+    simp only [Int.natCast_natAbs]
     rfl
   rw [← this] at h_norm
   exact_mod_cast h_norm
diff --git a/FormalBook/Ch44_Of_friends_and_politicians.lean b/FormalBook/Ch44_Of_friends_and_politicians.lean
index d7fdf10..f3a7191 100644
--- a/FormalBook/Ch44_Of_friends_and_politicians.lean
+++ b/FormalBook/Ch44_Of_friends_and_politicians.lean
@@ -85,7 +85,7 @@ theorem friendship_theorem [Nonempty V]
           refine' Fintype.one_lt_card_iff.mpr _
           use v
           use x
-        rw [eq₁] at this
+        rw [(show Fintype.card V = n by rfl), eq₁] at this
         tauto
     -- In case k = 2, we have G = K₃
     · norm_num at eq₁
@@ -104,7 +104,7 @@ theorem friendship_theorem [Nonempty V]
           exact fun h => ⟨(G.ne_of_adj h).symm, Finset.mem_univ _⟩
         convert_to 2 ≤ _
         · convert_to _ = Fintype.card V - 1
-          · rw [eq₁]
+          · rw [(show Fintype.card V = n by rfl), eq₁]
           · exact Finset.card_erase_of_mem (Finset.mem_univ _)
         · rw [hregular]
       rw [this]
diff --git a/lake-manifest.json b/lake-manifest.json
index 7d9df30..3f7f1ed 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c",
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3",
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "66439f5ad62664e7dda3c6b6a5fedbfee4112950",
+   "rev": "9125a0936fd86f4bb74bebe27f0b1cd0c5a2b7cf",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index 3f21e50..9ad3040 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.7.0

From c769b0341ad0279a4e61097805e85d317f2586e7 Mon Sep 17 00:00:00 2001
From: Ralf Stephan <ralf@ark.in-berlin.de>
Date: Thu, 18 Apr 2024 19:03:13 +0200
Subject: [PATCH 02/10] add lemma for proof 4 (#50)

---
 .../Ch01_Six_proofs_of_the_infinity_of_primes.lean   | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean b/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
index df6dfb7..a7ddfc7 100644
--- a/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
+++ b/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean
@@ -213,6 +213,18 @@ theorem infinity_of_primes₄ : Tendsto π atTop atTop := by
   -- (2) This implies that it is not bounded
   sorry
 
+-- This might be useful for the proof. Rename as you like.
+lemma H_P4_1 {k p: ℝ} (hk: k > 0) (hp: p ≥ k + 1): p / (p - 1) ≤ (k + 1) / k := by
+  have h_k_nonzero: k ≠ 0 := ne_iff_lt_or_gt.mpr (Or.inr hk)
+  have h_p_pred_pos: p - 1 > 0 := by linarith
+  have h_p_pred_nonzero: p - 1 ≠ 0 := ne_iff_lt_or_gt.mpr (Or.inr h_p_pred_pos)
+  have h₁: p / (p - 1) = 1 + 1 / (p - 1) := by
+    rw [one_add_div h_p_pred_nonzero, sub_add_cancel]
+  rw [← one_add_div h_k_nonzero, h₁, add_le_add_iff_left,
+    one_div_le_one_div h_p_pred_pos hk, @le_sub_iff_add_le]
+  exact hp
+
+
 /-!
 ### Fifth proof
 

From 47ff7fdf836a9c1f82aaeb29a17058484b6a5054 Mon Sep 17 00:00:00 2001
From: Ralf Stephan <ralf@ark.in-berlin.de>
Date: Fri, 19 Apr 2024 10:23:01 +0200
Subject: [PATCH 03/10] fix typo (#48)

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 240997c..a5ea071 100644
--- a/README.md
+++ b/README.md
@@ -39,7 +39,7 @@ Status of the chapters:
   4. :x: [Representing numbers as sums of two squares](./src/chapters/04_Representing_numbers_as_sums_of_two_squares.lean)
   5. :thought_balloon: [The law of quadratic reciprocity](./src/chapters/05_The_law_of_quadratic_reciprocity.lean)
   6. :thought_balloon: [Every finite division ring is a field](./src/chapters/06_Every_finite_division_ring_is_a_field.lean)
-  7. :thought_ballon: [The spectral theorem and Hadamard's determinant problem](./src/chapters/07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
+  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](./src/chapters/07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
   8. :thought_balloon: [Some irrational numbers](./src/chapters/08_Some_irrational_numbers.lean)
   9. :x: [Four times ](./src/chapters/09_Four_times_pi²_over_6.lean)$\pi^2/6$
 

From 863bdae99ef1c77c36c6556fd801604736384eef Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 21 Apr 2024 13:08:26 +0200
Subject: [PATCH 04/10] fix links

---
 README.md | 90 +++++++++++++++++++++++++++----------------------------
 1 file changed, 45 insertions(+), 45 deletions(-)

diff --git a/README.md b/README.md
index a5ea071..8aafbc8 100644
--- a/README.md
+++ b/README.md
@@ -33,56 +33,56 @@ Status of the chapters:
   - :tada: chapter is completely formalized (possibly excluding the Appendix)
 
 ### Number Theory
-  1. :speech_balloon: [Six proofs of the infinity of primes](./src/chapters/01_Six_proofs_of_the_infinity_of_primes.lean)
-  2. :speech_balloon: [Bertrand's postulate](./src/chapters/02_Bertrand's_postulate.lean)
-  3. :speech_balloon: [Binomial coefficients are (almost) never powers](./src/chapters/03_Binomial_coefficients_are_(almost)_never_powers.lean)
-  4. :x: [Representing numbers as sums of two squares](./src/chapters/04_Representing_numbers_as_sums_of_two_squares.lean)
-  5. :thought_balloon: [The law of quadratic reciprocity](./src/chapters/05_The_law_of_quadratic_reciprocity.lean)
-  6. :thought_balloon: [Every finite division ring is a field](./src/chapters/06_Every_finite_division_ring_is_a_field.lean)
-  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](./src/chapters/07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
-  8. :thought_balloon: [Some irrational numbers](./src/chapters/08_Some_irrational_numbers.lean)
-  9. :x: [Four times ](./src/chapters/09_Four_times_pi²_over_6.lean)$\pi^2/6$
+  1. :speech_balloon: [Six proofs of the infinity of primes](./FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
+  2. :speech_balloon: [Bertrand's postulate](./FormalBook/Ch02_Bertrand's_postulate.lean)
+  3. :speech_balloon: [Binomial coefficients are (almost) never powers](./FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
+  4. :x: [Representing numbers as sums of two squares](./FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
+  5. :thought_balloon: [The law of quadratic reciprocity](./FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
+  6. :thought_balloon: [Every finite division ring is a field](./FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
+  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](./FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
+  8. :thought_balloon: [Some irrational numbers](./FormalBook/Ch08_Some_irrational_numbers.lean)
+  9. :x: [Four times ](./FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
 
 ### Geometry
-  10. :x: [Hilbert's third problem: decomposing polyhedra](./src/chapters/10_Hilbert's_third_problem_decomposing_polyhedra.lean)
-  11. :x: [Lines in the plane and decompositions of graphs](./src/chapters/11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
-  12. :x: [The slope problem](./src/chapters/12_The_slope_problem.lean)
-  13. :x: [Three applications of Euler's formula](./src/chapters/13_Three_applications_of_Euler's_formula.lean)
-  14. :x: [Cauchy's rigidity theorem](./src/chapters/14_Cauchy's_rigidity_theorem.lean)
-  15. :x: [The Borromean rings don't exist](./src/chapters/15_The_Borromean_rings_don't_exist.lean)
-  16. :x: [Touching simplices](./src/chapters/16_Touching_simplices.lean)
-  17. :x: [Every large point set has an obtuse angle](./src/chapters/17_Every_large_point_set_has_an_obtuse_angle.lean)
-  18. :x: [Borsuk's conjecture](./src/chapters/18_Borsuk's_conjecture.lean)
+  10. :x: [Hilbert's third problem: decomposing polyhedra](./FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
+  11. :x: [Lines in the plane and decompositions of graphs](./FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
+  12. :x: [The slope problem](./FormalBook/Ch12_The_slope_problem.lean)
+  13. :x: [Three applications of Euler's formula](./FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
+  14. :x: [Cauchy's rigidity theorem](./FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
+  15. :x: [The Borromean rings don't exist](./FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
+  16. :x: [Touching simplices](./FormalBook/Ch16_Touching_simplices.lean)
+  17. :x: [Every large point set has an obtuse angle](./FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
+  18. :x: [Borsuk's conjecture](./FormalBook/Ch18_Borsuk's_conjecture.lean)
 ### Analysis
-  19. :x: [Sets, functions, and the continuum hypothesis](./src/chapters/19_Sets,_functions,_and_the_continuum_hypothesis.lean)
-  20. :thought_balloon: [In praise of inequalities](./src/chapters/20_In_praise_of_inequalities.lean)
-  21. :thought_balloon: [The fundamental theorem of algebra](./src/chapters/21_The_fundamental_theorem_of_algebra.lean)
-  22. :x: [One square and an odd number of triangles](./src/chapters/22_One_square_and_an_odd_number_of_triangles.lean)
-  23. :x: [A theorem of Pólya on polynomials](./src/chapters/23_A_theorem_of_Pólya_on_polynomials.lean)
-  24. :x: [Van der Waerden's permanent conjecture](./src/chapters/24_Van_der_Waerden's_permanent_conjecture.lean)
-  25. :x: [On a lemma of Littlewook and Offord](./src/chapters/25_On_a_lemma_of_Littlewook_and_Offord.lean)
-  26. :x: [Cotangent and the Herglotz trick](./src/chapters/26_Cotangent_and_the_Herglotz_trick.lean)
-  27. :x: [Buffon's needle problem](./src/chapters/27_Buffon's_needle_problem.lean)
+  19. :x: [Sets, functions, and the continuum hypothesis](./FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
+  20. :thought_balloon: [In praise of inequalities](./FormalBook/Ch20_In_praise_of_inequalities.lean)
+  21. :thought_balloon: [The fundamental theorem of algebra](./FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
+  22. :x: [One square and an odd number of triangles](./FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
+  23. :x: [A theorem of Pólya on polynomials](./FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
+  24. :x: [Van der Waerden's permanent conjecture](./FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
+  25. :x: [On a lemma of Littlewook and Offord](./FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
+  26. :x: [Cotangent and the Herglotz trick](./FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
+  27. :x: [Buffon's needle problem](./FormalBook/Ch27_Buffon's_needle_problem.lean)
 ### Combinatorics
-  28. :x: [Pigeon-hole and double counting](./src/chapters/28_Pigeon-hole_and_double_counting.lean)
-  29. :x: [Tiling rectangles](./src/chapters/29_Tiling_rectangles.lean)
-  30. :x: [Three famous theorems on finite sets](./src/chapters/30_Three_famous_theorems_on_finite_sets.lean)
-  31. :x: [Shuffling cards](./src/chapters/31_Shuffling_cards.lean)
-  32. :thought_balloon: [Lattice paths and determinants](./src/chapters/32_Lattice_paths_and_determinants.lean)
-  33. :x: [Cayley's formula for the number of trees](./src/chapters/33_Cayley's_formula_for_the_number_of_trees.lean)
-  34. :x: [Identities versus bijections](./src/chapters/34_Identities_versus_bijections.lean)
-  35. :x: [The finite Kakeya problem](./src/chapters/35_The_finite_Kakeya_problem.lean)
-  36. :x: [Completing Latin squares](./src/chapters/36_Completing_Latin_squares.lean)
+  28. :x: [Pigeon-hole and double counting](./FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
+  29. :x: [Tiling rectangles](./FormalBook/Ch29_Tiling_rectangles.lean)
+  30. :x: [Three famous theorems on finite sets](./FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
+  31. :x: [Shuffling cards](./FormalBook/Ch31_Shuffling_cards.lean)
+  32. :thought_balloon: [Lattice paths and determinants](./FormalBook/Ch32_Lattice_paths_and_determinants.lean)
+  33. :x: [Cayley's formula for the number of trees](./FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
+  34. :x: [Identities versus bijections](./FormalBook/Ch34_Identities_versus_bijections.lean)
+  35. :x: [The finite Kakeya problem](./FormalBook/Ch35_The_finite_Kakeya_problem.lean)
+  36. :x: [Completing Latin squares](./FormalBook/Ch36_Completing_Latin_squares.lean)
 ### Graph Theory
-  37. :x: [Permanents and the power of entropy](./src/chapters/37_Permanents_and_the_power_of_entropy.lean)
-  38. :x: [The Dinitz problem](./src/chapters/38_The_Dinitz_problem.lean)
-  39. :x: [Five-coloring plane graphs](./src/chapters/39_Five-coloring_plane_graphs.lean)
-  40. :x: [How to guard a museum](./src/chapters/40_How_to_guard_a_museum.lean)
-  41. :x: [Turán's graph theorem](./src/chapters/41_Turán's_graph_theorem.lean)
-  42. :x: [Communicating without errors](./src/chapters/42_Communicating_without_errors.lean)
-  43. :x: [The chromatic number of Kneser graphs](./src/chapters/43_The_chromatic_number_of_Kneser_graphs.lean)
-  44. :speech_balloon: [Of friends and politicians](./src/chapters/44_Of_friends_and_politicians.lean)
-  45. :thought_balloon: [Probability makes counting (sometimes) easy](./src/chapters/45_Probability_makes_counting_(sometimes)_easy.lean)
+  37. :x: [Permanents and the power of entropy](./FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
+  38. :x: [The Dinitz problem](./FormalBook/Ch38_The_Dinitz_problem.lean)
+  39. :x: [Five-coloring plane graphs](./FormalBook/Ch39_Five-coloring_plane_graphs.lean)
+  40. :x: [How to guard a museum](./FormalBook/Ch40_How_to_guard_a_museum.lean)
+  41. :x: [Turán's graph theorem](./FormalBook/Ch41_Turán's_graph_theorem.lean)
+  42. :x: [Communicating without errors](./FormalBook/Ch42_Communicating_without_errors.lean)
+  43. :x: [The chromatic number of Kneser graphs](./FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
+  44. :speech_balloon: [Of friends and politicians](./FormalBook/Ch44_Of_friends_and_politicians.lean)
+  45. :thought_balloon: [Probability makes counting (sometimes) easy](./FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
 
 ## Contributing
 

From 571d36fe22a31d2aee6b59986d4991e86d396306 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 21 Apr 2024 13:11:15 +0200
Subject: [PATCH 05/10] fix links

---
 README.md | 90 +++++++++++++++++++++++++++----------------------------
 1 file changed, 45 insertions(+), 45 deletions(-)

diff --git a/README.md b/README.md
index 8aafbc8..df66023 100644
--- a/README.md
+++ b/README.md
@@ -33,56 +33,56 @@ Status of the chapters:
   - :tada: chapter is completely formalized (possibly excluding the Appendix)
 
 ### Number Theory
-  1. :speech_balloon: [Six proofs of the infinity of primes](./FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
-  2. :speech_balloon: [Bertrand's postulate](./FormalBook/Ch02_Bertrand's_postulate.lean)
-  3. :speech_balloon: [Binomial coefficients are (almost) never powers](./FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
-  4. :x: [Representing numbers as sums of two squares](./FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
-  5. :thought_balloon: [The law of quadratic reciprocity](./FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
-  6. :thought_balloon: [Every finite division ring is a field](./FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
-  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](./FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
-  8. :thought_balloon: [Some irrational numbers](./FormalBook/Ch08_Some_irrational_numbers.lean)
-  9. :x: [Four times ](./FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
+  1. :speech_balloon: [Six proofs of the infinity of primes](FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
+  2. :speech_balloon: [Bertrand's postulate](FormalBook/Ch02_Bertrand's_postulate.lean)
+  3. :speech_balloon: [Binomial coefficients are (almost) never powers](FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
+  4. :x: [Representing numbers as sums of two squares](FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
+  5. :thought_balloon: [The law of quadratic reciprocity](FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
+  6. :thought_balloon: [Every finite division ring is a field](FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
+  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
+  8. :thought_balloon: [Some irrational numbers](FormalBook/Ch08_Some_irrational_numbers.lean)
+  9. :x: [Four times ](FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
 
 ### Geometry
-  10. :x: [Hilbert's third problem: decomposing polyhedra](./FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
-  11. :x: [Lines in the plane and decompositions of graphs](./FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
-  12. :x: [The slope problem](./FormalBook/Ch12_The_slope_problem.lean)
-  13. :x: [Three applications of Euler's formula](./FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
-  14. :x: [Cauchy's rigidity theorem](./FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
-  15. :x: [The Borromean rings don't exist](./FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
-  16. :x: [Touching simplices](./FormalBook/Ch16_Touching_simplices.lean)
-  17. :x: [Every large point set has an obtuse angle](./FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
-  18. :x: [Borsuk's conjecture](./FormalBook/Ch18_Borsuk's_conjecture.lean)
+  10. :x: [Hilbert's third problem: decomposing polyhedra](FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
+  11. :x: [Lines in the plane and decompositions of graphs](FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
+  12. :x: [The slope problem](FormalBook/Ch12_The_slope_problem.lean)
+  13. :x: [Three applications of Euler's formula](FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
+  14. :x: [Cauchy's rigidity theorem](FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
+  15. :x: [The Borromean rings don't exist](FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
+  16. :x: [Touching simplices](FormalBook/Ch16_Touching_simplices.lean)
+  17. :x: [Every large point set has an obtuse angle](FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
+  18. :x: [Borsuk's conjecture](FormalBook/Ch18_Borsuk's_conjecture.lean)
 ### Analysis
-  19. :x: [Sets, functions, and the continuum hypothesis](./FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
-  20. :thought_balloon: [In praise of inequalities](./FormalBook/Ch20_In_praise_of_inequalities.lean)
-  21. :thought_balloon: [The fundamental theorem of algebra](./FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
-  22. :x: [One square and an odd number of triangles](./FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
-  23. :x: [A theorem of Pólya on polynomials](./FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
-  24. :x: [Van der Waerden's permanent conjecture](./FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
-  25. :x: [On a lemma of Littlewook and Offord](./FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
-  26. :x: [Cotangent and the Herglotz trick](./FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
-  27. :x: [Buffon's needle problem](./FormalBook/Ch27_Buffon's_needle_problem.lean)
+  19. :x: [Sets, functions, and the continuum hypothesis](FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
+  20. :thought_balloon: [In praise of inequalities](FormalBook/Ch20_In_praise_of_inequalities.lean)
+  21. :thought_balloon: [The fundamental theorem of algebra](FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
+  22. :x: [One square and an odd number of triangles](FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
+  23. :x: [A theorem of Pólya on polynomials](FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
+  24. :x: [Van der Waerden's permanent conjecture](FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
+  25. :x: [On a lemma of Littlewook and Offord](FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
+  26. :x: [Cotangent and the Herglotz trick](FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
+  27. :x: [Buffon's needle problem](FormalBook/Ch27_Buffon's_needle_problem.lean)
 ### Combinatorics
-  28. :x: [Pigeon-hole and double counting](./FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
-  29. :x: [Tiling rectangles](./FormalBook/Ch29_Tiling_rectangles.lean)
-  30. :x: [Three famous theorems on finite sets](./FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
-  31. :x: [Shuffling cards](./FormalBook/Ch31_Shuffling_cards.lean)
-  32. :thought_balloon: [Lattice paths and determinants](./FormalBook/Ch32_Lattice_paths_and_determinants.lean)
-  33. :x: [Cayley's formula for the number of trees](./FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
-  34. :x: [Identities versus bijections](./FormalBook/Ch34_Identities_versus_bijections.lean)
-  35. :x: [The finite Kakeya problem](./FormalBook/Ch35_The_finite_Kakeya_problem.lean)
-  36. :x: [Completing Latin squares](./FormalBook/Ch36_Completing_Latin_squares.lean)
+  28. :x: [Pigeon-hole and double counting](FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
+  29. :x: [Tiling rectangles](FormalBook/Ch29_Tiling_rectangles.lean)
+  30. :x: [Three famous theorems on finite sets](FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
+  31. :x: [Shuffling cards](FormalBook/Ch31_Shuffling_cards.lean)
+  32. :thought_balloon: [Lattice paths and determinants](FormalBook/Ch32_Lattice_paths_and_determinants.lean)
+  33. :x: [Cayley's formula for the number of trees](FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
+  34. :x: [Identities versus bijections](FormalBook/Ch34_Identities_versus_bijections.lean)
+  35. :x: [The finite Kakeya problem](FormalBook/Ch35_The_finite_Kakeya_problem.lean)
+  36. :x: [Completing Latin squares](FormalBook/Ch36_Completing_Latin_squares.lean)
 ### Graph Theory
-  37. :x: [Permanents and the power of entropy](./FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
-  38. :x: [The Dinitz problem](./FormalBook/Ch38_The_Dinitz_problem.lean)
-  39. :x: [Five-coloring plane graphs](./FormalBook/Ch39_Five-coloring_plane_graphs.lean)
-  40. :x: [How to guard a museum](./FormalBook/Ch40_How_to_guard_a_museum.lean)
-  41. :x: [Turán's graph theorem](./FormalBook/Ch41_Turán's_graph_theorem.lean)
-  42. :x: [Communicating without errors](./FormalBook/Ch42_Communicating_without_errors.lean)
-  43. :x: [The chromatic number of Kneser graphs](./FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
-  44. :speech_balloon: [Of friends and politicians](./FormalBook/Ch44_Of_friends_and_politicians.lean)
-  45. :thought_balloon: [Probability makes counting (sometimes) easy](./FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
+  37. :x: [Permanents and the power of entropy](FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
+  38. :x: [The Dinitz problem](FormalBook/Ch38_The_Dinitz_problem.lean)
+  39. :x: [Five-coloring plane graphs](FormalBook/Ch39_Five-coloring_plane_graphs.lean)
+  40. :x: [How to guard a museum](FormalBook/Ch40_How_to_guard_a_museum.lean)
+  41. :x: [Turán's graph theorem](FormalBook/Ch41_Turán's_graph_theorem.lean)
+  42. :x: [Communicating without errors](FormalBook/Ch42_Communicating_without_errors.lean)
+  43. :x: [The chromatic number of Kneser graphs](FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
+  44. :speech_balloon: [Of friends and politicians](FormalBook/Ch44_Of_friends_and_politicians.lean)
+  45. :thought_balloon: [Probability makes counting (sometimes) easy](FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
 
 ## Contributing
 

From e54e58541fc395483d06e5755f739c21171023b9 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 21 Apr 2024 13:15:21 +0200
Subject: [PATCH 06/10] fix links

---
 README.md | 90 +++++++++++++++++++++++++++----------------------------
 1 file changed, 45 insertions(+), 45 deletions(-)

diff --git a/README.md b/README.md
index df66023..77dde2c 100644
--- a/README.md
+++ b/README.md
@@ -33,56 +33,56 @@ Status of the chapters:
   - :tada: chapter is completely formalized (possibly excluding the Appendix)
 
 ### Number Theory
-  1. :speech_balloon: [Six proofs of the infinity of primes](FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
-  2. :speech_balloon: [Bertrand's postulate](FormalBook/Ch02_Bertrand's_postulate.lean)
-  3. :speech_balloon: [Binomial coefficients are (almost) never powers](FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
-  4. :x: [Representing numbers as sums of two squares](FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
-  5. :thought_balloon: [The law of quadratic reciprocity](FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
-  6. :thought_balloon: [Every finite division ring is a field](FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
-  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
-  8. :thought_balloon: [Some irrational numbers](FormalBook/Ch08_Some_irrational_numbers.lean)
-  9. :x: [Four times ](FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
+  1. :speech_balloon: [Six proofs of the infinity of primes](/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
+  2. :speech_balloon: [Bertrand's postulate](/FormalBook/Ch02_Bertrand's_postulate.lean)
+  3. :speech_balloon: [Binomial coefficients are (almost) never powers](/FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
+  4. :x: [Representing numbers as sums of two squares](/FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
+  5. :thought_balloon: [The law of quadratic reciprocity](/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
+  6. :thought_balloon: [Every finite division ring is a field](/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
+  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](/FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
+  8. :thought_balloon: [Some irrational numbers](/FormalBook/Ch08_Some_irrational_numbers.lean)
+  9. :x: [Four times ](/FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
 
 ### Geometry
-  10. :x: [Hilbert's third problem: decomposing polyhedra](FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
-  11. :x: [Lines in the plane and decompositions of graphs](FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
-  12. :x: [The slope problem](FormalBook/Ch12_The_slope_problem.lean)
-  13. :x: [Three applications of Euler's formula](FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
-  14. :x: [Cauchy's rigidity theorem](FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
-  15. :x: [The Borromean rings don't exist](FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
-  16. :x: [Touching simplices](FormalBook/Ch16_Touching_simplices.lean)
-  17. :x: [Every large point set has an obtuse angle](FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
-  18. :x: [Borsuk's conjecture](FormalBook/Ch18_Borsuk's_conjecture.lean)
+  10. :x: [Hilbert's third problem: decomposing polyhedra](/FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
+  11. :x: [Lines in the plane and decompositions of graphs](/FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
+  12. :x: [The slope problem](/FormalBook/Ch12_The_slope_problem.lean)
+  13. :x: [Three applications of Euler's formula](/FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
+  14. :x: [Cauchy's rigidity theorem](/FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
+  15. :x: [The Borromean rings don't exist](/FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
+  16. :x: [Touching simplices](/FormalBook/Ch16_Touching_simplices.lean)
+  17. :x: [Every large point set has an obtuse angle](/FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
+  18. :x: [Borsuk's conjecture](/FormalBook/Ch18_Borsuk's_conjecture.lean)
 ### Analysis
-  19. :x: [Sets, functions, and the continuum hypothesis](FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
-  20. :thought_balloon: [In praise of inequalities](FormalBook/Ch20_In_praise_of_inequalities.lean)
-  21. :thought_balloon: [The fundamental theorem of algebra](FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
-  22. :x: [One square and an odd number of triangles](FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
-  23. :x: [A theorem of Pólya on polynomials](FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
-  24. :x: [Van der Waerden's permanent conjecture](FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
-  25. :x: [On a lemma of Littlewook and Offord](FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
-  26. :x: [Cotangent and the Herglotz trick](FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
-  27. :x: [Buffon's needle problem](FormalBook/Ch27_Buffon's_needle_problem.lean)
+  19. :x: [Sets, functions, and the continuum hypothesis](/FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
+  20. :thought_balloon: [In praise of inequalities](/FormalBook/Ch20_In_praise_of_inequalities.lean)
+  21. :thought_balloon: [The fundamental theorem of algebra](/FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
+  22. :x: [One square and an odd number of triangles](/FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
+  23. :x: [A theorem of Pólya on polynomials](/FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
+  24. :x: [Van der Waerden's permanent conjecture](/FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
+  25. :x: [On a lemma of Littlewook and Offord](/FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
+  26. :x: [Cotangent and the Herglotz trick](/FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
+  27. :x: [Buffon's needle problem](/FormalBook/Ch27_Buffon's_needle_problem.lean)
 ### Combinatorics
-  28. :x: [Pigeon-hole and double counting](FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
-  29. :x: [Tiling rectangles](FormalBook/Ch29_Tiling_rectangles.lean)
-  30. :x: [Three famous theorems on finite sets](FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
-  31. :x: [Shuffling cards](FormalBook/Ch31_Shuffling_cards.lean)
-  32. :thought_balloon: [Lattice paths and determinants](FormalBook/Ch32_Lattice_paths_and_determinants.lean)
-  33. :x: [Cayley's formula for the number of trees](FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
-  34. :x: [Identities versus bijections](FormalBook/Ch34_Identities_versus_bijections.lean)
-  35. :x: [The finite Kakeya problem](FormalBook/Ch35_The_finite_Kakeya_problem.lean)
-  36. :x: [Completing Latin squares](FormalBook/Ch36_Completing_Latin_squares.lean)
+  28. :x: [Pigeon-hole and double counting](/FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
+  29. :x: [Tiling rectangles](/FormalBook/Ch29_Tiling_rectangles.lean)
+  30. :x: [Three famous theorems on finite sets](/FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
+  31. :x: [Shuffling cards](/FormalBook/Ch31_Shuffling_cards.lean)
+  32. :thought_balloon: [Lattice paths and determinants](/FormalBook/Ch32_Lattice_paths_and_determinants.lean)
+  33. :x: [Cayley's formula for the number of trees](/FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
+  34. :x: [Identities versus bijections](/FormalBook/Ch34_Identities_versus_bijections.lean)
+  35. :x: [The finite Kakeya problem](/FormalBook/Ch35_The_finite_Kakeya_problem.lean)
+  36. :x: [Completing Latin squares](/FormalBook/Ch36_Completing_Latin_squares.lean)
 ### Graph Theory
-  37. :x: [Permanents and the power of entropy](FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
-  38. :x: [The Dinitz problem](FormalBook/Ch38_The_Dinitz_problem.lean)
-  39. :x: [Five-coloring plane graphs](FormalBook/Ch39_Five-coloring_plane_graphs.lean)
-  40. :x: [How to guard a museum](FormalBook/Ch40_How_to_guard_a_museum.lean)
-  41. :x: [Turán's graph theorem](FormalBook/Ch41_Turán's_graph_theorem.lean)
-  42. :x: [Communicating without errors](FormalBook/Ch42_Communicating_without_errors.lean)
-  43. :x: [The chromatic number of Kneser graphs](FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
-  44. :speech_balloon: [Of friends and politicians](FormalBook/Ch44_Of_friends_and_politicians.lean)
-  45. :thought_balloon: [Probability makes counting (sometimes) easy](FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
+  37. :x: [Permanents and the power of entropy](/FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
+  38. :x: [The Dinitz problem](/FormalBook/Ch38_The_Dinitz_problem.lean)
+  39. :x: [Five-coloring plane graphs](/FormalBook/Ch39_Five-coloring_plane_graphs.lean)
+  40. :x: [How to guard a museum](/FormalBook/Ch40_How_to_guard_a_museum.lean)
+  41. :x: [Turán's graph theorem](/FormalBook/Ch41_Turán's_graph_theorem.lean)
+  42. :x: [Communicating without errors](/FormalBook/Ch42_Communicating_without_errors.lean)
+  43. :x: [The chromatic number of Kneser graphs](/FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
+  44. :speech_balloon: [Of friends and politicians](/FormalBook/Ch44_Of_friends_and_politicians.lean)
+  45. :thought_balloon: [Probability makes counting (sometimes) easy](/FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
 
 ## Contributing
 

From 38a797a3c937eb011da5b87aa6c118e892ccafb0 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 21 Apr 2024 13:18:17 +0200
Subject: [PATCH 07/10] fix links

---
 README.md | 90 +++++++++++++++++++++++++++----------------------------
 1 file changed, 45 insertions(+), 45 deletions(-)

diff --git a/README.md b/README.md
index 77dde2c..90676df 100644
--- a/README.md
+++ b/README.md
@@ -33,56 +33,56 @@ Status of the chapters:
   - :tada: chapter is completely formalized (possibly excluding the Appendix)
 
 ### Number Theory
-  1. :speech_balloon: [Six proofs of the infinity of primes](/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
-  2. :speech_balloon: [Bertrand's postulate](/FormalBook/Ch02_Bertrand's_postulate.lean)
-  3. :speech_balloon: [Binomial coefficients are (almost) never powers](/FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
-  4. :x: [Representing numbers as sums of two squares](/FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
-  5. :thought_balloon: [The law of quadratic reciprocity](/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
-  6. :thought_balloon: [Every finite division ring is a field](/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
-  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](/FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
-  8. :thought_balloon: [Some irrational numbers](/FormalBook/Ch08_Some_irrational_numbers.lean)
-  9. :x: [Four times ](/FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
+  1. :speech_balloon: [Six proofs of the infinity of primes](formal_book/blob/main/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
+  2. :speech_balloon: [Bertrand's postulate](formal_book/blob/main/FormalBook/Ch02_Bertrand's_postulate.lean)
+  3. :speech_balloon: [Binomial coefficients are (almost) never powers](formal_book/blob/main/FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
+  4. :x: [Representing numbers as sums of two squares](formal_book/blob/main/FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
+  5. :thought_balloon: [The law of quadratic reciprocity](formal_book/blob/main/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
+  6. :thought_balloon: [Every finite division ring is a field](formal_book/blob/main/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
+  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](formal_book/blob/main/FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
+  8. :thought_balloon: [Some irrational numbers](formal_book/blob/main/FormalBook/Ch08_Some_irrational_numbers.lean)
+  9. :x: [Four times ](formal_book/blob/main/FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
 
 ### Geometry
-  10. :x: [Hilbert's third problem: decomposing polyhedra](/FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
-  11. :x: [Lines in the plane and decompositions of graphs](/FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
-  12. :x: [The slope problem](/FormalBook/Ch12_The_slope_problem.lean)
-  13. :x: [Three applications of Euler's formula](/FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
-  14. :x: [Cauchy's rigidity theorem](/FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
-  15. :x: [The Borromean rings don't exist](/FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
-  16. :x: [Touching simplices](/FormalBook/Ch16_Touching_simplices.lean)
-  17. :x: [Every large point set has an obtuse angle](/FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
-  18. :x: [Borsuk's conjecture](/FormalBook/Ch18_Borsuk's_conjecture.lean)
+  10. :x: [Hilbert's third problem: decomposing polyhedra](formal_book/blob/main/FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
+  11. :x: [Lines in the plane and decompositions of graphs](formal_book/blob/main/FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
+  12. :x: [The slope problem](formal_book/blob/main/FormalBook/Ch12_The_slope_problem.lean)
+  13. :x: [Three applications of Euler's formula](formal_book/blob/main/FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
+  14. :x: [Cauchy's rigidity theorem](formal_book/blob/main/FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
+  15. :x: [The Borromean rings don't exist](formal_book/blob/main/FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
+  16. :x: [Touching simplices](formal_book/blob/main/FormalBook/Ch16_Touching_simplices.lean)
+  17. :x: [Every large point set has an obtuse angle](formal_book/blob/main/FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
+  18. :x: [Borsuk's conjecture](formal_book/blob/main/FormalBook/Ch18_Borsuk's_conjecture.lean)
 ### Analysis
-  19. :x: [Sets, functions, and the continuum hypothesis](/FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
-  20. :thought_balloon: [In praise of inequalities](/FormalBook/Ch20_In_praise_of_inequalities.lean)
-  21. :thought_balloon: [The fundamental theorem of algebra](/FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
-  22. :x: [One square and an odd number of triangles](/FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
-  23. :x: [A theorem of Pólya on polynomials](/FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
-  24. :x: [Van der Waerden's permanent conjecture](/FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
-  25. :x: [On a lemma of Littlewook and Offord](/FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
-  26. :x: [Cotangent and the Herglotz trick](/FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
-  27. :x: [Buffon's needle problem](/FormalBook/Ch27_Buffon's_needle_problem.lean)
+  19. :x: [Sets, functions, and the continuum hypothesis](formal_book/blob/main/FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
+  20. :thought_balloon: [In praise of inequalities](formal_book/blob/main/FormalBook/Ch20_In_praise_of_inequalities.lean)
+  21. :thought_balloon: [The fundamental theorem of algebra](formal_book/blob/main/FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
+  22. :x: [One square and an odd number of triangles](formal_book/blob/main/FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
+  23. :x: [A theorem of Pólya on polynomials](formal_book/blob/main/FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
+  24. :x: [Van der Waerden's permanent conjecture](formal_book/blob/main/FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
+  25. :x: [On a lemma of Littlewook and Offord](formal_book/blob/main/FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
+  26. :x: [Cotangent and the Herglotz trick](formal_book/blob/main/FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
+  27. :x: [Buffon's needle problem](formal_book/blob/main/FormalBook/Ch27_Buffon's_needle_problem.lean)
 ### Combinatorics
-  28. :x: [Pigeon-hole and double counting](/FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
-  29. :x: [Tiling rectangles](/FormalBook/Ch29_Tiling_rectangles.lean)
-  30. :x: [Three famous theorems on finite sets](/FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
-  31. :x: [Shuffling cards](/FormalBook/Ch31_Shuffling_cards.lean)
-  32. :thought_balloon: [Lattice paths and determinants](/FormalBook/Ch32_Lattice_paths_and_determinants.lean)
-  33. :x: [Cayley's formula for the number of trees](/FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
-  34. :x: [Identities versus bijections](/FormalBook/Ch34_Identities_versus_bijections.lean)
-  35. :x: [The finite Kakeya problem](/FormalBook/Ch35_The_finite_Kakeya_problem.lean)
-  36. :x: [Completing Latin squares](/FormalBook/Ch36_Completing_Latin_squares.lean)
+  28. :x: [Pigeon-hole and double counting](formal_book/blob/main/FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
+  29. :x: [Tiling rectangles](formal_book/blob/main/FormalBook/Ch29_Tiling_rectangles.lean)
+  30. :x: [Three famous theorems on finite sets](formal_book/blob/main/FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
+  31. :x: [Shuffling cards](formal_book/blob/main/FormalBook/Ch31_Shuffling_cards.lean)
+  32. :thought_balloon: [Lattice paths and determinants](formal_book/blob/main/FormalBook/Ch32_Lattice_paths_and_determinants.lean)
+  33. :x: [Cayley's formula for the number of trees](formal_book/blob/main/FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
+  34. :x: [Identities versus bijections](formal_book/blob/main/FormalBook/Ch34_Identities_versus_bijections.lean)
+  35. :x: [The finite Kakeya problem](formal_book/blob/main/FormalBook/Ch35_The_finite_Kakeya_problem.lean)
+  36. :x: [Completing Latin squares](formal_book/blob/main/FormalBook/Ch36_Completing_Latin_squares.lean)
 ### Graph Theory
-  37. :x: [Permanents and the power of entropy](/FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
-  38. :x: [The Dinitz problem](/FormalBook/Ch38_The_Dinitz_problem.lean)
-  39. :x: [Five-coloring plane graphs](/FormalBook/Ch39_Five-coloring_plane_graphs.lean)
-  40. :x: [How to guard a museum](/FormalBook/Ch40_How_to_guard_a_museum.lean)
-  41. :x: [Turán's graph theorem](/FormalBook/Ch41_Turán's_graph_theorem.lean)
-  42. :x: [Communicating without errors](/FormalBook/Ch42_Communicating_without_errors.lean)
-  43. :x: [The chromatic number of Kneser graphs](/FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
-  44. :speech_balloon: [Of friends and politicians](/FormalBook/Ch44_Of_friends_and_politicians.lean)
-  45. :thought_balloon: [Probability makes counting (sometimes) easy](/FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
+  37. :x: [Permanents and the power of entropy](formal_book/blob/main/FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
+  38. :x: [The Dinitz problem](formal_book/blob/main/FormalBook/Ch38_The_Dinitz_problem.lean)
+  39. :x: [Five-coloring plane graphs](formal_book/blob/main/FormalBook/Ch39_Five-coloring_plane_graphs.lean)
+  40. :x: [How to guard a museum](formal_book/blob/main/FormalBook/Ch40_How_to_guard_a_museum.lean)
+  41. :x: [Turán's graph theorem](formal_book/blob/main/FormalBook/Ch41_Turán's_graph_theorem.lean)
+  42. :x: [Communicating without errors](formal_book/blob/main/FormalBook/Ch42_Communicating_without_errors.lean)
+  43. :x: [The chromatic number of Kneser graphs](formal_book/blob/main/FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
+  44. :speech_balloon: [Of friends and politicians](formal_book/blob/main/FormalBook/Ch44_Of_friends_and_politicians.lean)
+  45. :thought_balloon: [Probability makes counting (sometimes) easy](formal_book/blob/main/FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
 
 ## Contributing
 

From 940abed95c9f4ffc9bc7a8f4a0c1f95f2c2f44f9 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 21 Apr 2024 13:31:19 +0200
Subject: [PATCH 08/10] make links absolute

---
 README.md | 90 +++++++++++++++++++++++++++----------------------------
 1 file changed, 45 insertions(+), 45 deletions(-)

diff --git a/README.md b/README.md
index 90676df..2ffc63e 100644
--- a/README.md
+++ b/README.md
@@ -33,56 +33,56 @@ Status of the chapters:
   - :tada: chapter is completely formalized (possibly excluding the Appendix)
 
 ### Number Theory
-  1. :speech_balloon: [Six proofs of the infinity of primes](formal_book/blob/main/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
-  2. :speech_balloon: [Bertrand's postulate](formal_book/blob/main/FormalBook/Ch02_Bertrand's_postulate.lean)
-  3. :speech_balloon: [Binomial coefficients are (almost) never powers](formal_book/blob/main/FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
-  4. :x: [Representing numbers as sums of two squares](formal_book/blob/main/FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
-  5. :thought_balloon: [The law of quadratic reciprocity](formal_book/blob/main/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
-  6. :thought_balloon: [Every finite division ring is a field](formal_book/blob/main/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
-  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](formal_book/blob/main/FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
-  8. :thought_balloon: [Some irrational numbers](formal_book/blob/main/FormalBook/Ch08_Some_irrational_numbers.lean)
-  9. :x: [Four times ](formal_book/blob/main/FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
+  1. :speech_balloon: [Six proofs of the infinity of primes](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch01_Six_proofs_of_the_infinity_of_primes.lean)
+  2. :speech_balloon: [Bertrand's postulate](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch02_Bertrand's_postulate.lean)
+  3. :speech_balloon: [Binomial coefficients are (almost) never powers](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch03_Binomial_coefficients_are_(almost)_never_powers.lean)
+  4. :x: [Representing numbers as sums of two squares](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch04_Representing_numbers_as_sums_of_two_squares.lean)
+  5. :thought_balloon: [The law of quadratic reciprocity](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch05_The_law_of_quadratic_reciprocity.lean)
+  6. :thought_balloon: [Every finite division ring is a field](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch06_Every_finite_division_ring_is_a_field.lean)
+  7. :thought_balloon: [The spectral theorem and Hadamard's determinant problem](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch07_The_spectral_theorem_and_Hadamard's_determinant_problem.lean)
+  8. :thought_balloon: [Some irrational numbers](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch08_Some_irrational_numbers.lean)
+  9. :x: [Four times ](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch09_Four_times_pi²_over_6.lean)$\pi^2/6$
 
 ### Geometry
-  10. :x: [Hilbert's third problem: decomposing polyhedra](formal_book/blob/main/FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
-  11. :x: [Lines in the plane and decompositions of graphs](formal_book/blob/main/FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
-  12. :x: [The slope problem](formal_book/blob/main/FormalBook/Ch12_The_slope_problem.lean)
-  13. :x: [Three applications of Euler's formula](formal_book/blob/main/FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
-  14. :x: [Cauchy's rigidity theorem](formal_book/blob/main/FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
-  15. :x: [The Borromean rings don't exist](formal_book/blob/main/FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
-  16. :x: [Touching simplices](formal_book/blob/main/FormalBook/Ch16_Touching_simplices.lean)
-  17. :x: [Every large point set has an obtuse angle](formal_book/blob/main/FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
-  18. :x: [Borsuk's conjecture](formal_book/blob/main/FormalBook/Ch18_Borsuk's_conjecture.lean)
+  10. :x: [Hilbert's third problem: decomposing polyhedra](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch10_Hilbert's_third_problem_decomposing_polyhedra.lean)
+  11. :x: [Lines in the plane and decompositions of graphs](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch11_Lines_in_the_plane_and_decompositions_of_graphs.lean)
+  12. :x: [The slope problem](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch12_The_slope_problem.lean)
+  13. :x: [Three applications of Euler's formula](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch13_Three_applications_of_Euler's_formula.lean)
+  14. :x: [Cauchy's rigidity theorem](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch14_Cauchy's_rigidity_theorem.lean)
+  15. :x: [The Borromean rings don't exist](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch15_The_Borromean_rings_don't_exist.lean)
+  16. :x: [Touching simplices](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch16_Touching_simplices.lean)
+  17. :x: [Every large point set has an obtuse angle](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch17_Every_large_point_set_has_an_obtuse_angle.lean)
+  18. :x: [Borsuk's conjecture](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch18_Borsuk's_conjecture.lean)
 ### Analysis
-  19. :x: [Sets, functions, and the continuum hypothesis](formal_book/blob/main/FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
-  20. :thought_balloon: [In praise of inequalities](formal_book/blob/main/FormalBook/Ch20_In_praise_of_inequalities.lean)
-  21. :thought_balloon: [The fundamental theorem of algebra](formal_book/blob/main/FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
-  22. :x: [One square and an odd number of triangles](formal_book/blob/main/FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
-  23. :x: [A theorem of Pólya on polynomials](formal_book/blob/main/FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
-  24. :x: [Van der Waerden's permanent conjecture](formal_book/blob/main/FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
-  25. :x: [On a lemma of Littlewook and Offord](formal_book/blob/main/FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
-  26. :x: [Cotangent and the Herglotz trick](formal_book/blob/main/FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
-  27. :x: [Buffon's needle problem](formal_book/blob/main/FormalBook/Ch27_Buffon's_needle_problem.lean)
+  19. :x: [Sets, functions, and the continuum hypothesis](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch19_Sets,_functions,_and_the_continuum_hypothesis.lean)
+  20. :thought_balloon: [In praise of inequalities](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch20_In_praise_of_inequalities.lean)
+  21. :thought_balloon: [The fundamental theorem of algebra](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch21_The_fundamental_theorem_of_algebra.lean)
+  22. :x: [One square and an odd number of triangles](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch22_One_square_and_an_odd_number_of_triangles.lean)
+  23. :x: [A theorem of Pólya on polynomials](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch23_A_theorem_of_Pólya_on_polynomials.lean)
+  24. :x: [Van der Waerden's permanent conjecture](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch24_Van_der_Waerden's_permanent_conjecture.lean)
+  25. :x: [On a lemma of Littlewook and Offord](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch25_On_a_lemma_of_Littlewook_and_Offord.lean)
+  26. :x: [Cotangent and the Herglotz trick](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch26_Cotangent_and_the_Herglotz_trick.lean)
+  27. :x: [Buffon's needle problem](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch27_Buffon's_needle_problem.lean)
 ### Combinatorics
-  28. :x: [Pigeon-hole and double counting](formal_book/blob/main/FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
-  29. :x: [Tiling rectangles](formal_book/blob/main/FormalBook/Ch29_Tiling_rectangles.lean)
-  30. :x: [Three famous theorems on finite sets](formal_book/blob/main/FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
-  31. :x: [Shuffling cards](formal_book/blob/main/FormalBook/Ch31_Shuffling_cards.lean)
-  32. :thought_balloon: [Lattice paths and determinants](formal_book/blob/main/FormalBook/Ch32_Lattice_paths_and_determinants.lean)
-  33. :x: [Cayley's formula for the number of trees](formal_book/blob/main/FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
-  34. :x: [Identities versus bijections](formal_book/blob/main/FormalBook/Ch34_Identities_versus_bijections.lean)
-  35. :x: [The finite Kakeya problem](formal_book/blob/main/FormalBook/Ch35_The_finite_Kakeya_problem.lean)
-  36. :x: [Completing Latin squares](formal_book/blob/main/FormalBook/Ch36_Completing_Latin_squares.lean)
+  28. :x: [Pigeon-hole and double counting](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch28_Pigeon-hole_and_double_counting.lean)
+  29. :x: [Tiling rectangles](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch29_Tiling_rectangles.lean)
+  30. :x: [Three famous theorems on finite sets](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch30_Three_famous_theorems_on_finite_sets.lean)
+  31. :x: [Shuffling cards](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch31_Shuffling_cards.lean)
+  32. :thought_balloon: [Lattice paths and determinants](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch32_Lattice_paths_and_determinants.lean)
+  33. :x: [Cayley's formula for the number of trees](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch33_Cayley's_formula_for_the_number_of_trees.lean)
+  34. :x: [Identities versus bijections](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch34_Identities_versus_bijections.lean)
+  35. :x: [The finite Kakeya problem](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch35_The_finite_Kakeya_problem.lean)
+  36. :x: [Completing Latin squares](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch36_Completing_Latin_squares.lean)
 ### Graph Theory
-  37. :x: [Permanents and the power of entropy](formal_book/blob/main/FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
-  38. :x: [The Dinitz problem](formal_book/blob/main/FormalBook/Ch38_The_Dinitz_problem.lean)
-  39. :x: [Five-coloring plane graphs](formal_book/blob/main/FormalBook/Ch39_Five-coloring_plane_graphs.lean)
-  40. :x: [How to guard a museum](formal_book/blob/main/FormalBook/Ch40_How_to_guard_a_museum.lean)
-  41. :x: [Turán's graph theorem](formal_book/blob/main/FormalBook/Ch41_Turán's_graph_theorem.lean)
-  42. :x: [Communicating without errors](formal_book/blob/main/FormalBook/Ch42_Communicating_without_errors.lean)
-  43. :x: [The chromatic number of Kneser graphs](formal_book/blob/main/FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
-  44. :speech_balloon: [Of friends and politicians](formal_book/blob/main/FormalBook/Ch44_Of_friends_and_politicians.lean)
-  45. :thought_balloon: [Probability makes counting (sometimes) easy](formal_book/blob/main/FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
+  37. :x: [Permanents and the power of entropy](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch37_Permanents_and_the_power_of_entropy.lean)
+  38. :x: [The Dinitz problem](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch38_The_Dinitz_problem.lean)
+  39. :x: [Five-coloring plane graphs](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch39_Five-coloring_plane_graphs.lean)
+  40. :x: [How to guard a museum](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch40_How_to_guard_a_museum.lean)
+  41. :x: [Turán's graph theorem](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch41_Turán's_graph_theorem.lean)
+  42. :x: [Communicating without errors](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch42_Communicating_without_errors.lean)
+  43. :x: [The chromatic number of Kneser graphs](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch43_The_chromatic_number_of_Kneser_graphs.lean)
+  44. :speech_balloon: [Of friends and politicians](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch44_Of_friends_and_politicians.lean)
+  45. :thought_balloon: [Probability makes counting (sometimes) easy](https://github.com/mo271/formal_book/blob/main/FormalBook/Ch45_Probability_makes_counting_(sometimes)_easy.lean)
 
 ## Contributing
 

From 28bc37048ea8d8b868af85efc4cc3beb1f666379 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 21 Apr 2024 14:19:17 +0200
Subject: [PATCH 09/10] Setup blueprint (#51)

---
 .github/workflows/blueprint.yml | 92 +++++++++++++++++++++++++++++++++
 blueprint/src/content.tex       |  7 +++
 blueprint/src/extra_styles.css  | 25 +++++++++
 blueprint/src/latexmkrc         |  5 ++
 blueprint/src/macros/common.tex |  3 ++
 blueprint/src/macros/print.tex  | 26 ++++++++++
 blueprint/src/macros/web.tex    |  5 ++
 blueprint/src/plastex.cfg       | 17 ++++++
 blueprint/src/print.tex         | 33 ++++++++++++
 blueprint/src/web.tex           | 27 ++++++++++
 lake-manifest.json              |  9 ++++
 lakefile.lean                   |  6 +++
 12 files changed, 255 insertions(+)
 create mode 100644 .github/workflows/blueprint.yml
 create mode 100644 blueprint/src/content.tex
 create mode 100644 blueprint/src/extra_styles.css
 create mode 100644 blueprint/src/latexmkrc
 create mode 100644 blueprint/src/macros/common.tex
 create mode 100644 blueprint/src/macros/print.tex
 create mode 100644 blueprint/src/macros/web.tex
 create mode 100644 blueprint/src/plastex.cfg
 create mode 100644 blueprint/src/print.tex
 create mode 100644 blueprint/src/web.tex

diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
new file mode 100644
index 0000000..a0e41dc
--- /dev/null
+++ b/.github/workflows/blueprint.yml
@@ -0,0 +1,92 @@
+on:
+  push:
+    branches:
+      - main
+
+# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+jobs:
+  build_project:
+    runs-on: ubuntu-latest
+    name: Build project
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v2
+        with:
+          fetch-depth: 0
+
+      - name: Install elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0
+
+      - name: Update checkdecls
+        run: ~/.elan/bin/lake update checkdecls
+
+      - name: Get cache
+        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+
+      - name: Build project
+        run: ~/.elan/bin/lake -Kenv=dev build FormalBook
+
+      - name: Cache mathlib docs
+        uses: actions/cache@v3
+        with:
+          path: |
+            .lake/build/doc/Init
+            .lake/build/doc/Lake
+            .lake/build/doc/Lean
+            .lake/build/doc/Std
+            .lake/build/doc/Mathlib
+            .lake/build/doc/declarations
+            !.lake/build/doc/declarations/declaration-data-FormalBook*
+          key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
+          restore-keys: |
+            MathlibDoc-
+
+      - name: Build documentation
+        run: ~/.elan/bin/lake -Kenv=dev build FormalBook:docs
+
+      - name: Build blueprint and copy to `docs/blueprint`
+        uses: xu-cheng/texlive-action@v2
+        with:
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
+          run: |
+            apk update
+            apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
+            git config --global --add safe.directory $GITHUB_WORKSPACE
+            git config --global --add safe.directory `pwd`
+            python3 -m venv env
+            source env/bin/activate
+            pip install --upgrade pip requests wheel
+            pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/"
+            pip install git+https://github.com/PatrickMassot/leanblueprint.git@client
+            leanblueprint pdf
+            mkdir docs
+            cp blueprint/print/print.pdf docs/blueprint.pdf
+            leanblueprint web
+            cp -r blueprint/web docs/blueprint
+
+      - name: Check declarations
+        run: |
+            ~/.elan/bin/lake exe checkdecls blueprint/lean_decls
+
+      - name: Move documentation to `docs/docs`
+        run: |
+          sudo chown -R runner docs
+          cp -r .lake/build/doc docs/docs
+
+      - name: Upload docs & blueprint artifact
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: docs/
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v1
+
+      - name: Make sure the cache works
+        run: |
+          mv docs/docs .lake/build/doc
\ No newline at end of file
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
new file mode 100644
index 0000000..b5cd27b
--- /dev/null
+++ b/blueprint/src/content.tex
@@ -0,0 +1,7 @@
+% In this file you should put the actual content of the blueprint.
+% It will be used both by the web and the print version.
+% It should *not* include the \begin{document}
+%
+% If you want to split the blueprint content into several files then
+% the current file can be a simple sequence of \input. Otherwise It
+% can start with a \section or \chapter for instance.
\ No newline at end of file
diff --git a/blueprint/src/extra_styles.css b/blueprint/src/extra_styles.css
new file mode 100644
index 0000000..b96c776
--- /dev/null
+++ b/blueprint/src/extra_styles.css
@@ -0,0 +1,25 @@
+/* This file contains CSS tweaks for this blueprint.
+ * As an example, we included CSS rules that put
+ * a vertical line on the left of theorem statements
+ * and proofs.
+ * */
+
+div.theorem_thmcontent {
+	border-left: .15rem solid black;
+}
+
+div.proposition_thmcontent {
+	border-left: .15rem solid black;
+}
+
+div.lemma_thmcontent {
+	border-left: .1rem solid black;
+}
+
+div.corollary_thmcontent {
+	border-left: .1rem solid black;
+}
+
+div.proof_content {
+	border-left: .08rem solid grey;
+}
diff --git a/blueprint/src/latexmkrc b/blueprint/src/latexmkrc
new file mode 100644
index 0000000..38d5963
--- /dev/null
+++ b/blueprint/src/latexmkrc
@@ -0,0 +1,5 @@
+# This file configures the latexmk command you can use to compile
+# the pdf version of the blueprint
+$pdf_mode = 1;
+$pdflatex = 'xelatex -synctex=1';
+@default_files = ('print.tex');
\ No newline at end of file
diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex
new file mode 100644
index 0000000..131c9f8
--- /dev/null
+++ b/blueprint/src/macros/common.tex
@@ -0,0 +1,3 @@
+% In this file you should put all LaTeX macros to be used
+% both by the pdf version and the web version.
+% This should be most of your macros.
\ No newline at end of file
diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex
new file mode 100644
index 0000000..0b59bae
--- /dev/null
+++ b/blueprint/src/macros/print.tex
@@ -0,0 +1,26 @@
+% In this file you should put macros to be used only by
+% the printed version. Of course they should have a corresponding
+% version in macros/web.tex.
+% Typically the printed version could have more fancy decorations.
+% This should be a very short file.
+%
+% This file starts with dummy macros that ensure the pdf
+% compiler will ignore macros provided by plasTeX that make
+% sense only for the web version, such as dependency graph
+% macros.
+
+
+% Dummy macros that make sense only for web version.
+\newcommand{\lean}[1]{}
+\newcommand{\leanok}{}
+% Make sure that arguments of \uses and \proves are real labels, by using invisible refs:
+% latex prints a warning if the label is not defined, but nothing is shown in the pdf file.
+% It uses LaTeX3 programming, this is why we use the expl3 package.
+\ExplSyntaxOn
+\NewDocumentCommand{\uses}{m}
+ {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
+  \ignorespaces}
+\NewDocumentCommand{\proves}{m}
+ {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
+  \ignorespaces}
+\ExplSyntaxOff
\ No newline at end of file
diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex
new file mode 100644
index 0000000..ceee975
--- /dev/null
+++ b/blueprint/src/macros/web.tex
@@ -0,0 +1,5 @@
+% In this file you should put macros to be used only by
+% the web version. Of course they should have a corresponding
+% version in macros/print.tex.
+% Typically the printed version could have more fancy decorations.
+% This will probably be a very short file.
\ No newline at end of file
diff --git a/blueprint/src/plastex.cfg b/blueprint/src/plastex.cfg
new file mode 100644
index 0000000..de3dbae
--- /dev/null
+++ b/blueprint/src/plastex.cfg
@@ -0,0 +1,17 @@
+[general]
+renderer=HTML5
+copy-theme-extras=yes
+plugins=plastexdepgraph  plastexshowmore  leanblueprint
+
+[document]
+toc-depth=3
+toc-non-files=True
+
+[files]
+directory=../web/
+split-level= 0
+
+[html5]
+localtoc-level=0
+extra-css=extra_styles.css
+mathjax-dollars=False
\ No newline at end of file
diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex
new file mode 100644
index 0000000..cc097e3
--- /dev/null
+++ b/blueprint/src/print.tex
@@ -0,0 +1,33 @@
+% This file makes a printable version of the blueprint
+% It should include all the \usepackage needed for the pdf version.
+% The template version assume you want to use a modern TeX compiler
+% such as xeLaTeX or luaLaTeX including support for unicode
+% and Latin Modern Math font with standard bugfixes applied.
+% It also uses expl3 in order to support macros related to the dependency graph.
+% It also includes standard AMS packages (and their improved version
+% mathtools) as well as support for links with a sober decoration
+% (no ugly rectangles around links).
+% It is otherwise a very minimal preamble (you should probably at least
+% add cleveref and tikz-cd).
+
+\documentclass[a4paper]{report}
+
+\usepackage{geometry}
+
+\usepackage{expl3}
+
+\usepackage{amssymb, amsthm, mathtools}
+\usepackage[unicode,colorlinks=true,linkcolor=blue,urlcolor=magenta, citecolor=blue]{hyperref}
+
+\usepackage[warnings-off={mathtools-colon,mathtools-overbracket}]{unicode-math}
+
+\input{macros/common}
+\input{macros/print}
+
+\title{Formal Book}
+\author{Moritz Firsching \and Nikolas Kuhn}
+
+\begin{document}
+\maketitle
+\input{content}
+\end{document}
\ No newline at end of file
diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex
new file mode 100644
index 0000000..e2fd8b2
--- /dev/null
+++ b/blueprint/src/web.tex
@@ -0,0 +1,27 @@
+% This file makes a web version of the blueprint
+% It should include all the \usepackage needed for this version.
+% The template includes standard AMS packages.
+% It is otherwise a very minimal preamble (you should probably at least
+% add cleveref and tikz-cd).
+
+\documentclass{report}
+
+\usepackage{amssymb, amsthm, amsmath}
+\usepackage{hyperref}
+\usepackage[showmore, dep_graph]{blueprint}
+
+
+\input{macros/common}
+\input{macros/web}
+
+\home{https://mo271.github.io/formal_book}
+\github{https://github.com/mo271/formal_book}
+\dochome{https://mo271.github.io/formal_book/docs}
+
+\title{Formal Book}
+\author{Moritz Firsching \and Nikolas Kuhn}
+
+\begin{document}
+\maketitle
+\input{content}
+\end{document}
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
index 3f7f1ed..7eccd50 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -63,6 +63,15 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "2ee81a0269048010900117b675876a1d8db5883c",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "formal_book",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 2779ee9..5158f6f 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -13,3 +13,9 @@ require mathlib from git
 lean_lib «FormalBook» {
   -- add any library configuration options here
 }
+
+require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
+
+meta if get_config? env = some "dev" then
+require «doc-gen4» from git
+  "https://github.com/leanprover/doc-gen4" @ "main"
\ No newline at end of file

From d489678971d2b4d6d522763f80c4697290248247 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Sun, 21 Apr 2024 14:44:51 +0200
Subject: [PATCH 10/10] make doc4-gen dependency unconditional

---
 lake-manifest.json | 36 ++++++++++++++++++++++++++++++++++++
 lakefile.lean      |  3 +--
 2 files changed, 37 insertions(+), 2 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 7eccd50..540d7a1 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -72,6 +72,42 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/xubaiw/CMark.lean",
+   "type": "git",
+   "subDir": null,
+   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+   "name": "CMark",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/hargonix/LeanInk",
+   "type": "git",
+   "subDir": null,
+   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
+   "name": "leanInk",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "doc-gen",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "rev": "a34d3c1f7b72654c08abe5741d94794db40dbb2e",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "formal_book",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 5158f6f..a037803 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -16,6 +16,5 @@ lean_lib «FormalBook» {
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
-meta if get_config? env = some "dev" then
 require «doc-gen4» from git
-  "https://github.com/leanprover/doc-gen4" @ "main"
\ No newline at end of file
+  "https://github.com/leanprover/doc-gen4" @ "main"