Magic Squares
Does there exist a 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.
Mathematical statement
Does there exist a 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 matrix with entries such that each for some positive integer , all nine cubes are distinct, and all row sums and column sums are equal. Reference:* Semi-Magic Square of Cubes
Statement source: Wikipedia statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
exists_semi_magic_square_cubes
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) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References