The counting function of semi-magic squares is a polynomial

Proved

MagicSquares.semi_magic_polynomial_exists

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

combinatoricsehrhartenumerative-combinatoricsmagic-squares

Existence and degree, uniformly in the order. For every $n\ge 1$ there is a polynomial $p\in\mathbb{Q}[X]$ , of degree exactly $(n-1)^{2}$ , whose value at each nonnegative integer $t$ is the number $H_{n}(t)$ of $n\times n$ semi-magic squares of line sum $t$ . The degree $(n-1)^{2}$ is the dimension of the Birkhoff polytope $B_{n}$ , and the integrality of its vertices is what makes the period one, so that the counting function is a polynomial and not merely a quasi-polynomial. This is the first half of the goal, isolated so that it can be attacked on its own.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

theorem semi_magic_polynomial_exists (n : ℕ) (hn : 1 ≤ n) :
    ∃ p : Polynomial ℚ,
      p.natDegree = (n - 1) ^ 2 ∧
        ∀ t : ℕ, p.eval (t : ℚ) = (semiMagicCount n t : ℚ) := 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)

Let $n$ be a natural number and assume the hypothesis $1\le n$ . Then there exists a polynomial $p\in\mathbb{Q}[X]$ such that two conditions hold. First, the natural degree of $p$ equals $(n-1)^2$ , where the subtraction $n-1$ is the natural-number subtraction (guaranteed non-negative by the assumption $1\le n$ ). The natural degree $\operatorname{natDegree}(p)$ is defined to be $0$ when $p$ is the zero polynomial and otherwise equals the ordinary degree; consequently this condition forces $p$ to be non-zero with ordinary degree exactly $(n-1)^2$ . Second, for every natural number $t$ , evaluating $p$ at the rational number obtained by lifting $t$ to $\mathbb{Q}$ equals $\operatorname{semiMagicCount}(n,t)$ also coerced to $\mathbb{Q}$ . (As above, $\operatorname{semiMagicCount}(n,t)$ counts the $n\times n$ arrays over $\operatorname{Fin}(t+1)$ whose every row and column sums to $t$ .)

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