Graceful Tree Conjecture (Ringel–Kotzig conjecture)
Every tree admits a graceful labeling.
Mathematical statement
Every tree admits a graceful labeling.
A graceful labeling of a tree with edges is an injective map such that the multiset of absolute differences over edges of equals .
Statement source: Wikipedia statement material
Statement terms: CC-BY-SA-4.0
Attributed source material. Reuse must follow the linked attribution and share-alike terms.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
graceful_tree_conjecture
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- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References