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.

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

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
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.

Exact formal proposition

Hypotheses and conclusion

theorem matrixTreeTheorem : MatrixTreeTheoremStatement

Proof route

How a determinant filters edge choices into spanning trees

7 proof 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 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.

  1. Scientific figure illustrating: The reduced Laplacian factors as the reduced signed-incidence matrix times 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. A text-free field of colored column strips branches into several schematic selections that converge into a combined group; no numerical matrix or graph example is specified.
    Determinant expansion becomes a finite sum over edge-choice functions.
    02

    Expansion becomes edge choice

    det (Bᵣ Bᵣᵀ) = ∑ f : U → E(G), det(Bᵣ[f]) · ∏ v ∈ U, Bᵣ[v, f(v)]

    Let U be the non-root vertices. Each function f from U to graph edges selects one column for each vertex. Its summand is the determinant of that selected-column matrix multiplied by the product of entries Bᵣ[v, f(v)], not a squared minor. The image illustrates selection only; the exact weighted expansion is written below.

    Lean lemmas for this step
    • det_mul_rectangular_apply
    • signedIncidenceMinorTerm
    • signedIncidenceMinorSum
    • reducedSignedIncidence_det_functionSum
  3. Scientific figure illustrating: Non-injective choices and non-incident choices contribute zero.
    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. Gold arrows show the selected other-endpoint map trapped away from root r. Blue dotted arrows toward r are unselected ambient connections, not steps of that map. The selected orbit yields a gold cycle v1 → v2 → v3 → ⋯ → vk → v1, with k ≥ 3.
    Gold arrows are selected steps; blue dotted arrows toward r are unselected ambient connections. An 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

    The dashed region represents vertices that do not reach the root under the selected gold-arrow map; blue dotted connections to r are not selected steps. Iterating this map within that finite set 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. A planar four-vertex complete graph has a central double-ring root and a clockwise directed triangle on its three non-root vertices. Beside it is the reduced incidence matrix with rows (-1, 0, 1), (1, -1, 0), and (0, 1, -1), whose row and column sums are 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. Scientific figure illustrating: A root-reaching incident choice selects a spanning tree and contributes exactly one to the determinant sum.
    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. Scientific figure illustrating: Each root-reaching choice determines one spanning tree, and each spanning tree has a unique parent edge toward the root.
    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

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

Scientific figure illustrating: For K4, deleting one Laplacian row and column gives a cofactor whose determinant counts its 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.

Result boundary

What this theorem 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.

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

Open questions and extensions

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.

What the source ZIP contains

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.

Complete checked Lean source · 1 Lean file · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Publication review

Review record

Publication reviews accepted

Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.

01

Formal evidence

The formal-evidence 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

The public-wording 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