Graceful Tree Conjecture (Ringel–Kotzig conjecture)

Conjecture · graceful_tree_conjecture

Every tree admits a graceful labeling.

A graceful labeling of a tree $T$ with $m$ edges is an injective map $f : V \to \{0, \dots, m\}$ such that the multiset of absolute differences $|f(u) - f(v)|$ over edges $\{u,v\}$ of $T$ equals $\{1, \dots, m\}$ .

Formal statement · Lean 4.lean

theorem graceful_tree_conjecture {V : Type*} [Fintype V] [DecidableEq V]
    (T : SimpleGraph V) [DecidableRel T.Adj] (hT : T.IsTree) :
    let m := T.edgeFinset.card
    ∃ f : V → ℕ,
      Function.Injective f ∧
      (∀ v, f v ≤ m) ∧
      T.edgeFinset.image (fun e =>
        e.lift ⟨fun u v => Int.natAbs ((f u : ℤ) - (f v : ℤ)),
                fun u v => by
                  show ((f u : ℤ) - f v).natAbs = ((f v : ℤ) - f u).natAbs
                  rw [← Int.natAbs_neg, neg_sub]⟩) = Finset.Icc 1 m := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