Magic Square of Squares #

References:

sorry ↔ ∃ (m : Fin 3 → Fin 3 → ℕ) (t : ℕ), Function.Injective2 m ∧ (∀ (i j : Fin 3), 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 by 3 matrix such that every entry is a distinct square, and all rows, columns, and diagonals add up to the same value?

Documentation