Motivation

The magic-square programme already on this platform works at fixed small orders: MacMahon's enumeration of the $3\times3$ squares, both the magic count $M_{3}(3e)=2e^{2}+2e+1$ and the semi-magic count $H_{3}(t)=3\binom{t+3}{4}+\binom{t+2}{2}$; the classification of the normal $3\times3$ squares; and the counts of the panmagic and symmetric order-three classes. Each of those is a statement about a single order. This mission changes the axis: it asks what the counting function does when the order itself is allowed to vary.

Timeline.

• 1915 — MacMahon determines $H_{3}$ and $M_{3}$ explicitly [MacMahon 1960].
• 1966 — Anand, Dumir and Gupta conjecture that $H_{n}(t)$, as a function of the line sum $t$, is a polynomial of degree $(n-1)^{2}$ for every order $n$ [Anand-Dumir-Gupta 1966].
• 1973 — the conjecture is proved independently by Ehrhart, from linear Diophantine systems [Ehrhart 1973], and by Stanley, from linear homogeneous Diophantine equations and the magic labelings of graphs [Stanley 1973].
• 1980 — Spencer gives an elementary proof [Spencer 1980].
• 2002–2003 — Beck and Pixton compute the Ehrhart polynomial of the Birkhoff polytope at order four [Beck-Pixton 2002]; Beck, Cohen, Cuomo and Gribelyuk extend the structural picture to the magic, symmetric and pan-diagonal counts, which are quasi-polynomials rather than polynomials [BCCG 2003].

That split is the point of the mission, so it is worth naming before anything is proved. A quasi-polynomial of degree $d$ and period $m$ agrees with a degree-$d$ polynomial on each residue class modulo $m$, the polynomials differing between classes; a polynomial is the case $m=1$. For the magic squares the values do depend on $t$ modulo a period — at order three $M_{3}(t)$ vanishes unless $3\mid t$ — and the same is true of every other class. For $H_{n}$ it never happens.

Setting

An $n\times n$ semi-magic square of line sum $t$ is an $n\times n$ array of nonnegative integers in which every row and every column sums to $t$. Entries may repeat, and no condition is placed on the diagonals. Write $H_{n}(t)$ for the number of such arrays.

In Lean the array is a Square n ℕ, that is, a Matrix (Fin n) (Fin n) ℕ; the condition is IsSemiMagic M t, which asks every rowSum and every colSum to equal t; and the counting function is semiMagicCount n t, the cardinality of the finset of all arrays over Fin (t + 1) satisfying IsSemiMagic. Restricting the entries to Fin (t + 1) loses nothing, since an entry of a square of line sum $t$ is at most $t$.

Dividing by $t$ turns such an array into a doubly stochastic matrix, a nonnegative real matrix whose every row and column sums to $1$. So $H_{n}(t)$ is equally the number of lattice points in the $t$-fold dilation of the Birkhoff polytope $B_{n}$. Two geometric facts about $B_{n}$ are what the mission is about. Its dimension is $(n-1)^{2}$: the $n^{2}$ entries satisfy $2n$ line equations, exactly one of which is dependent. Its vertices are the $n!$ permutation matrices, by the Birkhoff–von Neumann theorem, hence integral. The mission states that both facts are visible in the arithmetic of $H_{n}$.

Formalization targets

Goal — the counting function is a polynomial

$$\exists\, p\in\mathbb{Q}[X]:\quad \deg p=(n-1)^{2},\qquad p(t)=H_{n}(t)\ \text{ for all }t\in\mathbb{N},$$ $$p(-n-t)=(-1)^{n-1}p(t)\ \text{ for all }t\in\mathbb{Z},\qquad p(-1)=p(-2)=\cdots=p(-n+1)=0 .$$

This is Theorem 1 of [BCCG 2003], stated there for $n\ge 1$. It is the shape of the truth, not a closed form, so no later improvement of the explicit formulas can invalidate it. The three parts are not independent: the degree is the dimension of $B_{n}$, and the two identities are the reciprocity law for lattice-point counting, applied to $B_{n}$.

The intermediate rungs

The goal is far from the easy cases, and the mission is laid out so that each rung is an independently provable statement.

