No 3x3 magic square has a line sum coprime to 3

Proved

MagicSquares.magic_count_three_otherwise

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

combinatoricsmagic-squares

If $t$ is not divisible by $3$ , there is no $3 \times 3$ magic square with line sum $t$ .

Write $M_{3}(t)$ for the number of $3 \times 3$ arrays of nonnegative integers whose three rows, three columns and two main diagonals all sum to $t$ . Then

3 \nmid t \;\Longrightarrow\; M_{3}(t) = 0 .

This is an immediate consequence of the fact that the centre entry satisfies $3M_{1,1} = t$ ; see MagicSquares.center_of_order_three. Together with MagicSquares.magic_count_three_divisible this determines $M_{3}$ completely.

Preamble

import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares

Formal statement

namespace MagicSquares

theorem magic_count_three_otherwise (t : ℕ) (ht : ¬ 3 ∣ t) :
    magicCount 3 t = 0 := by sorry

end MagicSquares

Source

Beck, Cohen, Cuomo & Gribelyuk, The number of ``magic'' squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707-717; arXiv:math/0201013v3, Section 2, MacMahon's formula for

M_{3}(t)

(1915).

View graph