Conjectures about Latin Squares

The question

oddOrderLatinSquareTransversal. Conjecture 3.2 in [Wa2011]: Each Latin square of odd order has at least one transversal.

latinSquareOrder11Transversal. The smallest odd number for which this conjecture is not known is 11.

latinSquareNearTransversal. Conjecture 5.1 in [Wa2011]: Every latin square has a near-transversal

numTransversalsZn. Conjecture 6.7 in [Wa2011]: There exist real constants $0<c_1<c_2<1$ such that $$c_1^{n}n!\le z_n\le c_2^{n}n!$$ for all odd $n\ge 3$.

growthRateZn. Conjecture 6.9 in [Wa2011]: $$\underset{\begin{array}{c}n\to \infty \\ n\text{ odd}\end{array}}{\lim }\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$.

molsExistenceProblem. 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.

molsOrder12. The smallest unresolved case of the MOLS existence problem: whether there are 11 mutually orthogonal latin squares of order 12.

This file formalizes some conjectures and theorems around latin squares.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Paper.LatinSquare (7 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem oddOrderLatinSquareTransversal : answer(sorry) ↔
    ∀ (n : ℕ), Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ

theorem latinSquareOrder11Transversal : answer(sorry) ↔
    ∀ (L : LatinSquare 11), ∃ σ, IsTransversal L σ

theorem latinSquareNearTransversal : answer(sorry) ↔
    ∀ (n : ℕ) (L : LatinSquare n), ∃ ρ σ, IsNearTransversal L ρ σ

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)

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))

theorem molsExistenceProblem : answer(sorry) = {n : ℕ | HasCompleteMOLS n}

theorem molsOrder12 : answer(sorry) ↔ HasCompleteMOLS 12

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

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

Source and licence

Imported from Formal Conjectures (research papers), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.