Formal target: Corpus.WikipediaGracefulLabeling.graceful_tree_conjecture

Let T be a finite tree, meaning a nonempty connected simple graph with no cycles, and let m be its number of edges. Can its vertices be given distinct integer labels from 0 through m so that the absolute differences of the labels at the ends of its edges are exactly 1, 2, …, m, each once? For a one-vertex tree, label its vertex 0; the required edge-difference list is empty.

Exact formal statement

∀ {V : Type u_1} [inst : Fintype.{u_1} V] [DecidableEq.{u_1 + 1} V] (T : SimpleGraph.{u_1} V)
  [inst_2 : DecidableRel.{u_1 + 1, u_1 + 1} (SimpleGraph.Adj.{u_1} T)],
  SimpleGraph.IsTree.{u_1} T →
    have m := Finset.card.{u_1} (SimpleGraph.edgeFinset.{u_1} T);
    Exists.{u_1 + 1} fun f =>
      And (Function.Injective.{u_1 + 1, 1} f)
        (And (∀ (v : V), LE.le.{0} (f v) m)
          (Eq.{1}
            (Finset.image.{u_1, 0}
              (fun e =>
                DFunLike.coe.{max 1 (u_1 + 1), max 1 (u_1 + 1), max 1 (u_1 + 1)} Sym2.lift.{u_1, 0}
                  (Subtype.mk.{max 1 (u_1 + 1)}
                    (fun u v => (HSub.hSub.{0, 0, 0} (Nat.cast.{0} (f u)) (Nat.cast.{0} (f v))).natAbs) ⋯)
                  e)
              (SimpleGraph.edgeFinset.{u_1} T))
            (Finset.Icc.{0} 1 m)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record