ProofAtlas

Graph theory · linear algebra · formal theorem

Kirchhoff’s Matrix-Tree Theorem

For any finite simple graph and chosen root, the determinant of the integer reduced Laplacian equals the number of spanning trees.

Lean proofpassed
Unfinished proof stepsNone
Formal resultAccepted
Matrix-tree theorem statement mapDeleting one row and column from a finite simple graph's Laplacian produces a determinant that counts its spanning trees.
Exact scope: For every finite simple graph and chosen root, the determinant of the integer reduced Laplacian equals the number of spanning trees.

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.

The theorem at a glance

Kirchhoff’s Matrix-Tree Theorem at a glance

Editorial theorem poster connecting a finite graph, its reduced Laplacian, determinant expansion, and the count of spanning trees.
Kirchhoff’s Matrix-Tree Theorem turns one reduced Laplacian determinant into the number of spanning trees.

Accessible transcript

det (reducedLaplacian G root) = Nat.card (SpanningTree G)

For a finite simple graph and any chosen root, the determinant of the integer reduced Laplacian equals the number of spanning-tree subgraphs.

Read the complete poster transcript

GRAPH THEORY · LINEAR ALGEBRA

KIRCHHOFF’S MATRIX–TREE THEOREM

ONE DETERMINANT COUNTS EVERY SPANNING TREE

FOR EVERY FINITE SIMPLE GRAPH G AND ROOT r

det(L_r) = |SpanningTree(G)|

THE REDUCED LAPLACIAN

L_ii = degree(i)

L_ij = −1 if i ∼ j

L_ij = 0 otherwise

Delete the row and column indexed by r.

THE COMBINATORIAL MEANING

Each determinant term chooses one edge at every non-root vertex.

Cycles cancel. Root-directed choices contribute 1.

HOW THE PROOF MOVES

1 · FACTOR THE LAPLACIAN

2 · EXPAND THE DETERMINANT

3 · CANCEL CYCLIC CHOICES

4 · IDENTIFY ROOTED CHOICES

5 · COUNT THE SPANNING TREES

EXACT SCOPE

Finite simple graphs, integer Laplacian, and any chosen root.

Spanning trees use every vertex and only edges of G.

Theorem schematic

A cofactor counts spanning trees

A complete four-vertex graph leads through a three-by-three reduced Laplacian cofactor to four distinct spanning trees.
For K4, deleting one Laplacian row and column gives a cofactor whose determinant counts its spanning trees.

det (reducedLaplacian G root) = Nat.card (SpanningTree G)

A chosen root fixes one reduced Laplacian cofactor. Its determinant counts the spanning-tree subgraphs of the same graph.

Proof architecture

How a determinant filters edge choices into spanning trees

7 curated stages

The checked proof factors the reduced Laplacian through signed incidence, expands its determinant into edge choices, eliminates invalid and cyclic terms, evaluates every root-reaching survivor as one, and identifies those survivors exactly with spanning trees.

