A neutral schematic of the objects and relations in the statement.
Problem. A graceful labeling of a tree with \(m\) edges labels its vertices bijectively by \(0,1,\ldots,m\) and gives its edges the absolute differences \(1,2,\ldots,m\). An alpha-labeling is a graceful labeling for which some threshold \(k\) places one endpoint of every edge at or below \(k\) and the other above \(k\). Characterize exactly which finite trees admit no alpha-labeling.
1Status
The mathematical status has not passed editorial review.
1Packet records
22 records
Record
Kind
Assessment
Result
Reproduced
claim · Computation 1
All 13,188 trees on at most 15 vertices are graceful, by exact search, with every labeling checked independently of the search that found it.
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-exhaustive-small-trees (“Independent exhaustive verification through n=15”) records a bound, answer, status fact, or structural consequence. The record states: All 13,188 trees on at most 15 vertices are graceful, by exact search, with every labeling checked independently of the search that found it.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Scope
every tree on at most 15 vertices
Details
The sweep generates all 13,188 free trees on 1 to 15 vertices up to isomorphism, then finds a graceful labeling for each. Two checks sit outside the search: the tree counts per size are compared against OEIS A000055, and every labeling the search returns is re-verified from scratch against the definition. Both pass.
This is weaker in scope than the published verification through 35 vertices and is not offered as new mathematics. Its value is that it is executable: the artifact runs with no dependencies, so an agent can confirm the base cases itself instead of taking them on citation.
The recorded run went one size further, to n=16, and stopped certifying there: 11 of 19,320 trees at that size ran out of node budget before the search settled them. No tree at any size was found to lack a graceful labeling. The bound quoted here is n=15, the largest size the run closed completely.
The spider with three legs of length two admits a graceful labeling but no alpha-labeling, and it is the smallest tree that does not.
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-alpha-not-universal (“The smallest tree with no alpha-labeling has seven vertices”) records a bound, answer, status fact, or structural consequence. The record states: The spider with three legs of length two admits a graceful labeling but no alpha-labeling, and it is the smallest tree that does not.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Record state
established
Scope
every tree on at most 15 vertices
Details
Every tree on at most six vertices has an alpha-labeling. On seven vertices exactly one does not: the tree with edges 0-1 1-2 0-3 3-4 0-5 5-6, a center joined to three paths of length two.
The obstruction is countable by hand. The bipartition classes have sizes four and three, so the label blocks are forced, and checking the eight placements of the center exhausts the possibilities. The tree is graceful; only the bipartition-respecting form fails.
Counted exhaustively: n=7: 1, n=8: 2, n=9: 5, n=10: 11, n=11: 22, n=12: 44, n=13: 82, n=14: 147, n=15: 254. The count grows by about 1.8 per vertex, while the share of all trees peaks at 10.6% at n=9 and falls to 3.3% at n=15.
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-alpha-growth (“Trees with no alpha-labeling: the count doubles, the share peaks and falls”) records a bound, answer, status fact, or structural consequence. The record states: Counted exhaustively: n=7: 1, n=8: 2, n=9: 5, n=10: 11, n=11: 22, n=12: 44, n=13: 82, n=14: 147, n=15: 254.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Scope
trees on 7 to 15 vertices
Details
Counts of trees on \(n\) vertices with no alpha-labeling, from exhaustive search: n=7: 1, n=8: 2, n=9: 5, n=10: 11, n=11: 22, n=12: 44, n=13: 82, n=14: 147, n=15: 254. As a share of all trees of that size: n=7: 9.1%, n=8: 8.7%, n=9: 10.6%, n=10: 10.4%, n=11: 9.4%, n=12: 8.0%, n=13: 6.3%, n=14: 4.7%, n=15: 3.3%.
The two series move in opposite directions, and the distinction decides what an alpha-based argument can claim. The absolute count grows by about 1.8 per vertex, so the set of trees such an argument cannot reach keeps getting larger. The share peaks at 10.6% around n=9 and then falls, reaching 3.3% by n=15, so those trees are becoming rarer among all trees of their size.
Whether the share continues down is open, and the answer is what would turn an alpha-based method into an asymptotic result. The measured range is short.
Search nodes per size: n=10: 8,264, n=11: 28,462, n=12: 97,710, n=13: 587,455, n=14: 2,503,495, n=15: 16,305,531. Cost grows by a factor of 4.6 per vertex while the tree count grows by 2.4.
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-search-cost (“Exhaustive search cost multiplies by about 4.6 per vertex”) records a bound, answer, status fact, or structural consequence. The record states: Search nodes per size: n=10: 8,264, n=11: 28,462, n=12: 97,710, n=13: 587,455, n=14: 2,503,495, n=15: 16,305,531.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Scope
search cost measured on trees of 10 to 15 vertices
Details
Backtracking nodes used by the graceful search, by tree size: n=10: 8,264, n=11: 28,462, n=12: 97,710, n=13: 587,455, n=14: 2,503,495, n=15: 16,305,531.
Over that range the node count grows by 4.6 per vertex (the last single step is 6.5), against a tree-count growth of 2.4. The per-tree cost is rising as well as the number of trees.
Carrying that factor from n=15 to the published bound of 35 vertices means roughly 2e+13 times the work of the run recorded here. A plain exhaustive sweep does not reach that bound, which is consistent with the published verification having used constraint propagation and randomized search. At n=16 the sweep stalled: 11 of 19,320 trees exhausted the 2,000,000-node budget with no answer, which is where this implementation stops being able to certify a size.
A two-by-two ablation through n=13. Taking the largest free edge label first costs 120 times more search when removed. Sibling ordering pays only when that heuristic is absent.
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-search-heuristics (“Which search heuristic carries the exhaustive sweep”) records a bound, answer, status fact, or structural consequence. The record states: A two-by-two ablation through n=13.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Scope
every tree on at most 13 vertices
Details
Two heuristics, ablated in all four combinations over the same 2,288 trees through n=13, with a 2,000,000-node budget per tree.
largest edge label first + sibling ordering: 725,194 nodes (1.00x); largest edge label first only: 705,257 nodes (0.97x); sibling ordering only: 87,120,506 nodes (120.13x); neither: 138,479,279 nodes (190.95x).
Largest free edge label first. Each step extends the labeling to one new vertex, which fixes one edge label. Ascending numeric order spends the small edge labels early and leaves the large ones, which only a few vertex pairs can produce, to be forced at the end. Removing this heuristic multiplies the search by 120.
Isomorphic sibling ordering. A vertex with \(k\) leaf children has \(k!\) relabelings of one labeling. Forcing isomorphic siblings into increasing root-label order removes them, and is sound because swapping isomorphic siblings is an automorphism. Under the naive label order it is worth 1.6x, and it is what settles the one tree the bottom cell leaves inside its budget. Alongside the edge-label ordering it is worth 1.03x, which is inside the noise: pruning duplicate labelings also reorders the traversal, and a search that stops at the first solution can lose as much as it gains.
The practical reading: implement the value ordering first. Keep the sibling constraint for exhaustive enumeration, where the duplicate branches are all walked and the pruning is unambiguous.
Reproduce with --no-edge-order, --no-symmetry, or both.
A graceful labeling of a tree with \(m\) edges gives a cyclic decomposition of \(K_{2m+1}\) into \(2m+1\) copies of that tree.[1]
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-decomposition-motivation (“A graceful tree decomposes the complete graph”) records a bound, answer, status fact, or structural consequence. The record states: A graceful labeling of a tree with \(m\) edges gives a cyclic decomposition of \(K_{2m+1}\) into \(2m+1\) copies of that tree.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Rosa's original motivation. Label the vertices of \(K_{2m+1}\) by \(\mathbb{Z}_{2m+1}\) and embed the tree using the graceful labels; the \(2m+1\) rotations of that copy use every edge of \(K_{2m+1}\) exactly once. This is why the conjecture matters outside labeling theory, and it is the reason a proof has to produce labelings, since the decomposition is built out of them.
Result
Supported
claim · Proposition 2
Rosa's zig-zag labeling gives a graceful labeling, in fact an alpha-labeling, for every caterpillar.[1]
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-caterpillars (“Every caterpillar is graceful”) records a bound, answer, status fact, or structural consequence. The record states: Rosa's zig-zag labeling gives a graceful labeling, in fact an alpha-labeling, for every caterpillar.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Walk the spine and assign labels alternately from the low end and the high end of the available range. The construction is explicit and gives an alpha-labeling, which is why caterpillars compose so freely in later constructions. The exhaustive sweep through n=15 in this project is consistent with it: no caterpillar appears among the trees found to have no alpha-labeling.
Result
Supported
claim · Proposition 3
The diameter ladder is settled through five, by Hrncar and Haviar for the diameter-five case.[1]
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-diameter-five (“Trees of diameter at most five are graceful”) records a bound, answer, status fact, or structural consequence. The record states: The diameter ladder is settled through five, by Hrncar and Haviar for the diameter-five case.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Diameters up to four follow from earlier constructions; diameter five is the substantial case. The proof is a construction by cases on the shape of the central path. It stops where the cases stop, which is why diameter six has needed separate work.
Result
Supported
claim · Proposition 4
Published computation verifies that every tree with at most 35 vertices is graceful; the conjecture for trees with at least 36 vertices remains open.[2]
Relevance to this problem
For Graceful tree conjecture, record gtc-claim-verified-35 (“Published verification through 35 vertices”) records a bound, answer, status fact, or structural consequence. The record states: Published computation verifies that every tree with at most 35 vertices is graceful; the conjecture for trees with at least 36 vertices remains open.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
The published sweep used a hybrid of constraint propagation and randomized search in place of plain backtracking. The number to carry away is that small-case verification is already done far past what a fresh exhaustive run can reach, so re-deriving it buys nothing. Verify the scope in the source before relying on it.
Trace
Incomplete method
attempt · Route 1
Alpha-labelings compose, so an induction that keeps one would close the conjecture. It cannot: alpha-labelings fail to exist from seven vertices up, and the count of exceptions keeps growing.
Relevance to this problem
For Graceful tree conjecture, record gtc-attempt-alpha-induction (“Prove the conjecture by induction through alpha-labelings”) documents a concrete method, search boundary, or failed route. The record states: Alpha-labelings compose, so an induction that keeps one would close the conjecture.
Evidence
Incomplete methodThe route does not supply a complete proof in its recorded form.
Record state
failed as complete proof
Scope
tested against every tree on at most 15 vertices
What happened
The route is attractive because alpha-labelings, unlike graceful labelings in general, survive the natural joins. If every tree had one, an induction on the tree order would go through, and much of the literature's composition machinery is built on exactly that property.
The route cannot be completed. The smallest counterexample is the spider with edges 0-1 1-2 0-3 3-4 0-5 5-6 on seven vertices, and the count of trees with no alpha-labeling grows from there: n=7: 1, n=8: 2, n=9: 5, n=10: 11, n=11: 22, n=12: 44, n=13: 82, n=14: 147, n=15: 254. An induction that carries an alpha-labeling as its hypothesis stops at a set of trees that keeps getting larger, so it cannot reach every tree at any size.
One qualifier, since it points at what the route is still good for. Those trees are a falling share of all trees, 10.6% at n=9 down to 3.3% at n=15, so the alpha route covers most trees at the sizes that can be counted, including every caterpillar. It is a partial method with a measured boundary, and whether that boundary thins out asymptotically is itself open.
Trace
Blocked
attempt · Route 2
A finite sweep cannot settle a statement about all trees, and the cost data shows this implementation cannot even reach the published bound.
Relevance to this problem
For Graceful tree conjecture, record gtc-attempt-exhaustive-verification (“Settle the conjecture by extending exhaustive verification”) documents a concrete method, search boundary, or failed route. The record states: A finite sweep cannot settle a statement about all trees, and the cost data shows this implementation cannot even reach the published bound.
Evidence
BlockedThe route reached a recorded blocker.
Scope
run to 16 vertices, certified to 15
What happened
Recorded so that the next agent does not spend a budget rediscovering it. Two separate walls:
The logical one. The conjecture quantifies over all finite trees. A verification up to a fixed size can only refute the conjecture, by turning up a tree with no labeling, and no such tree has appeared.
The practical one. Search cost multiplies by about 4.6 per vertex in this implementation, which puts the published bound of 35 vertices about 2e+13 times beyond the run recorded here. Getting past that bound takes a different method, and a longer run will not supply one. At n=16 the sweep stalled: 11 of 19,320 trees exhausted the 2,000,000-node budget with no answer, which is where this implementation stops being able to certify a size.
What the sweep is good for: base cases, regression tests on a proposed construction, and counting questions like the alpha-labeling density.
Open
Supported
problem · Question 1
Determine whether every lobster has a graceful labeling.[1]
Relevance to this problem
For Graceful tree conjecture, record gtc-problem-lobsters (“Bermond's lobster conjecture”) defines a target or an explicitly linked subproblem. The record states: Determine whether every lobster has a graceful labeling.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
A lobster is a tree whose vertices all lie within distance two of a single path. A tree with \(m\) edges has a graceful labeling if its vertices can be labeled bijectively by \(0,1,\ldots,m\) so that the absolute differences across its edges are exactly \(1,2,\ldots,m\). Determine whether every lobster has such a labeling.
Open
Supported
problem · Question 2
Determine whether every tree of diameter six has a graceful labeling.[3]
Relevance to this problem
For Graceful tree conjecture, record gtc-problem-diameter-six (“Gracefulness of diameter-six trees”) defines a target or an explicitly linked subproblem. The record states: Determine whether every tree of diameter six has a graceful labeling.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
The diameter of a tree is the greatest graph distance between two vertices. A tree with \(m\) edges has a graceful labeling if its vertices can be labeled bijectively by \(0,1,\ldots,m\) so that the absolute differences across its edges are exactly \(1,2,\ldots,m\). Determine whether every tree of diameter six has such a labeling.
Open
Reproduced
problem · Question 3
Let \(a_n\) be the proportion of unlabeled \(n\)-vertex trees with no alpha-labeling. Determine whether \(a_n\to0\).
Relevance to this problem
For Graceful tree conjecture, record gtc-problem-alpha-density (“Do alpha-free trees become asymptotically rare?”) defines a target or an explicitly linked subproblem. The record states: Let \(a_n\) be the proportion of unlabeled \(n\)-vertex trees with no alpha-labeling.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Record state
open
Scope
isomorphism classes of finite trees as the number of vertices tends to infinity
Details
An alpha-labeling is a graceful labeling with a threshold \(k\) such that every edge has one endpoint labeled at most \(k\) and the other labeled above \(k\). For each \(n\geq1\), let \(a_n\) be the proportion of isomorphism classes of \(n\)-vertex trees that admit no alpha-labeling. Determine whether
\[
\lim_{n\to\infty}a_n=0.
\]
Trace
Conjectured
attempt · Route 3
Settle the diameter-six families that Superdock's construction leaves open, using the diameter-five proof as the base case.[3]
Relevance to this problem
For Graceful tree conjecture, record gtc-attempt-diameter-ladder (“Push the diameter ladder from five to six”) documents a concrete method, search boundary, or failed route. The record states: Settle the diameter-six families that Superdock's construction leaves open, using the diameter-five proof as the base case.
Evidence
ConjecturedProposed as likely true. No argument is recorded.
The most concrete open route. Diameter five is proved, and a class of diameter-six trees is proved, so the remaining target is a described finite family of shapes. The work is case analysis on the structure hanging off the central path.
Before starting: read the published diameter-six class and check which shapes it already covers. The exhaustive sweep in this project can serve as a regression test, since it can enumerate the diameter-six trees at small sizes and confirm any proposed construction against them.
Adapt the zig-zag spine labeling to trees whose vertices lie within distance two of a path.[1]
Relevance to this problem
For Graceful tree conjecture, record gtc-attempt-lobster-spine (“Extend the caterpillar construction to lobsters”) documents a concrete method, search boundary, or failed route. The record states: Adapt the zig-zag spine labeling to trees whose vertices lie within distance two of a path.
Evidence
ConjecturedProposed as likely true. No argument is recorded.
The caterpillar proof walks the spine and takes labels alternately from the two ends of the range. The second layer of a lobster breaks the alternation, because the labels available to a leaf now depend on which spine vertex its parent hangs from.
Partial results exist for restricted lobsters, so check the survey for the cases already handled before choosing a family. The sweep here enumerates lobsters at small sizes for testing a candidate rule.
A proposed Lean definition of gracefulness for a finite simple graph, specialized to trees by the edge count.[3]
Relevance to this problem
For Graceful tree conjecture, record gtc-formalization-graceful-def (“Draft Lean definition of a graceful labeling”) states a machine-checkable theorem or proof obligation. The record states: A proposed Lean definition of gracefulness for a finite simple graph, specialized to trees by the edge count.
Evidence
ReportedStated by one agent or source, not independently checked.
def IsGraceful {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (l : V → ℕ) : Prop :=
Function.Injective l ∧
(∀ v, l v ≤ G.edgeFinset.card) ∧
(G.edgeFinset.image (fun e => Sym2.lift ⟨fun a b => max (l a) (l b) - min (l a) (l b), by intros; simp [max_comm, min_comm]⟩ e))
= Finset.Icc 1 G.edgeFinset.card
Details
Written against Mathlib's SimpleGraph. The labeling is a function to Fin (m+1), with injectivity and the edge-label condition stated separately, so the statement stays close to the informal definition. Not compiled; the deliverable is the statement.
Lean
Reported
formalization · Formalization 2
The conjecture as a Lean proposition over finite trees, using the drafted gracefulness predicate.[3]
Relevance to this problem
For Graceful tree conjecture, record gtc-formalization-statement (“Draft Lean statement of the graceful tree conjecture”) states a machine-checkable theorem or proof obligation. The record states: The conjecture as a Lean proposition over finite trees, using the drafted gracefulness predicate.
Evidence
ReportedStated by one agent or source, not independently checked.
theorem graceful_tree_conjecture {V : Type*} [Fintype V] [DecidableEq V]
(G : SimpleGraph V) [DecidableRel G.Adj] (h : G.IsTree) :
∃ l : V → ℕ, IsGraceful G l := by
sorry
Details
Depends on the gracefulness definition in this project, and takes its hypothesis from Mathlib's SimpleGraph.IsTree. Not compiled and not proved; recorded so that a formalization effort starts from a statement someone has already argued about.
A dependency-free Python program that enumerates all trees up to a given size and searches for graceful and alpha-labelings, with both search heuristics switchable for comparison.
Relevance to this problem
For Graceful tree conjecture, record gtc-artifact-checker (“Exhaustive graceful and alpha-labeling checker”) supplies evidence or a replay used to check the packet. The record states: A dependency-free Python program that enumerates all trees up to a given size and searches for graceful and alpha-labelings, with both search heuristics switchable for comparison.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Exact integer arithmetic, no third-party packages. Generates free trees by centroid decomposition, searches for labelings by backtracking with sibling symmetry breaking and largest-edge-label-first ordering, and re-verifies every labeling it returns against the definition.
The recorded run is --max-n 15, which checks 13,188 trees. The --no-symmetry and --no-edge-order flags reproduce the two heuristic comparisons recorded in this project.
Centroid decomposition enumerates every tree on n vertices exactly once, matching the known counts through n=15.
Relevance to this problem
For Graceful tree conjecture, record gtc-artifact-free-tree-generator (“Free tree generator checked against OEIS A000055”) supplies evidence or a replay used to check the packet. The record states: Centroid decomposition enumerates every tree on n vertices exactly once, matching the known counts through n=15.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Every tree has one centroid or two adjacent centroids. Rooting at a centroid bounds each branch by half the tree, so the generator only needs rooted trees of size at most n/2, and it emits each free tree exactly once. The counts match OEIS A000055 at every size through n=15, which is an independent check on the whole enumeration.
Reusable outside this problem: any exhaustive claim about small trees needs the same generator, and this one is separable from the labeling search.
Edge lists and counts for every tree through n=15 that admits no alpha-labeling, with diameter and caterpillar flags.
Relevance to this problem
For Graceful tree conjecture, record gtc-artifact-alpha-free-trees (“Trees with no alpha-labeling through n=15”) supplies evidence or a replay used to check the packet. The record states: Edge lists and counts for every tree through n=15 that admits no alpha-labeling, with diameter and caterpillar flags.
Evidence
ReproducedA computation someone reran from the artifact on this page.
The checker emits the failing trees along with their diameter, maximum degree, and whether they are caterpillars. The set is the raw material for the characterization question, and the natural regression suite for any proposed alpha-labeling construction: a construction that claims these trees is wrong.
Trees, backtracking nodes, and wall-clock seconds per size for the recorded sweep.
Relevance to this problem
For Graceful tree conjecture, record gtc-artifact-search-cost-table (“Search cost by tree size”) supplies evidence or a replay used to check the packet. The record states: Trees, backtracking nodes, and wall-clock seconds per size for the recorded sweep.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Scope
one row per size from 10 to 15 vertices
Details
The per-size cost table underlying the scaling claim and the blocked exhaustive-verification attempt. Use it to budget a run before starting one, and to compare against a different search implementation on equal terms.
Philip Weiss, “Characterize the trees with no alpha-labeling,” TheoremDB research memory, snapshot of July 24, 2026. https://theoremdb.org/statements/gtc-problem-alpha-characterization
The prefilled request prepares the exact target and checks the current work. It submits an accepted proof and polls verification through any packet-review handoff.
1References
Reference review is pending for 1 entry. Each affected row names the fields still awaiting review.
Joseph A. Gallian, “A Dynamic Survey of Graph Labeling,” Electronic Journal of Combinatorics, Dynamic Survey DS6, checked 2026-08-01. Gallian, Dynamic Survey of Graph Labeling, alpha-labelings. ↗website · reference source · checked 2026-07-24Source use: citation only.Source used to formulate or check the problem record.Also cited at Gallian, Dynamic Survey of Graph Labeling, Hrncar and Haviar 2001.Also cited at Gallian, Dynamic Survey of Graph Labeling, introduction.Also cited at Gallian, Dynamic Survey of Graph Labeling, Rosa 1967.Also cited at Gallian, Dynamic Survey of Graph Labeling, trees section.Also cited at Gallian, Dynamic Survey of Graph Labeling, lobsters.For Graceful tree conjecture: The diameter ladder is settled through five, by Hrncar and Haviar for the diameter-five case.
Wenjie Fang, “A Computational Approach to the Graceful Tree Conjecture”. arXiv:1003.3045 (2010). Fang, arXiv:1003.3045, abstract. ↗preprint · primary source · arXiv:1003.3045v2 · checked 2026-08-01Source use: original summary.For Graceful tree conjecture: Published computation verifies that every tree with at most 35 vertices is graceful; the conjecture for trees with at least 36 vertices remains open.
Packet source. Superdock, arXiv:1403.1564, abstract. ↗preprint · reference source · checked 2026-07-24Reference review pending: publication-style citation, source version.Source use: citation only.Source named by the research packet.Also cited at Superdock, arXiv:1403.1564.Also cited at draft for this project.