The symmetric magic squares of order two

Proved

MagicSquares.symmetric_magic_count_two

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

combinatoricsenumerative-combinatoricsmagic-squares

The order-two symmetric count. Writing $S_{n}(t)$ for the number of $n\times n$ arrays of nonnegative integers which are magic of line sum $t$ and equal to their own transpose, the theorem states

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

Proof. For order two the transpose condition is $M_{01}=M_{10}$ , which already holds for every semi-magic square: the first row and first column both read $M_{00}+M_{01}=t$ and $M_{00}+M_{10}=t$ . So symmetry adds no condition at order two, $S_{2}=M_{2}$ , and the order-two magic count applies. Symmetry only starts to bite at order three, where it cuts the two-parameter MacMahon family down to a one-parameter one.

Preamble

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

Formal statement

namespace MagicSquares

theorem symmetric_magic_count_two (t : ℕ) : symmetricMagicCount 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