This Textbook project develops a reusable Lean library around Martin Aigner and Günter M. Ziegler's Proofs from THE BOOK. It combines results imported from the existing proof_in_the_book repository with precise contribution targets from the sixth edition (2018). The aim is to preserve mathematical meaning, reuse existing proofs, and make the remaining work accessible to other contributors.
The original import contains 156 distinct platform-accepted results. Euclid, the original main theorem, is retained as a completed milestone when the project goal moves to the sixth-edition extension. Every one of the repository's 40 chapter topics has accepted results. Each result certifies its actual Lean statement, including its hypotheses; this does not certify every argument or every theorem in a chapter. Some proofs reuse Mathlib, while others were developed in the repository. Their source and proof notes retain that distinction.
The imported source snapshot is 873d52e0c88cd351f594221e70c3c5b3559777a9. Imported results use Lean 4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Immutable public source links are used only where the linked source matches the verified artifact. Compatibility changes, unsuccessful attempts, and verification evidence are retained in the integration project.
The live goal is the explicit conjunction of the 21 linked sixth-edition extension targets. Its reduction connects these targets to the goal, so proving the remaining children advances the project. This goal is deliberately narrower than “every theorem and every proof in the book”; the unlinked topology tasks below are additional formalization work.
New milestones explicitly marked 6th ed. cover Chapters 7 (spectral theorem and determinants), 15 (round circles and links), 35 (finite Kakeya), 37 (permanents and entropy), and 45 (probabilistic counting). They include the precise definitions and boundary conditions needed to state the results. Compiled Open targets are requests for proofs, not proved results. The spectral theorem has a direct Mathlib proof; community results are reused under their actual statements and with attribution.
Two Chapter 15 tasks intentionally remain unlinked mathematical milestones: the full non-equivalence assertion for the depicted Borromean, Tait, and trivial links, and the Fox-coloring invariance bridge for equivalent link diagrams. These invite formalization of the diagrams and the topology bridge as well as proof. The separate modular Fox calculations do not by themselves establish ambient non-equivalence.
The crossing-lemma target is the universal good-drawing form: actual injective edge arcs and exact finite intersection records appear in its interface. It does not assume the desired crossing bound. The Ramsey target preserves the real exponent for odd k. The related public Erdős–Ramsey result with a rounded exponent is identified as a supporting result, not as proof of that full target.
Older milestones use the repository's chapter labels. Repository Chapters 1–21 match the bundled fourth edition; Chapter 22 inserts Van der Waerden's permanent theorem, and Chapters 23–40 correspond to fourth-edition Chapters 22–39. The sixth edition has 45 chapters, so these organizational labels are not sixth-edition chapter numbers. New milestones give sixth-edition numbers and printed source pages explicitly.
Some existing formalizations preserve narrower statements or additional premises. Examples include repository Chapter 13's dihedral-angle conclusion, Chapter 28's Dilworth lower-bound result, and the geometric premises in Chapter 36. Read the actual linked theorem and its description before reusing it. A chapter title or the former Euclid main theorem is not a completion certificate for the collection.
Choose an Open linked theorem and inspect its definitions, exact binders, Mathlib revision, and prior attempts. Reuse a compatible existing result when it proves that statement; preserve the original contributor's attribution. Submit a matching proof for verification. For an unlinked milestone, first formalize and review the source statement and its definitions. These are known textbook results awaiting formalization or proof in this project, rather than claims of new unresolved mathematics.
Source repository: https://github.com/xiangyazi24/proof_in_the_book
Book: Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), https://doi.org/10.1007/978-3-662-57265-8
theorem BookSixth.sixthEditionExtension :
(∀ {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsHermitian),
∃ Q : Matrix.unitaryGroup (Fin n) ℝ, ∃ d : Fin n → ℝ,
star (Q : Matrix (Fin n) (Fin n) ℝ) * A * (Q : Matrix (Fin n) (Fin n) ℝ) = Matrix.diagonal d) ∧
(∀ {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsHermitian) (h : 0 < offDiagonalMass A),
∃ Q : Matrix.unitaryGroup (Fin n) ℝ,
offDiagonalMass (star (Q : Matrix (Fin n) (Fin n) ℝ) * A * (Q : Matrix (Fin n) (Fin n) ℝ)) < offDiagonalMass A) ∧
(∀ {n : ℕ} (hn : 0 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A),
|A.det| ≤ (n : ℝ) ^ ((n : ℝ) / 2)) ∧
(∀ {n : ℕ} (hn : 0 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A),
(|A.det| = (n : ℝ) ^ ((n : ℝ) / 2)) ↔
∀ i j, i ≠ j → (∑ k, A k i * A k j) = 0) ∧
(∀ {n : ℕ} (hn : 2 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A) (horth : A.transpose * A = (n : ℝ) • (1 : Matrix (Fin n) (Fin n) ℝ)),
4 ∣ n) ∧
(∀ (m : ℕ),
∃ A : Matrix (Fin (2^m)) (Fin (2^m)) ℝ, SignMatrix A ∧
A.transpose * A = ((2^m : ℕ) : ℝ) • (1 : Matrix (Fin (2^m)) (Fin (2^m)) ℝ)) ∧
(∀ (n : ℕ) (hn : 2 ≤ n),
∃ A : Matrix (Fin n) (Fin n) ℝ, SignMatrix A ∧ Real.sqrt (n.factorial : ℝ) < A.det) ∧
(∀ {m : ℕ} (C : Fin m → Set Space3) (hround : ∀ i, RoundCircle (C i)) (hdisjoint : ∀ i j, i ≠ j → Disjoint (C i) (C j)) (hpairs : ∀ i j, i ≠ j → IsUnlink (![C i, C j] : Fin 2 → Set Space3)),
IsUnlink C) ∧
(∀ {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (hn : 0 < n) (p : MvPolynomial (Fin n) F) (hp : p ≠ 0),
(Finset.univ.filter (fun x : Fin n → F => MvPolynomial.eval x p = 0)).card ≤
p.totalDegree * Fintype.card F ^ (n-1)) ∧
(∀ {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} (E : Finset (Fin n → F)) (hE : E.card < Nat.choose (n+d) d),
∃ p : MvPolynomial (Fin n) F, p ≠ 0 ∧ p.totalDegree ≤ d ∧
∀ x ∈ E, MvPolynomial.eval x p = 0) ∧
(∀ {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (hn : 0 < n) (K : Finset (Fin n → F)) (hK : Kakeya K),
Nat.choose (Fintype.card F + n - 1) n ≤ K.card ∧
Fintype.card F ^ n ≤ n.factorial * K.card) ∧
(∀ {n : ℕ} (A : Matrix (Fin n) (Fin n) ℕ) (hA : ∀ i j, A i j ≤ 1) (hrows : ∀ i, 0 < ∑ j, A i j),
(permanent A : ℝ) ≤ ∏ i, ((Nat.factorial (∑ j, A i j) : ℕ) : ℝ) ^
(1 / ((∑ j, A i j : ℕ) : ℝ))) ∧
(∀ (n : ℕ) (hn : 0 < n),
((n.factorial : ℝ) ^ (2*n) / (n : ℝ) ^ (n*n) ≤ latinCount n) ∧
((latinCount n : ℝ) ≤ ∏ k ∈ Finset.Icc 1 n,
(k.factorial : ℝ) ^ ((n : ℝ) / (k : ℝ)))) ∧
(Filter.Tendsto (fun n : ℕ => (latinCount n : ℝ) ^ (1 / (n : ℝ)^2) / (n : ℝ))
Filter.atTop (nhds (Real.exp (-2)))) ∧
(∀ {N d : ℕ} (hd : 2 ≤ d) (A : Finset (Finset (Fin N))) (hsize : ∀ S ∈ A, S.card = d) (hcard : A.card ≤ 2^(d-1)),
∃ c : Fin N → Bool, ∀ S ∈ A, ∃ u ∈ S, ∃ v ∈ S, c u ≠ c v) ∧
(∀ (k N : ℕ) (hk : 2 ≤ k) (hN : (N : ℝ) < (2 : ℝ)^((k : ℝ)/2)),
∃ G : SimpleGraph (Fin N), NoMono k G) ∧
(∀ (k : ℕ) (hk : 2 ≤ k),
∃ N : ℕ, ∃ G : SimpleGraph (Fin N), ¬ HasColoring G k ∧
∀ l : ℕ, l ≤ k → ¬ HasCycle G l) ∧
(∀ {N M : ℕ} (hN : 0 < N) (hM : 4*N ≤ M) (D : PlaneDrawing N M),
M^3 ≤ 64 * N^2 * D.crossings.card) ∧
(∀ (n : ℕ),
(∑ B : Fin n → Fin n → Bool, (Matrix.det (fun i j => if B i j then (1 : ℝ) else -1))^2) = (2 : ℝ)^(n*n) * (n.factorial : ℝ)) ∧
(∀ (n : ℕ) (hn : 3 ≤ n) (hodd : Odd n) (a b c : ZMod n),
BorromeanFox a b c ↔ a = b ∧ b = c) ∧
(∀ (a : Fin 6 → ZMod 5),
TaitFox a ↔ a 0 = a 2 ∧ a 2 = a 4 ∧ a 1 = a 3 ∧ a 3 = a 5) := by sorryThis project goal is the conjunction of the 21 explicitly stated results in the sixth-edition extension: spectral diagonalization and its off-diagonal reduction; Hadamard bound, equality, order restriction and powers-of-two construction; a strict determinant lower bound and the mean-square determinant identity; pairwise unlinked round circles forming an unlink; polynomial zero and interpolation bounds and finite Kakeya; the permanent bound and Latin-square bounds and asymptotic; hypergraph two-colorability, the real-exponent Ramsey bound, high-girth/high-chromatic graphs and the good-drawing crossing lemma; and the two explicit Fox-coloring calculations. Every component retains the exact binders and boundary conditions of its linked child. This is a collection-completion goal, not a claim that every theorem or every proof in the book is covered. The full diagram-to-topology bridge remains an explicitly unlinked milestone outside this conjunction.