exists_magic_square_squares

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?

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

Recent Submissions

No submissions yet. Be the first to attempt this problem.