Magic Squares

References:

• Magic Square of Squares - Wikipedia
• multimagie.com
• Semi-Magic Square of Cubes
• Magic Square of Squares

theorem MagicSquares.exists_magic_square_squares : True ↔ ∃ (m : Fin 3 → Fin 3 → ℕ) (t : ℕ), Function.Injective2 m ∧ (∀ (i j : Fin 3), 0 < m i j ∧ IsSquare (m i j)) ∧ (∀ (i : Fin 3), ∑ j : Fin 3, m i j = t) ∧ (∀ (j : Fin 3), ∑ i : Fin 3, m i j = t) ∧ m 0 0 + m 1 1 + m 2 2 = t ∧ m 0 2 + m 1 1 + m 2 0 = t

Does there exist a $3 \times 3$ matrix such that every entry is a distinct square, and all rows, columns, and diagonals add up to the same value?

0 is excluded, as a Magic Square of Squares with 0 and 8 distinct squares is know is knownn. See Magic Square of Squares

theorem MagicSquares.exists_semi_magic_square_cubes : True ↔ ∃ (m : Fin 3 → Fin 3 → ℕ) (t : ℕ), Function.Injective2 m ∧ (∀ (i j : Fin 3), ∃ (n : ℕ), 0 < n ∧ m i j = n ^ 3) ∧ (∀ (i : Fin 3), ∑ j : Fin 3, m i j = t) ∧ ∀ (j : Fin 3), ∑ i : Fin 3, m i j = t

Does there exist a $3 \times 3$ semi-magic square whose entries are all distinct positive integer cubes? A square is semi-magic if all rows and columns sum to the same total.

More precisely, we seek a $3 \times 3$ matrix with entries $a_{ij}$ such that each $a_{ij} = n_{ij}^3$ for some positive integer $n_{ij}$, all nine cubes are distinct, and all row sums and column sums are equal.

Reference: Semi-Magic Square of Cubes