Motivation

Counting the trees on a fixed, labeled vertex set is one of the oldest enumeration problems in graph theory. Cayley stated the count in 1889 while enumerating isomers of saturated hydrocarbons — each tree corresponds to a possible carbon skeleton — and the same number reappears throughout combinatorics as the number of spanning trees of the complete graph $K_n$, a special case of Kirchhoff's Matrix–Tree Theorem, and as the base case against which more refined tree-counting results (trees with a prescribed degree sequence, forests, spanning trees of general graphs) are measured.

Several independent proofs of the count are known — a direct recursive argument, a determinant computation via the Matrix–Tree Theorem, a double-counting argument on increasing trees — and each exposes a different piece of structure. This mission formalizes the proof via Prüfer sequences, due to Prüfer (1918): an explicit, computable bijection between labeled trees and certain finite sequences, presented here following Gross and Yellen, Graph Theory and Its Applications, 3rd ed. (CRC Press, 2018), Section 3.7, pp. 157–162.

Setting

Fix $n \geq 2$ and take the vertex set to be $\{1, \dots, n\}$ (formalized as Fin n). A labeled tree on $n$ vertices is a simple graph $T$ on this vertex set that is connected and acyclic (Mathlib's SimpleGraph.IsTree). Two labeled trees are the same exactly when their edge sets coincide — the two 4-vertex trees in Figure 3.7.1 of the source are both paths but are different labeled trees, since the labels sit on different vertices.

A Prüfer sequence of length $n - 2$ is any sequence $(s_1, \dots, s_{n-2})$ of labels drawn from $\{1, \dots, n\}$, repetitions allowed (so there are $n^{n-2}$ of them, by the rule of product).

The encoding of a tree $T$ (Algorithm 3.7.1, p. 157) builds its Prüfer sequence by repeating, $n-2$ times: find the leaf (degree-one vertex) with the smallest label among those not yet removed, record the label of its neighbor, then delete that leaf. The decoding of a sequence (Algorithm 3.7.3, p. 159) reverses this: it rebuilds the tree edge by edge, at each step joining the smallest label not yet used and not appearing later in the sequence to the next label in the sequence, finishing by joining the two labels left over.

Formalization targets

Goal — Cayley's Tree Formula (Theorem 3.7.5, p. 162)

$$\operatorname{Nat.card}\, \{T : \text{SimpleGraph}(\text{Fin } n) \mid T.\text{IsTree}\} = n^{\,n-2}, \qquad n \geq 2.$$

This is the weakest stable statement: it is exactly the count Cayley identified, phrased without reference to any particular proof method, so it is not tied to properties of Prüfer sequences beyond what is needed to establish the count.

Significance

The identity itself is foundational: it is the base case of Kirchhoff's Matrix–Tree Theorem (which computes the analogous count for spanning trees of an arbitrary graph as a cofactor of its Laplacian) and it appears as an ingredient in random graph theory (counting spanning trees of $K_n$ bounds the number of ways a random graph process can build a tree) and in the analysis of algorithms on trees, where the Prüfer encoding itself is used as a compact serialization of a labeled tree.

The result has been proved by hand for over a century, and its most classical proof (the one formalized here) has not, to this project's knowledge, appeared as a machine-checked Lean proof; Mathlib's Combinatorics.SimpleGraph library has the tree and acyclicity infrastructure this mission builds on, but not the Prüfer bijection or the count itself. Formalizing it here means constructing the encoding and decoding maps explicitly as computable, total recursive functions, and proving they are mutually inverse — the mission's four milestones below are exactly the four supporting results the source uses for this.

Difficulty

The obvious first attempt is to define the encoding by structural recursion, peeling one leaf per step, but this immediately runs into a dependent-typing obstacle: after deleting a vertex, the "remaining graph" naturally lives on a smaller vertex type, so a naive recursive definition changes type at every step and the final sequence's type (length $n-2$) is not visible to the recursion by construction. The formalization here sidesteps this by keeping the ambient vertex type fixed at Fin n throughout and tracking the shrinking set of "active" vertices as an ordinary Finset (Fin n) parameter, so the recursion is on a natural number step-counter rather than on the type itself; the price is that every step's "leaf" and "neighbor" must be picked out by an explicit Finset.filter/Finset.min computation whose well-definedness (there is always a smallest active leaf, and it always has a unique active neighbor) is exactly the content of Propositions 3.7.1 and 3.7.3 below, rather than something the type system gives for free. The inverse direction has the dual issue in reverse: decoding recurses structurally on the sequence while tracking a shrinking label set, and showing the two recursions undo each other (Proposition 3.7.4) requires the same induction run in both directions simultaneously.

Formalization scope

Trees are SimpleGraph (Fin n) satisfying Mathlib's SimpleGraph.IsTree; no alternate, weaker notion of "tree" is used. Prüfer sequences are functions Fin (n - 2) → Fin n (equivalently, by Fintype.card_fun, exactly the $n^{n-2}$ count needed) rather than List or Vector, so that the final counting step is immediate once the bijection is established. The encoding and decoding functions (pruferEncode, pruferDecode) are supplied as noncomputable definitions in Definitions.Def_GYGraphTheory — noncomputable only because Prop-level decidability of a general SimpleGraph.Adj is classical, not because the algorithm is non-constructive; every step is the literal Prüfer procedure, junk-valued (defaulting to label 0) outside its intended domain in exactly the way a hand proof would say "this step is meaningless once fewer than two active vertices remain." The four milestones give the precise faithful statements of the source's Propositions 3.7.1, Corollary 3.7.2, Proposition 3.7.3, and Proposition 3.7.4; the goal theorem is the immediate corollary once all four are in hand, via Fintype.card_congr and Fintype.card_fun. A trivializing formalization is not available here: IsTree is Mathlib's standard, non-vacuous notion, and the milestones pin down pruferEncode and pruferDecode to the source's specific algorithm rather than leaving the bijection's existence as a free black box. Beyond the four milestones, a full development needs: basic Finset/List manipulation lemmas relating pruferPeel's step-indexed recursion to pruferDecodeAux's list-indexed recursion (reusable in any future mission touching Prüfer-style encodings); and the final cardinality argument tying the bijection to n ^ (n - 2). Contributions connecting this formula to Mathlib's general Matrix–Tree machinery (if and when it exists) would be a natural, welcome extension but are out of scope for this mission.

Selected references

• A. Cayley, A theorem on trees, Quart. J. Math. 23 (1889), 376–378.
• H. Prüfer, Neuer Beweis eines Satzes über Permutationen, Archiv der Mathematischen Physik 27 (1918), 742–744.
• J.L. Gross and J. Yellen, Graph Theory and Its Applications, 3rd ed., CRC Press, 2018, Section 3.7 "Counting Labeled Trees: Prüfer Encoding", pp. 157–162.