/-
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 FormalConjecturesUtilConjectures about Latin Squares
This file formalizes some conjectures and theorems around latin squares.
References:
[Wa2011] Wanless, Ian. "Transversals in Latin Squares: A Survey." Surveys in Combinatorics 2011, R. Chapman, Ed. Cambridge University Press, 2011, pp. 403–437. https://users.monash.edu.au/~iwanless/papers/transurveyBCC.pdf
https://en.wikipedia.org/wiki/Problems_in_Latin_squares
namespace LatinSquareTwo latin squares of the same order are orthogonal if superimposing them gives each ordered pair of symbols at most once.
def Orthogonal {n : ℕ} (L M : LatinSquare n) : Prop :=
Function.Injective fun p : Fin n × Fin n => (L.mat p.1 p.2, M.mat p.1 p.2)A family of latin squares is mutually orthogonal if any two distinct members are orthogonal.
def MutuallyOrthogonal {k n : ℕ} (L : Fin k → LatinSquare n) : Prop :=
∀ ⦃i j : Fin k⦄, i ≠ j → Orthogonal (L i) (L j)
A complete set of mutually orthogonal latin squares (MOLS) of order n consists of n - 1
latin squares of order n, pairwise orthogonal to each other.
def HasCompleteMOLS (n : ℕ) : Prop :=
0 < n ∧ ∃ L : Fin (n - 1) → LatinSquare n, MutuallyOrthogonal LConjecture 3.2 in [Wa2011]: Each Latin square of odd order has at least one transversal.
@[category research open, AMS 5]
theorem oddOrderLatinSquareTransversal : answer(sorry) ↔
∀ (n : ℕ), Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ := ⊢ True ↔ ∀ (n : ℕ), Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ
All goals completed! 🐙The conjecture is known to be true for $n \leq 9$.
@[category research solved, AMS 5]
theorem oddOrderLeq9LatinSquareTransversal : answer(True) ↔
∀ n ≤ 9, Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ := ⊢ True ↔ ∀ n ≤ 9, Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ
All goals completed! 🐙The smallest odd number for which this conjecture is not known is 11.
@[category research open, AMS 5]
theorem latinSquareOrder11Transversal : answer(sorry) ↔
∀ (L : LatinSquare 11), ∃ σ, IsTransversal L σ := ⊢ True ↔ ∀ (L : LatinSquare 11), ∃ σ, IsTransversal L σ
All goals completed! 🐙Conjecture 5.1 in [Wa2011]: Every latin square has a near-transversal
@[category research open, AMS 5]
theorem latinSquareNearTransversal : answer(sorry) ↔
∀ (n : ℕ) (L : LatinSquare n), ∃ ρ σ, IsNearTransversal L ρ σ := ⊢ True ↔ ∀ (n : ℕ) (L : LatinSquare n), ∃ ρ σ, IsNearTransversal L ρ σ
All goals completed! 🐙The number of transversals of the Cayley table of the cyclic group $\mathbb{Z}_n$
def z (n : ℕ) : ℕ := numTransversals {
mat := Matrix.of fun i j : Fin n => i + j
row_injective := fun i _a _b h => n:ℕi:Fin n_a:Fin n_b:Fin nh:Matrix.of (fun i j ↦ i + j) i _a = Matrix.of (fun i j ↦ i + j) i _b⊢ _a = _b
n:ℕi:Fin n_a:Fin n_b:Fin nh:i + _a = i + _b⊢ _a = _b; All goals completed! 🐙
col_injective := fun j _a _b h => n:ℕj:Fin n_a:Fin n_b:Fin nh:(Matrix.of fun i j ↦ i + j).transpose j _a = (Matrix.of fun i j ↦ i + j).transpose j _b⊢ _a = _b
n:ℕj:Fin n_a:Fin n_b:Fin nh:_a + j = _b + j⊢ _a = _b; All goals completed! 🐙
}The $0 \times 0$ Cayley table has exactly $1$ transversal (vacuously).
@[category test, AMS 5]
theorem z_zero : z 0 = 1 := ⊢ z 0 = 1 All goals completed! 🐙The number of transversals of the Cayley table of $\mathbb{Z}_n$ for odd $n$ forms OEIS A006717, starting with $z(1) = 1, z(3) = 3, z(5) = 15, z(7) = 133$.
@[category test, AMS 5]
theorem z_odd_values : [z 1, z 3, z 5, z 7] = [1, 3, 15, 133] := ⊢ [z 1, z 3, z 5, z 7] = [1, 3, 15, 133] All goals completed! 🐙The Cayley table of $\mathbb{Z}_n$ for positive even $n$ has no transversals.
n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1)hNpos:0 < Nthis:NeZero Nx✝:{ σ // IsTransversal { mat := Matrix.of fun i j ↦ i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i ↦ i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i ↦ i + σ i) ⋯g:Fin N → ZMod N := fun i ↦ ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g ihcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i)h1:∑ i, g (i + σ i) = Sh2:∑ i, g (σ i) = ShSS:S + S = ShS0:↑((n + 1) * (2 * n + 1)) = 0hval:S = ↑((Finset.range N).sum id)hdiv:N * (N - 1) / 2 = (n + 1) * (2 * n + 1)hdvd:2 ∣ 2 * n + 1⊢ False
All goals completed! 🐙Conjecture 6.7 in [Wa2011]: There exist real constants $0 < c_1 < c_2 < 1$ such that $$ c_1^n n! \leq z_n \leq c_2^n n! $$ for all odd $n \geq 3$.
@[category research open, AMS 5]
theorem numTransversalsZn : answer(sorry) ↔
∃ᵉ (c₁ > (0 : ℝ)) (c₂ < (1 : ℝ)) (_ : c₁ < c₂),
∀ n ≥ 3, Odd n →
(z n : ℝ) ∈ Set.Icc (c₁ ^ n * n.factorial) (c₂ ^ n * n.factorial) := ⊢ True ↔
∃ c₁ > 0, ∃ c₂ < 1, ∃ (_ : c₁ < c₂), ∀ n ≥ 3, Odd n → ↑(z n) ∈ Set.Icc (c₁ ^ n * ↑n.factorial) (c₂ ^ n * ↑n.factorial)
All goals completed! 🐙
Conjecture 6.9 in [Wa2011]:
$$
\lim_{\substack{n \to \infty \ n \text{ odd}}} \frac{1}{n} \log(z_n / n!) = -1
$$
It is not even known if this limit exists. Note that $z_n = 0$ for even $n$ (see z_even), so the
limit must be restricted to odd $n$; here we parametrise odd $n$ as $2k + 1$.
@[category research open, AMS 5]
theorem growthRateZn : answer(sorry) ↔
Filter.Tendsto (fun k => (1 : ℝ) / (2 * k + 1) *
Real.log (z (2 * k + 1) / (2 * k + 1).factorial)) Filter.atTop
(nhds (-1)) := ⊢ True ↔
Filter.Tendsto (fun k ↦ 1 / (2 * ↑k + 1) * Real.log (↑(z (2 * k + 1)) / ↑(2 * k + 1).factorial)) Filter.atTop
(nhds (-1))
All goals completed! 🐙
The maximum number of transversals over all latin squares of order n.
def T (n : ℕ) : ℕ := Finset.sup Finset.univ (fun L : LatinSquare n => numTransversals L)Theorem 7.2 in [Wa2011]: For all $n \geq 5$, $$ 15^{n/5} \leq T(n) \leq c^n \sqrt{n} \cdot n! $$ where $c = \sqrt{\frac{3 - \sqrt{3}}{6}} \cdot e^{\sqrt{3}/6}$
@[category research solved, AMS 5]
theorem maxTransversalsBound :
let c := Real.sqrt ((3 - Real.sqrt 3) / 6) * Real.exp (Real.sqrt 3 / 6)
∀ n : ℕ, n ≥ 5 →
(T n : ℝ) ∈ Set.Icc ((15 : ℝ) ^ ((n : ℝ) / 5)) (c ^ n * Real.sqrt n * n.factorial) := ⊢ let c := √((3 - √3) / 6) * Real.exp (√3 / 6);
∀ n ≥ 5, ↑(T n) ∈ Set.Icc (15 ^ (↑n / 5)) (c ^ n * √↑n * ↑n.factorial)
All goals completed! 🐙
MOLS existence problem: determine exactly which orders n admit a complete set of n - 1
mutually orthogonal latin squares.
Equivalently, this asks for which orders affine planes of order n exist. Complete sets are known
for prime-power orders; the smallest currently unresolved order is 12.
@[category research open, AMS 5]
theorem molsExistenceProblem : answer(sorry) = {n : ℕ | HasCompleteMOLS n} := ⊢ sorry = {n | HasCompleteMOLS n}
All goals completed! 🐙
The smallest unresolved case of the MOLS existence problem: whether there are 11 mutually
orthogonal latin squares of order 12.
@[category research open, AMS 5]
theorem molsOrder12 : answer(sorry) ↔ HasCompleteMOLS 12 := ⊢ True ↔ HasCompleteMOLS 12
All goals completed! 🐙/-
TODO(rao107): Conjecture 8.5 in [Wa2011]:
Every latin square has the maximum number of disjoint duplexes. In particular, every latin square of
even order has a 2-partition and every latin square of odd order has a
(2, 2, 2, ..., 2, 1)-partition.
-/
/-
TODO(rao107): Conjecture 8.6 in [Wa2011]:
For all even $n > 4$ there exists a latin square of ordern $n$ which has no transversal but does
contain a 3-plex.
-/
/-
TODO(rao107): Conjecture 9.2 in [Wa2011]:
If $n$ is even, then $f(n, 2) = n$; if $n$ is odd, then $f(n, 2) > n$.
-/
/-
TODO(rao107): Conjecture 10.10 in [Wa2011]:
Every latin hypercube of odd dimension or of odd order has a transversal.
-/
end LatinSquare