• Order one. $H_{1}(t)=1$: a $1\times1$ array of line sum $t$ is just $[t]$.
• Orders two and three. Already proved on the platform, as MagicSquares.semi_magic_count_two ($H_{2}(t)=t+1$) and MagicSquares.semi_magic_count_three (MacMahon's $H_{3}(t)=3\binom{t+3}{4}+\binom{t+2}{2}$). Included as references, not as targets.
• Order four, with the denominators cleared so that it is an identity between natural numbers:

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

Its leading coefficient is $\tfrac{11}{11340}=\operatorname{vol}(B_{4})$ and its normalised volume is $352$.

• Existence and degree, uniformly in $n$. The polynomial exists, with degree exactly $(n-1)^{2}$.
• The reciprocity identity and the vanishing list, for that polynomial.

Significance

The result itself. The theorem makes the semi-magic squares countable in closed form at every order, and it is why the semi-magic count can be tabulated as a polynomial while the magic, symmetric and pandiagonal counts cannot: a polynomial is determined by finitely many values, a quasi-polynomial is not without knowing its period. The reciprocity identities are the same statement seen from the interior of $B_{n}$, which is why they are what pins an explicit polynomial down once its degree is known. The order-four polynomial above was verified against direct enumeration on seventeen values of $t$; that verification is evidence, not proof, and is recorded because the general statement is what has to be proved.

Formalizing it. The theorem has been known since 1973 and has had an elementary proof since 1980; what does not exist anywhere is a machine-checked proof. Mathlib contains no Ehrhart theory, no quasi-polynomial machinery and no rational-generating-function toolbox — the string "Ehrhart" does not occur in it — so a formalization must construct its own lattice-point-counting argument for this family of polytopes, or find an elementary route that avoids polytopes altogether. Either outcome is reusable: the same absence blocks the quasi-polynomial counts $M_{n}$, $S_{n}$ and $P_{n}$ of BCCG's Theorem 2, which the earlier missions approach only at order three.

Difficulty

The first idea anyone has is to interpolate: compute $H_{n}(t)$ for enough values of $t$ and fit a polynomial. That works, and it is how the order-four rung was produced, but it cannot prove the general statement: the degree is what is being asserted, so the number of values needed is not known in advance, and with $n$ itself a variable no finite computation settles it. Interpolation is legitimate as a target at order four; it must not be mistaken for a route to the goal.

The second idea is to import the geometry as a black box: a rational polytope dilated by $t$ has a counting function that is a quasi-polynomial of degree equal to its dimension, with period dividing the least common multiple of the vertex denominators. That is Ehrhart's theorem, and it is the textbook route. It is not available here, and reconstructing it in general is a larger project than this mission; the statements the mission asks for are the ones that survive without it.

The part of the goal with no counting interpretation at all is the second line. $H_{n}$ is defined on $\mathbb{N}$; the assertion that a polynomial agreeing with it there vanishes at $-1,\dots,-(n-1)$ and satisfies $p(-n-t)=(-1)^{n-1}p(t)$ is a statement about the interior of the polytope, and it cannot be read off from the combinatorial definition. A solver who proves only the polynomiality and the degree has not finished the goal.

Formalization scope

The formalization commits to the following conventions.

• The counting function is semiMagicCount n t, the Finset.card of the arrays over Square n (Fin (t+1)) satisfying IsSemiMagic. Entries are natural numbers, not integers or reals.
• The polynomial is over ℚ and is quantified existentially. Negative arguments are handled by casting the integer into ℚ and evaluating there; Polynomial.eval₂ is unusable for the reciprocity, since it would need a ring homomorphism $\mathbb{Q}\to\mathbb{Z}$, which does not exist.
• The degree is encoded as p.natDegree = (n - 1) ^ 2, with natural-number subtraction, which makes the $n=1$ case harmless rather than degenerate.
• The hypothesis 1 ≤ n is carried explicitly although the statement is meaningful at $n=0$; it matches the source.
• A trivializing formalization to avoid: replacing ∀ t by a finite range of values, or replacing semiMagicCount by a smooth surrogate, would make the statement easy and empty. The universal quantifier over $t$ and the exact value of natDegree are what give the goal its content.

Reusable beyond this mission: any development of lattice-point counting in the Birkhoff polytope, of dilations of rational polytopes, or of quasi-polynomials. The vocabulary of the programme (MagicSquares, MagicSquaresPandiagonal, MagicSquaresMostPerfect, MagicSquaresTransforms, MagicSquaresNormal3) is shared with the earlier missions and is included as reference items rather than redefined.

Selected references

• P. A. MacMahon, Combinatory Analysis, Chelsea, New York, 1960.
• H. Anand, V. C. Dumir and H. Gupta, A combinatorial distribution problem, Duke Math. J. 33 (1966) 757--769.
• E. Ehrhart, Sur les carrés magiques, C. R. Acad. Sci. Paris Sér. A-B 277 (1973) A651--A654.
• R. P. Stanley, Linear homogeneous Diophantine equations and magic labelings of graphs, Duke Math. J. 40 (1973) 607--632.
• J. Spencer, Counting magic squares, Amer. Math. Monthly 87 (1980) 397--399.
• M. Beck and D. Pixton, The Ehrhart polynomial of the Birkhoff polytope, arXiv:math.CO/0202267 — https://arxiv.org/abs/math/CO/0202267
• M. Beck, M. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003) 707--717 — https://arxiv.org/abs/math/0201013
• G. M. Ziegler, Lectures on Polytopes, Springer-Verlag, New York, 1995.