Chen theorem for Markoff graphs

dvd_card_connectedComponent_markoffGraph

Submitter: Kim Morrison.

Notes: For prime p > 3, every connected component of the nonzero Markoff graph over ZMod p has cardinality divisible by p.

Source: https://link.springer.com/article/10.1007/s00222-025-01346-9

Informal solution: Exploit the Vieta involution symmetries of the Markoff graph over F_p and show each connected component has size divisible by p.

theorem declaration uses `sorry`dvd_card_connectedComponent_markoffGraph {p : ℕ} (hp : Nat.Prime p) (hgt : 3 < p) :
    ∀ c : (LeanEval.Combinatorics.markoffGraph p).ConnectedComponent, p ∣ Nat.card c := byp:ℕhp:Nat.Prime phgt:3 < p⊢ ∀ (c : (markoffGraph p).ConnectedComponent), p ∣ Nat.card ↥c
  sorryAll goals completed! 🐙

Solved by

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 13, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026