Chapter 15, Theorem 2 proof: Tait Fox 5-colorings

Proved

BookSixth.tait_fox_five

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

For the reduced Fox equations of Tait diagram 18 modulo five, the even-indexed outer labels agree and the odd-indexed labels agree, with the two labels otherwise arbitrary. Thus there are 25 assignments. The statement concerns the explicit equations, not an assumed link invariant.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.tait_fox_five (a : Fin 6 → ZMod 5) :
    TaitFox a ↔ a 0 = a 2 ∧ a 2 = a 4 ∧ a 1 = a 3 ∧ a 3 = a 5 := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 15, Theorem 2 proof: Tait Fox 5-colorings, p. 104. https://doi.org/10.1007/978-3-662-57265-8_15

View graph