Spanning-tree maximizers among square-lattice vertex sets

Among induced square-grid graphs on n² lattice points, does the n×n square have the most spanning trees, with equality only for its translates?

Why it matters and what counts as progress

Why it matters: The unrestricted shape question is stronger than balancing side lengths among rectangles.

What counts as progress: An upper bound for every n²-point lattice set together with the exact equality classification, or a non-square shape with as many or more trees.

How the problem developed

22 May 2026 · Rectangular case [1]
Jiechen Zhang Proved that among rectangular grid graphs with a fixed number of vertices, the most balanced rectangle has the most spanning trees; in particular, an n×n square maximizes among rectangles with n² vertices.
14 Oct 2026 · Generalization [2]
Jiechen Zhang Extended the result to all connected N-vertex sets in the square lattice, characterizing maximizers and proving uniqueness for N≥18; also proved a sharp stability inequality for square sizes.

AI contribution

AI-contributed lemmas help prove square-grid tree maximality

For every n>0 and every set of n² lattice points, the induced square-grid graph has at most as many spanning trees as the n×n square. Equality holds exactly for translates of that square.

AI involvementAI-centered

ImportanceNotable

Technical verificationFormal (Lean 4.32.0 kernel, Comparator and NanoDa + human)

Human understandingFew