Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

There are exactly eight normal magic squares of order three

Proved
MagicSquares.magic_three_normal_eight

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

combinatoricsenumerative-combinatoricsmagic-squares

Lo Shu uniqueness. Exactly eight admissible parameter pairs give a normal magic square of order three:

normalParamCount(5)=8,\mathrm{normalParamCount}(5)=8,normalParamCount(5)=8,

where normalParamCount(e)\mathrm{normalParamCount}(e)normalParamCount(e) counts the pairs (a,c)∈paramSet(e)(a,c)\in\mathrm{paramSet}(e)(a,c)∈paramSet(e) for which mkMagic3(e,a,c)\mathrm{mkMagic3}(e,a,c)mkMagic3(e,a,c) is normal.

By magic_three_param_bij the admissible parameter pairs are in bijection with the 3×33\times33×3 magic squares of line sum 151515, so this is precisely the statement that there are eight normal magic squares of order three — the eight images of

(492357816)\begin{pmatrix}4&9&2\\3&5&7\\8&1&6\end{pmatrix}​438​951​276​​

under the symmetry group D4D_{4}D4​ of the square. Equivalently: the Lo Shu square is the unique normal magic square of order three up to symmetry.

This is the oldest non-trivial classification in combinatorics, and the reason order three is exceptional: for n=4n=4n=4 there are 880880880 normal squares up to symmetry, and for n≥5n\ge5n≥5 no classification is known.

Proof. Immediate from magic_three_normal_classify, which characterizes normality by the eight parameter pairs (2,4),(2,6),(4,2),(4,8),(6,2),(6,8),(8,4),(8,6)(2,4),(2,6),(4,2),(4,8),(6,2),(6,8),(8,4),(8,6)(2,4),(2,6),(4,2),(4,8),(6,2),(6,8),(8,4),(8,6): the defining filter of normalParamSet 5 selects exactly those eight, and they are distinct.

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

theorem magic_three_normal_eight : normalParamCount 5 = 8 := by sorry

end MagicSquares
Source
P. A. MacMahon, Combinatory Analysis (1916); W. S. Andrews, Magic Squares and Cubes, 2nd ed., Dover, 1960.
Human review
  • Endorsed by Shuze Chen · Sep 17, 2026

  • Endorsed by Yuxuan Xu · Sep 17, 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