There is no normal magic square of order 2
ProvedMagicSquares.normal_order_two_nonecombinatoricsmagic-squares
No array can have the four distinct entries and be magic.
Suppose has all rows, columns and both diagonals summing to . Comparing the first row with the main diagonal gives , contradicting the requirement that the four entries be distinct. Hence no normal magic square of order exists.
This is the instance of the general fact that normal magic squares exist for every order except .
Formalization Note IsNormal supplies injectivity of the index-to-entry map, and the two
cells and are distinct, so the equality is immediately contradictory.
Preamble
import Mathlib import Definitions.Def_MagicSquares open MagicSquares
Formal statement
namespace MagicSquares
theorem normal_order_two_none :
¬ ∃ (M : Square 2 ℕ) (s : ℕ), IsNormal M ∧ IsMagic M s := by sorry
end MagicSquaresSource
Classical; consistent with Beck, Cohen, Cuomo & Gribelyuk, arXiv:math/0201013v3, Section 2, where for even and otherwise (i.e. every order-2 magic square has four equal entries).