A normal 3x3 magic square is associative with constant 10

Proved

MagicSquares.normal_order_three_associative

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

combinatoricsmagic-squares

Every normal $3 \times 3$ magic square is associative (also called regular or symmetric through the centre) with complement constant $10$ : any two centrally opposite cells add up to $10$ ,

M_{ij} + M_{2-i,\,2-j} = 10 \qquad \text{for all } 0 \le i, j \le 2 .

Indeed the centre is $5$ , and each opposite pair lies together with the centre on a row, a column, or one of the two diagonals, all of which sum to $15$ ; hence each pair sums to $15 - 5 = 10$ .

The pair $\{M_{11}, M_{11}\}$ is covered too, as $5 + 5 = 10$ .

Formalization Note IsAssociative M c is \forall i j, M i j + M (Fin.rev i) (Fin.rev j) = c, and Fin.rev is the reversal $i \mapsto 2-i$ on Fin 3. The proof splits the nine index pairs with fin_cases and closes each by omega from the row/column/diagonal identities and s = 15.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

theorem normal_order_three_associative (M : Square 3 ℕ) (s : ℕ)
    (hN : IsNormal M) (hM : IsMagic M s) :
    IsAssociative M 10 := by sorry

end MagicSquares

Source

Classical Lo Shu structure theory; see e.g. the associative-square discussion in Beck, Cohen, Cuomo & Gribelyuk, The number of ``magic'' squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717; arXiv:math/0201013v3.

View graph