Enumerative graph theory · formal theorem
For every n ≥ 1, the number of labeled unrooted trees on the vertex set Fin n is exactly n^(n − 2).
Scope: For every natural number n with 1 ≤ n, the number of labeled unrooted trees on Fin n is n^(n − 2).
Exact formal proposition
theorem cayleyTreeFormula : CayleyTreeFormulaStatementProof route
The checked proof turns labeled trees into Prüfer codes by repeatedly deleting one canonical leaf, builds an exact decoder with a final-pair step, proves both state machines are inverse, and transfers the code-space cardinality back to trees.
These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.
LabeledTree (n + 2) ≃ PruferCode (n + 2)
The proof separates the one-vertex boundary case and reduces the main count to an equivalence between trees and functions from n−2 positions into the labels.
PruferCodepruferCode_natCardlabeledTree_one_natCardpruferEquiv
chosenStep emits the neighbor label and erases the chosen leaf
The left tree has eight vertices and seven edges. The blue leaf ℓ has degree one and is directly incident to gold vertex 4. In the right tree, ℓ and that edge are absent; the same seven other vertices and six edges remain connected and acyclic, and 4 becomes a leaf. A gold guide from vertex 4 enters the single code tile labeled 4.
chosenLeafPruferState.chosenStepPruferState.chosenStep_labelFinset_eq_erase_chosenLeaf
pruferEncodeState records an ordered head and recursive tail
Successive encoder states erase STAR, SQUARE, and DIAMOND. Their neighbors become the ordered code prefix while original labels persist.
PruferState.labelFinsetPruferState.liftedGraphpruferEncodeState_succ_zeropruferEncodeState_succ_tail
pruferDecodeTree : PruferCode (n + 2) → LabeledTree (n + 2)
The decoder joins the least remaining label absent from the tail to the current head. Six recursive edges and the final pair produce a tree.
decodeLeafPruferDecodeState.stepPruferDecodeState.finishpruferDecodeGraph_isTreepruferDecodeTree
decode (encode T) = T and encode (decode c) = c
State invariants align the chosen leaf with the least missing label at every step, proving both inverse laws.
PruferState.decodeLeaf_encode_eq_chosenLeaf_labelpruferDecodeState_encode_graph_sup_final_liftedGraph_eqpruferEncode_decodeTree_succpruferEquiv
Nat.card (LabeledTree n) = n ^ (n − 2)
The equivalence transfers the code-space cardinality to labeled trees; the one- and two-vertex cases are handled separately in the source.
pruferCode_natCardpruferEquivlabeledTree_one_natCardcayleyTreeFormulaThe theorem at a glance
Accessible transcript
Nat.card (LabeledTree n) = n ^ (n − 2)
For every n at least one, the number of finite simple trees on the labeled vertex type Fin n is n raised to n minus two. The proof builds an encoder, decoder, and both inverse laws.
COMBINATORICS · LABELED TREES
CAYLEY’S FORMULA
HOW MANY TREES ON n LABELED VERTICES?
FOR EVERY n ≥ 1
|LabeledTree(n)| = n^(n − 2)
PRÜFER CODES
A tree on n ≥ 2 vertices corresponds to a sequence of length n − 2 with entries in Fin n.
LEAF → NEIGHBOR
Remove the least leaf and record its unique neighbor.
CODE → TREE
Reconnect the least missing remaining label, then join the final two labels.
WHY THE COUNT IS n^(n − 2)
n choices for each of n − 2 positions.
HOW THE PROOF MOVES
1 · CHOOSE THE LEAST LEAF
2 · ENCODE ITS NEIGHBOR
3 · REBUILD FROM THE CODE
4 · PROVE BOTH INVERSE LAWS
5 · TRANSFER CARDINALITY
EXACT SCOPE
Finite simple trees on the labeled vertex type Fin n. Counts labeled trees, not unlabeled tree shapes.
Theorem schematic
Labeled trees on n vertices ↔ Prüfer codes of length n − 2
The least current leaf is removed while its unique neighbor is recorded. Repetition produces an ordered code, and reversing the state changes reconstructs the labeled tree.
Result boundary
For every natural number n with 1 ≤ n, the number of labeled unrooted trees on Fin n is n^(n − 2).
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Review record
Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.
The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
The formal declaration was accepted against the named theorem and its exact variant.
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
The first-party source link is pinned to the checked package commit and exact Lean file.
A validated accepted-result record binds the four reviews to the checked formalization.