The pandiagonal squares of order two

Proved

MagicSquares.pandiagonal_count_two

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

combinatoricsenumerative-combinatoricsmagic-squares

The order-two pandiagonal count. With $P_{n}(t)$ the number of pandiagonal squares of order $n$ and line sum $t$ in the counting-theory sense of IsPandiagonal (semi-magic plus the wrapped diagonals parallel to the main diagonal), the theorem states

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

Proof. At order two the two wrapped diagonals of a semi-magic square are exactly its main and anti-diagonal, so IsPandiagonal coincides with IsMagic and $P_{2}=M_{2}$ . This is the last order at which the two notions agree: from order three on they diverge.

Preamble

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

Formal statement

namespace MagicSquares

theorem pandiagonal_count_two (t : ℕ) : pandiagonalCount 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