These source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.

  1. A rooted wheel graph is tethered to a signed-incidence grid whose root row is removed before multiplication by its transpose.
    The reduced Laplacian factors as the reduced signed-incidence matrix times its transpose.
    01

    The cofactor is a signed-incidence Gram determinant

    reducedSignedIncidence G root ⬝ (reducedSignedIncidence G root)ᵀ = reducedLaplacian G root

    Deleting the root row from the signed-incidence matrix produces a rectangular matrix whose Gram product is the reduced Laplacian.

    Lean lemmas for this step
    • reducedSignedIncidence
    • signedIncidence_mul_transpose_eq_laplacian
    • reducedSignedIncidence_mul_transpose_eq_reducedLaplacian
  2. Columns tethered to graph edges fan into one selected incident edge for each non-root vertex.
    Determinant expansion becomes a finite sum over edge-choice functions.
    02

    Expansion becomes edge choice

    det (Bᵣ Bᵣᵀ) = ∑ f, det(Bᵣ[f]) · det(Bᵣ[f]ᵀ)

    The rectangular determinant expansion selects one graph-edge column for each non-root vertex and squares the resulting signed-incidence minor.

    Lean lemmas for this step
    • det_mul_rectangular_apply
    • signedIncidenceMinorTerm
    • signedIncidenceMinorSum
    • reducedSignedIncidence_det_functionSum
  3. Two invalid edge-choice routes terminate: repeated columns and an edge not incident to its source.
    Non-injective choices and non-incident choices contribute zero.
    03

    Immediate invalid choices vanish

    not injective f or not incident f ⟹ signedIncidenceMinorTerm G root f = 0

    Repeated selected columns force a singular minor, while a selected edge not incident to its source forces the relevant diagonal factor to vanish.

    Lean lemmas for this step
    • signedIncidenceMinorTerm_eq_zero_of_not_injective
    • signedIncidenceMinorTerm_eq_zero_of_not_incident
  4. A non-root-reaching directed orbit inside the wheel repeats and closes into a highlighted cycle.
    Any injective incident choice that fails to reach the root contains a finite periodic obstruction.
    04

    Failure to reach the root produces a cycle

    not root-reaching ⟹ ∃ periodic orbit with minimal period k ≥ 3

    Iterating the chosen other-endpoint map inside the finite set of vertices that do not reach the root yields a minimal periodic orbit of length at least three.

    Lean lemmas for this step
    • edgeChoiceNext
    • exists_edgeChoiceNext_periodic_reachable
    • exists_edgeChoiceNext_minimal_periodic_reachable_three_le_of_injective
  5. Oppositely signed incidence contributions cancel around one selected cycle and collapse its determinant term to zero.
    Signed-incidence columns along the periodic cycle satisfy a nontrivial zero relation.
    05

    Signed incidence cancels around the cycle

    cycle relation ⟹ signedIncidenceMinorTerm G root f = 0

    Around the minimal selected cycle, each incoming signed-incidence contribution cancels the outgoing contribution, giving a column relation that annihilates the minor determinant.

    Lean lemmas for this step
    • signedIncidence_edgeChoiceNext_cycle_sum_eq_zero
    • det_reducedSignedIncidence_submatrix_eq_zero_of_edgeChoiceNext_cycle
    • signedIncidenceMinorTerm_eq_zero_of_cycle
  6. One exact root-directed six-edge path on a seven-node wheel flows inward to the double-ring root.
    A root-reaching incident choice selects a spanning tree and contributes exactly one to the determinant sum.
    06

    Root-reaching choices contribute one

    root-reaching f ⟹ signedIncidenceMinorTerm G root f = 1

    Every non-root vertex selects one incident edge leading one distance step closer to the root. Distance ordering makes the selected reduced-incidence minor triangular, and its squared determinant is one.

    Lean lemmas for this step
    • rootReachableEdgeChoice_dist_otherVertex_lt
    • rootReachableEdgeChoice_submatrix_blockTriangular
    • rootReachableEdgeChoice_submatrix_det_eq_diagProduct
    • signedIncidenceMinorTerm_eq_one_of_rootReachableEdgeChoice
  7. The same six-edge root-directed path and undirected spanning tree are paired in both directions on the original wheel graph.
    Each root-reaching choice determines one spanning tree, and each spanning tree has a unique parent edge toward the root.
    07

    Root-directed choices are spanning trees

    RootReachableEdgeChoice G root ≃ SpanningTree G

    Forgetting directions maps every root-reaching choice to a spanning tree. Orienting each spanning-tree edge toward the chosen root recovers the unique inverse choice.

    Lean lemmas for this step
    • rootReachableEdgeChoiceSpanningTree
    • rootReachableEdgeChoiceOfSpanningTree
    • rootReachableEdgeChoiceSpanningTree_surjective
    • rootReachableEdgeChoiceSpanningTree_injective
    • rootReachableEdgeChoice_card_eq_spanningTree_card
    • signedIncidenceMinorSum_eq_spanningTree_card

Exact formal proposition

Hypotheses and conclusion

theorem matrixTreeTheorem : MatrixTreeTheoremStatement

Result boundary

What this page does—and does not—establish

For every finite simple graph and chosen root, the determinant of the integer reduced Laplacian equals the number of spanning trees.

About these visual explanations

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.

Continue the mathematics

Start from the complete checked source

The pinned theorem and its complete local import closure let internal and external agents inspect the proof, compare an alternate route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks every proposed extension against its exact formal statement.

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled.

Checked source + agent continuation package · 1 Lean file · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Formal-result publication and review details

Independent publication review

The formal theorem's publication gates are accepted

Lean checks the proof. Independent AI review separately accepted evidence completeness, statement alignment, result boundary, and the retained theorem wording. Those gates apply to the formal result; generated media is reviewed and promoted separately. Neither review replaces Lean's proof check or broadens the theorem.

01

Formal evidence

Independent review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.

02

Statement alignment

The formal declaration was accepted against the named theorem and its exact variant.

03

Result boundary

The accepted boundary keeps nearby stronger or commonly confused claims out of scope.

04

Public wording

Independent review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.

05

Canonical source

The first-party source link is pinned to the checked package commit and exact Lean file.

06

Accepted result

A validated accepted-result record binds the four reviews to the checked formalization.

Expanded visual

Open original image in a new tab