Magic Squares of Squares over Finite Fields and an Extension to Arbitrary Powers

We study 3 × 3 magic squares with nine distinct entries that are squares, cubes, or more generally n-th powers in a finite field. Using the universal parametrization of magic squares, multiplicative characters, and center-zero and center-one constructions, we obtain explicit field-size bounds guaranteeing existence. Combining these bounds with finite classifications, we determine exactly which finite fields of odd order admit no magic square of distinct squares and which admit no magic square of distinct cubes. We also prove that characteristic two obstructs such squares for every exponent and that, for each fixed positive integer n, only finitely many odd field cardinalities are exceptional for n-th powers. The principal results are formalized in Lean 4 using mathlib. The formalization includes the split-polynomial multiplicative-character bounds needed for the existence arguments, including repeated roots, together with positive certificates, nonexistence proofs, and exhaustive coverage of the remaining finite cases. The accompanying repositories provide the formal proofs, computational search code, and documentation connecting the paper’s results to their Lean declarations.