/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilMagic Squares
namespace MagicSquares
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
@[category research open, AMS 11]
theorem exists_magic_square_squares :
answer(sorry) ↔ ∃ m : Fin 3 → Fin 3 → ℕ, ∃ t : ℕ,
m.Injective2 ∧
(∀ i j, 0 < (m 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 := ⊢ True ↔
∃ m t,
Function.Injective2 m ∧
(∀ (i j : Fin 3), 0 < m i j ∧ IsSquare (m i j)) ∧
(∀ (i : Fin 3), ∑ j, m i j = t) ∧
(∀ (j : Fin 3), ∑ 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
All goals completed! 🐙
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.
@[category research open, AMS 5 11]
theorem exists_semi_magic_square_cubes :
answer(sorry) ↔ ∃ m : Fin 3 → Fin 3 → ℕ, ∃ t : ℕ,
m.Injective2 ∧
(∀ i j, ∃ n : ℕ, 0 < n ∧ m i j = n ^ 3) ∧
(∀ i, ∑ j, m i j = t) ∧
(∀ j, ∑ i, m i j = t) := ⊢ True ↔
∃ m t,
Function.Injective2 m ∧
(∀ (i j : Fin 3), ∃ n, 0 < n ∧ m i j = n ^ 3) ∧ (∀ (i : Fin 3), ∑ j, m i j = t) ∧ ∀ (j : Fin 3), ∑ i, m i j = t
All goals completed! 🐙
end MagicSquares