The semi-magic squares of order two

Proved

MagicSquares.semi_magic_count_two

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

combinatoricsenumerative-combinatoricsmagic-squares

The order-two semi-magic count. Writing $H_{n}(t)$ for the number of $n\times n$ arrays of nonnegative integers whose rows and columns all sum to $t$ , the theorem states

H_{2}(t)=t+1 .

Proof. A $2\times2$ semi-magic square of line sum $t$ reads $\begin{pmatrix} a & t-a\\ t-a & a\end{pmatrix}$ , so it is determined by its top-left corner $a$ , and $a$ may be any of $0,1,\dots,t$ . This is the first value in the structural statement that $H_{n}(t)$ is a polynomial of degree $(n-1)^{2}$ — for $n=2$ that is degree one, matching $t+1$ .

Preamble

import Mathlib
import Definitions.Def_MagicSquares
import Definitions.Def_MagicSquaresPandiagonal
open MagicSquares

Formal statement

namespace MagicSquares

theorem semi_magic_count_two (t : ℕ) : semiMagicCount 2 t = t + 1 := 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).

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