Graceful trees: use every edge difference once

graph-theory · trees · graph-labeling

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.

Why it matters
A small labeling puzzle asks for simultaneous control of vertex labels and edge differences. Successful constructions connect tree structure with additive combinatorics and graph decompositions.

One possible first attack
For a path with m edges, label successive vertices 0, m, 1, m−1, 2, m−2, … and prove that the successive absolute differences are m, m−1, …, 1. Handle m = 0 explicitly. This is the known path family, not a proof for all trees.

Mathematical status
Open in full (checked 2026-09-11). Letzter, Pokrovskiy and Williams prove an asymptotic, almost-graceful result, not an exact labeling of every tree. The target’s equality of finite sets of edge differences is faithful: there are m edges and m required values, so none can repeat.

Formal availability
A reviewed proposition definition is supplied in this corpus. A target is a question to prove, not a proof. Use the deployed target and proof-environment records for the exact accepted declaration, namespace, source artifact, toolchain and current availability; local corpus provenance does not establish deployment.

Sources and provenance
Letzter, Pokrovskiy and Williams, On the gracesize of trees: exact graceful-labeling question and asymptotic partial result (checked 2026-09-11): https://arxiv.org/abs/2511.11331
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/GracefulLabeling.lean
Local target: Corpus.WikipediaGracefulLabeling.graceful_tree_conjecture
Source SHA-256: e735c42bc53f481dd20369c5a20962e3cbabee2819c2e1b7a2b6a8a6cafad809
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record