Order four: the Ehrhart polynomial of the Birkhoff polytope B_4

Proved

MagicSquares.semi_magic_count_four

by Yuxuan Xu · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsehrhartenumerative-combinatoricsmagic-squares

Order four, with the denominators cleared. The counting function $H_{4}(t)$ , the number of $4\times4$ arrays of nonnegative integers whose every row and every column sums to $t$ , is the Ehrhart polynomial of the four-dimensional Birkhoff polytope $B_{4}$ , whose degree is $(4-1)^{2}=9$ . Multiplying by the common denominator $11340$ of its coefficients gives the displayed identity in the natural numbers. The leading coefficient is $11/11340$ , which is $\operatorname{vol}(B_{4})$ ; the normalised volume $9!\cdot\tfrac{11}{11340}$ equals $352$ . This rung is the concrete order at which the general statement can be approached without building any lattice-point machinery.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

theorem semi_magic_count_four (t : ℕ) :
    11340 * semiMagicCount 4 t
      = 11 * t ^ 9 + 198 * t ^ 8 + 1596 * t ^ 7 + 7560 * t ^ 6 + 23289 * t ^ 5
        + 48762 * t ^ 4 + 70234 * t ^ 3 + 68220 * t ^ 2 + 40950 * t + 11340 := by
  sorry

end MagicSquares

Source

M. Beck, M. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717 (arXiv:math/0201013); E. Ehrhart (1973); R. P. Stanley, Duke Math. J. 40 (1973) 607--632; J. Spencer, Amer. Math. Monthly 87 (1980) 397--399; M. Beck and D. Paxton, The Ehrhart polynomial of the Birkhoff polytope (arXiv:math.CO/0202267).

Read-back

What the Lean code literally says, in plain math · deepseek-v4.1-flash (WorkBuddy blind sub-agent)

For every natural number $t$ ,

11340\cdot \operatorname{semiMagicCount}(4,t)=11\,t^{9}+198\,t^{8}+1596\,t^{7}+7560\,t^{6}+23289\,t^{5}+48762\,t^{4}+70234\,t^{3}+68220\,t^{2}+40950\,t+11340.

Here $\operatorname{semiMagicCount}(4,t)$ is the number of $4\times 4$ arrays with entries in $\operatorname{Fin}(t+1)$ (each entry an integer $0,1,\dots,t$ ) whose every row and every column sums to $t$ . All arithmetic in the displayed identity is performed in the natural numbers $\mathbb{N}$ : the multiplication $11340\cdot(\cdot)$ , the powers $t^k$ , the products of coefficients with powers, and the additions on the right-hand side, and the equality is an equality of natural numbers. The theorem asserts only this numerical identity in $\mathbb{N}$ ; it does not, as written, separately assert that the right-hand side is divisible by $11340$ .

Human review

Endorsed by Shuze Chen · Sep 19, 2026
Endorsed by Yuxuan Xu · Sep 19, 2026
Confirmed by the mission captain (proposal self-audit).

View graph