The magic squares of order two

Proved

MagicSquares.magic_count_two

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

combinatoricsenumerative-combinatoricsmagic-squares

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

M_{2}(t)=\begin{cases}1,&2\mid t,\\ 0,&2\nmid t.\end{cases}

The single square is the constant array with every entry $t/2$ . Proof. In the $\begin{pmatrix} a & t-a\\ t-a & a\end{pmatrix}$ family the two diagonals read $2a$ and $2(t-a)$ ; requiring both to equal $t$ forces $2a=t$ . This is the first instance of the divisibility obstruction that governs every magic-square count: the diagonal conditions are not automatic, and they vanish off a sublattice of line sums.

Preamble

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

Formal statement

namespace MagicSquares

theorem magic_count_two (t : ℕ) : magicCount 2 t = if 2 ∣ t then 1 else 0 := 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).

View graph