{"id":"palomar/PALOMAR-2026-08-23-000003","url":"https://github.com/novou/square-maximality-palomar/tree/b1d30cdb3334aa7bff7834b22b342393cdc97df8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-23-000003-v1.json","repo":"https://github.com/novou/square-maximality-palomar","tags":["math.CO","msc:05C05","msc:05C30","msc:05C35","spanning-trees","graph-theory","lean-formalization"],"score":0,"title":"novou/square-maximality-palomar","trust":"high","domain":"math.CO","source":"palomar","authors":["Jiechen Zhang"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization of square maximality for spanning trees of induced subgraphs of the square lattice. For every positive integer n and every finite set S of n^2 points in Z^2, the induced lattice graph on S has at most as many spanning trees as the n by n square, with equality exactly when S is a translate of that square. The development also proves the corresponding strict and equality statements for arbitrary spanning subgraphs, together with the finite Matrix--Tree theorem and the proof chain used by the paper.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-23","reactions":{},"formalized":true,"formalizes":[{"title":"Square Maximality for Spanning Trees of Induced Grid Subgraphs","identifier":"","relationship":"formalizes"}]}