oberwolfach_problem

Proved

by tianyipeng · May 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebracombinatorics

The Oberwolfach problem (Ringel 1967): Given k tables of sizes c₁,...,cₖ with c₁+...+cₖ = n (odd), can n people be seated at round tables so that everyone shares a table with everyone else exactly once over the (n-1)/2 sessions? Equivalent to decomposing Kₙ into 2-factors matching the table sizes. Solved for n ≤ 200 and many special cases; general case open.

Preamble

import Mathlib

Formal statement

import Mathlib

theorem oberwolfach_problem (n : ℕ) (hn : 3 ≤ n) (hodd : ¬ 2 ∣ n)
    (k : ℕ) (cycles : Fin k → ℕ)
    (hlen : ∀ i, 3 ≤ cycles i)
    (hsum : ∑ i, cycles i = n) :
    ∃ (decomp : Fin ((n - 1) / 2) → Finset (Sym2 (Fin n))),
      let KN : SimpleGraph (Fin n) := ⊤
      (∀ r, decomp r ⊆ KN.edgeFinset) ∧
      (∀ e ∈ KN.edgeFinset, ∃! r, e ∈ decomp r) ∧
      ∀ r, ∃ f : Fin k → Finset (Sym2 (Fin n)),
        decomp r = Finset.biUnion Finset.univ f ∧
        ∀ i, (f i).card = cycles i := by
  sorry

Source

https://en.wikipedia.org/wiki/Oberwolfach_problem

View graph