Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

In an order-three magic square, opposite cells sum to twice the centre

Proved
MagicSquares.order_three_opposite_sum_eq_twice_center

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

combinatoricsmagic-squares

Opposite cells in an order-three magic square. Let AAA be a 3×33\times33×3 magic square with line sum SSS. Then for every pair of centrally opposite cells,

Aij+A2−i, 2−j  =  2 A11.A_{ij} + A_{2-i,\,2-j} \;=\; 2\,A_{11} .Aij​+A2−i,2−j​=2A11​.

Equivalently, an order-three magic square is automatically associative with complement constant 2A112A_{11}2A11​. Since MacMahon's identity gives S=3A11S = 3A_{11}S=3A11​, each such pair sums to 23S\tfrac23 S32​S, and in particular the square is determined by its centre: every opposite pair is pinned to twice it.

The four pairs are (1,1)(1,1)(1,1)–(3,3)(3,3)(3,3) and (1,3)(1,3)(1,3)–(3,1)(3,1)(3,1) (the two diagonals) and (1,2)(1,2)(1,2)–(3,2)(3,2)(3,2), (2,1)(2,1)(2,1)–(2,3)(2,3)(2,3) (the middle column and middle row); the fifth "pair" is the centre with itself, which is trivial. This is the structural fact behind the classical parametrisation of 3×33\times33×3 magic squares by two corner entries: once A11A_{11}A11​ and one corner are chosen, all remaining cells follow.

Formalization Note Cells are indexed by Fin 3 and Fin.rev is the reversal i↦2−ii\mapsto 2-ii↦2−i, so (i,j)(i,j)(i,j) and (rev i,rev j)(\mathrm{rev}\,i,\mathrm{rev}\,j)(revi,revj) are the centrally opposite pair. The proof expands the nine line identities and finishes by linear arithmetic; no integrality hypothesis beyond N\mathbb{N}N is needed.

Preamble
import Mathlib
import Definitions.Def_MagicSquares
Formal statement
namespace MagicSquares

theorem order_three_opposite_sum_eq_twice_center
    (M : Square 3 ℕ) (s : ℕ) (hM : IsMagic M s) (i j : Fin 3) :
    M i j + M (Fin.rev i) (Fin.rev j) = 2 * M 1 1 := 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.
Human review
  • Endorsed by Shuze Chen · Sep 16, 2026

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