Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

No symmetric magic squares of order three when the line sum is not divisible by three

Proved
MagicSquares.symm_three_otherwise

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

combinatoricsenumerative-combinatoricsmagic-squares

The zero case for symmetric magic squares.

Writing Sn(t)S_{n}(t)Sn​(t) for the number of symmetric magic squares of order nnn and line sum ttt, the theorem is

3∤t  ⟹  S3(t)=0,3\nmid t\implies S_{3}(t)=0 ,3∤t⟹S3​(t)=0,

the companion of the evaluation S3(3e)=2e+1S_{3}(3e)=2e+1S3​(3e)=2e+1.

Proof. A symmetric magic square is in particular magic, and for a magic square of order three and line sum ttt the centre entry ccc satisfies 3c=t3c=t3c=t by center_of_order_three. Hence 3∣t3\mid t3∣t is necessary for existence, and the filtered finset symmetricMagicSquares 3 t is empty otherwise.

Context. Symmetry does not produce new line sums beyond those already admitted by the magic squares — it only cuts each magic fibre down. So the same divisibility obstruction applies, and the symmetric count, like the panmagic and the plain magic counts, vanishes off the multiples of three.

Preamble
import Mathlib
import Definitions.Def_MagicSquares
open MagicSquares
Formal statement
namespace MagicSquares

theorem symm_three_otherwise (t : ℕ) (ht : ¬ 3 ∣ t) : symmetricMagicCount 3 t = 0 := by sorry

end MagicSquares
Source
P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916; M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717 (arXiv:math/0201013); W. S. Andrews, Magic Squares and Cubes, 2nd ed., Dover, 1960.
Human review
  • Endorsed by Shuze Chen · Sep 18, 2026

  • Endorsed by Yuxuan Xu · Sep 18, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, licensed under Apache 2.0.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTermsJoin SlackJoin Zulip© 2026 Prove2Me