{"id":"palomar/PALOMAR-2026-10-16-000019","url":"https://github.com/jtraverso/matrix-tree/tree/aeab0f267c523dd3cac9a287b589f65a99d20d01","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000019-v1.json","repo":"https://github.com/jtraverso/matrix-tree","tags":["math.CO","msc:05C05","msc:05C30","msc:05C50","msc:15A15","combinatorics","matrix-tree-theorem","lean-formalization","spanning-trees"],"score":0,"title":"The Cauchy–Binet formula, Kirchhoff's matrix-tree theorem and Cayley's formula","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the Cauchy–Binet formula for determinants of products of rectangular matrices over commutative rings (not in Mathlib), of Kirchhoff's matrix-tree theorem (the number of spanning trees of a finite graph is any principal cofactor of Mathlib's Laplacian matrix), and of Cayley's formula (n^(n−2) labelled trees on n ≥ 1 vertices), derived from the matrix-tree theorem for the complete graph.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Ueber die Auflösung der Gleichungen, auf welche man bei der Untersuchung der linearen Vertheilung galvanischer Ströme geführt wird","identifier":"doi:10.1002/andp.18471481202","relationship":"formalizes"},{"title":"A theorem on trees","identifier":"","relationship":"formalizes"},{"title":"Mémoire sur un système de formules analytiques, et leur application à des considérations géométriques","identifier":"","relationship":"formalizes"},{"title":"Mémoire sur les fonctions qui ne peuvent obtenir que deux valeurs égales et de signes contraires par suite des transpositions opérées entre les variables qu'elles renferment","identifier":"","relationship":"formalizes"}]}