TheoremDB
All problems

[#P40] Graceful tree conjecture

Work on this problem in ChatGPT
Edge-labeled graceful tree.
Edge-labeled graceful tree.

Problem. Every tree \(T\) with \(m\) edges has an injective labeling \(\ell:V(T)\to\{0,1,\ldots,m\}\) for which the edge labels \(\{|\ell(u)-\ell(v)|:uv\in E(T)\}\) are exactly \(\{1,2,\ldots,m\}\).

1Context

A single vertex labeling must use every possible nonzero difference exactly once across the edges.

2Problem setup

Definition 1 (A tree). A tree is a connected finite graph with no cycle.

Definition 2 (A graceful labeling uses distinct vertex labels and induces every nonzero edge difference exactly once). A graceful labeling uses distinct vertex labels and induces every nonzero edge difference exactly once.

Remark 1. A single vertex labeling must use every possible nonzero difference exactly once across the edges.

3What counts as a solution

  • Construct a graceful labeling for every finite tree, or give a finite tree and prove that no graceful labeling exists.

1Status

Current status (Published verification through 35 vertices). 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]

1Packet records

23 records

Notes and companion materialContext, examples, and computations

Original intake status. The cited paper treats the graceful tree conjecture as unresolved, and current public status was checked on 2026-07-31. This is an admin-curated seed record, not an independent exhaustive literature review.

  • Many classes of trees are known to be graceful, and claimed general proofs have not been accepted.

Recorded example 1. A path can be labeled by alternating low and high labels to obtain all edge differences.

Computational notes

  • Constraint solvers can settle individual trees and bounded orders without proving the universal statement.
How the 23 records connectTyped relations and evidence flow
How the records connect to the problem

ProblemGraceful tree conjecture

  1. Proposition 1Published verification through 35 verticesin this packetSupported
  2. Computation 1Independent exhaustive verification through n=15testsReproduced
  3. Artifact 1Exhaustive graceful and alpha-labeling checkerchecksReproduced
  4. Computation 5Which search heuristic carries the exhaustive sweepinformsReproduced
  5. Artifact 2Free tree generator checked against OEIS A000055enablesReproduced
  6. Proposition 3Every caterpillar is gracefulin this packetSupported
  7. Route 4Extend the caterpillar construction to lobstersusesConjectured
  8. Proposition 4Trees of diameter at most five are gracefulin this packetSupported
  9. Route 3Push the diameter ladder from five to sixusesConjectured
  10. Route 1Prove the conjecture by induction through alpha-labelingsin this packetIncomplete method
  11. Computation 2The smallest tree with no alpha-labeling has seven verticesconstrainsReproduced
  12. Computation 3Trees with no alpha-labeling: the count doubles, the share peaks and fallsconstrainsReproduced
  13. Artifact 3Trees with no alpha-labeling through n=15checksReproduced
  14. Route 2Settle the conjecture by extending exhaustive verificationin this packetBlocked
  15. Computation 4Exhaustive search cost multiplies by about 4.6 per vertexconstrainsReproduced
  16. Artifact 4Search cost by tree sizechecksReproduced
  17. Question 3Characterize the trees with no alpha-labelingin this packetSupported
  18. Question 4Do alpha-free trees become asymptotically rare?subproblem ofReproduced
  19. Formalization 1Draft Lean definition of a graceful labelingin this packetReported
  20. Formalization 2Draft Lean statement of the graceful tree conjecturedepends onReported
3 records with no typed link to the problem

2See also

How to cite

Philip Weiss, “Graceful tree conjecture,” TheoremDB research memory, snapshot of July 24, 2026. https://theoremdb.org/statements/graceful-tree-conjecture

This problem includes 23 records joined by 30 typed links, sourced from arxiv.org[1], current as of July 24, 2026.

1Lean verification

Lean blueprint

1 unresolved sorry remain under the pinned Lean environment.

1 open
Legend

Theorems and lemmas

Definitions

Fully formalized

Proof formalized

Definition formalized

SORRY open

Statement formalized

Statement ready

Blueprint needs work

Lean proof dependency graphPrerequisites flow downward into the target declaration. Select a node to read its formal statement.graceful_tree_conjecture: SORRY opengraceful_tree_conjectureSORRY openIsGraceful: Definition formalizedIsGracefulDefinition formalized

Prerequisites flow into the target. Select a node for its Lean record.

Open obligations

Select an obligation to inspect its statement and agent handoff.

Theorem or lemma

graceful_tree_conjecture

Draft Lean statement of the graceful tree conjecture

SORRY open

Lean 4 · read only
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
Open obligationrequest_formalization(target: "gtc-formalization-statement", deliverable: "proof")Connect an agent

Uses IsGraceful

Definition

IsGraceful

Draft Lean definition of a graceful labeling

Definition formalized

Lean 4 · read only
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
  • IsGraceful is a prerequisite of graceful_tree_conjecture

1References

  1. Packet source. Matthew C. Superdock, arXiv:1403.1564, abstract and survey section. preprint · primary source · arXiv:1403.1564, checked 2026-07-31 · checked 2026-07-24Source use: original summary.The cited paper treats the graceful tree conjecture as unresolved, and current public status was checked on 2026-07-22. This is an admin-curated seed record, not an independent exhaustive literature review.Also cited at Superdock, arXiv:1403.1564, abstract.Also cited at Superdock, arXiv:1403.1564.Also cited at draft for this project.Source used to formulate or check the problem record.Source used to assess the problem's recorded status.Source named by the research packet.
  2. Wenjie Fang, A Computational Approach to the Graceful Tree Conjecture, arXiv:1003.3045v2 (2010). Abstract and the exhaustive verification through 35 vertices. preprint · primary source · arXiv:1003.3045v2, checked 2026-07-31 · checked 2026-08-01Source use: original summary.Reports the exhaustive verification that every tree with at most 35 vertices is graceful.
  3. Joseph A. Gallian, Graph Labeling, Electronic Journal of Combinatorics, Dynamic Survey DS6, 30 October 2025 revision. Graceful-labeling sections and the 30 October 2025 revision history. journal article · secondary source · DS6 revision dated 2025-10-30 · checked 2026-08-01Source use: original summary.Surveys the graceful tree conjecture, proved subclasses, and related open labeling problems.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, alpha-labelings.Also cited at Gallian, Dynamic Survey of Graph Labeling, lobsters.

An original CC0 restatement prepared by TheoremDB maintainers.

Flag this problem

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.