Papers With

← All papers
First page of A proper Euler magic matrix of order 6

A proper Euler magic matrix of order 6

Sanjit Singh Mehat

math.GM Aug 15, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract
TL;DR
A machine-checked Lean 4 with Mathlib proof verifies existence of a proper order-6 Euler magic matrix, with #print axioms confirming no sorry.
Abstract
An Euler magic matrix is an integer matrix M with MM^t = gamma I for some gamma != 0, whose squared entries sum to gamma along both main diagonals; it is proper if its squared entries are pairwise distinct. Euler gave a proper example of order 4; Müller settled orders 3 (none exists) and 8; and Kominers settled order 5. We give an order-6 construction, a case not addressed by Müller or Kominers, exhibiting a proper Euler magic matrix of order 6 with gamma = 18500 together with a second, independent one with gamma = 43290. The proof is the explicit matrix and a finite exact verification. We also record an elementary counting bound gamma >= 2485 for proper order-6 examples.
Problem

An Euler magic matrix is an integer matrix M with MM^t = γI whose squared entries sum to γ along both diagonals, and is proper if squared entries are pairwise distinct. Existence at order 6 was not settled by prior work (orders 1,2,3,4,5,8 were known).

Approach

An explicit order-6 matrix with γ=18500 and a second independent one with γ=43290 are constructed via a search generating matrices satisfying the orthogonality condition and post-filtering permutations for compatible diagonal sums. An elementary counting bound γ ≥ 2485 restricts the search range. The finite integer identities are verified three independent ways, including a machine-checked proof in Lean 4 with Mathlib whose #print axioms reports only propext, Classical.choice and Quot.sound with no sorry or native_decide.

Results

Two proper Euler magic matrices of order 6 are exhibited (γ=18500 and γ=43290), settling the previously unaddressed order-6 case, together with the lower bound γ ≥ 2485.