LatinSquare.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

17 declarations, 9 contain sorry, 0 declared as axioms

Conjectures 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

Imports (2)

def LatinSquare.Orthogonal Two latin squares of the same order are orthogonal if superimposing them gives each ordered pair of symbols at most once line 41 source
Source documentation
Two latin squares of the same order are orthogonal if superimposing them gives each ordered pair of symbols at most once.

standard axioms: Quot.sound what this means
Statement uses: Nat, LatinSquare
Proof uses: Function.Injective, Prod, Fin, Prod.mk, LatinSquare.mat, Prod.fst, Prod.snd
```
def Orthogonal {n : ℕ} (L M : LatinSquare n) : Prop :=
…
```
Mentions: LatinSquare
def LatinSquare.MutuallyOrthogonal A family of latin squares is mutually orthogonal if any two distinct members are orthogonal line 45 source
Source documentation
A family of latin squares is mutually orthogonal if any two distinct members are orthogonal.

standard axioms: Quot.sound what this means
Statement uses: Nat, Fin, LatinSquare
Proof uses: Ne, LatinSquare.Orthogonal
```
def MutuallyOrthogonal {k n : ℕ} (L : Fin k → LatinSquare n) : Prop :=
…
```
Mentions: LatinSquare
def LatinSquare.HasCompleteMOLS 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 line 52 source
Source documentation
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.

standard axioms: Quot.sound what this means
Statement uses: Nat
Proof uses: And, LT.lt, OfNat.ofNat, Exists, Fin, HSub.hSub, LatinSquare, LatinSquare.MutuallyOrthogonal
4 instances, coercions and auxiliary constants left out.
```
def HasCompleteMOLS (n : ℕ) : Prop :=
…
```
theorem LatinSquare.oddOrderLatinSquareTransversal Conjecture 3.2 in [Wa2011]: Each Latin square of odd order has at least one transversal sorry line 60 source
Source documentation
Conjecture 3.2 in [Wa2011]: Each Latin square of odd order has at least one transversal.

depends on sorry what this means
Statement uses: Iff, True, Nat, Odd, LatinSquare, Exists, Fin, IsTransversal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem oddOrderLatinSquareTransversal : answer(sorry) ↔
    ∀ (n : ℕ), Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ := by
…
```
Mentions: LatinSquare, IsTransversal
theorem LatinSquare.oddOrderLeq9LatinSquareTransversal The conjecture is known to be true for $n \leq 9$ sorry line 68 source
Source documentation
The conjecture is known to be true for $n \leq 9$.

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Odd, LatinSquare, Exists, Fin, IsTransversal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem oddOrderLeq9LatinSquareTransversal : answer(True) ↔
    ∀ n ≤ 9, Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ := by
…
```
Mentions: LatinSquare, IsTransversal
theorem LatinSquare.latinSquareOrder11Transversal The smallest odd number for which this conjecture is not known is 11 sorry line 76 source
Source documentation
The smallest odd number for which this conjecture is not known is 11.

depends on sorry what this means
Statement uses: Iff, True, LatinSquare, OfNat.ofNat, Nat, Exists, Fin, IsTransversal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem latinSquareOrder11Transversal : answer(sorry) ↔
    ∀ (L : LatinSquare 11), ∃ σ, IsTransversal L σ := by
…
```
Mentions: LatinSquare, IsTransversal
theorem LatinSquare.latinSquareNearTransversal Conjecture 5.1 in [Wa2011]: Every latin square has a near-transversal sorry line 91 source
Source documentation
Conjecture 5.1 in [Wa2011]: Every latin square has a near-transversal

depends on sorry what this means
Statement uses: Iff, True, Nat, LatinSquare, Exists, Fin, HSub.hSub, OfNat.ofNat, IsNearTransversal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem latinSquareNearTransversal : answer(sorry) ↔
    ∀ (n : ℕ) (L : LatinSquare n), ∃ ρ σ, IsNearTransversal L ρ σ := by
…
```
Mentions: LatinSquare, IsNearTransversal
def LatinSquare.z The number of transversals of the Cayley table of the cyclic group $\mathbb{Z}_n$ line 96 source
Source documentation
The number of transversals of the Cayley table of the cyclic group $\mathbb{Z}_n$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: numTransversals, LatinSquare.mk, Equiv, Fin, Matrix, Matrix.of, HAdd.hAdd, Eq, Matrix.transpose
7 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def z (n : ℕ) : ℕ := numTransversals {
…
```
Mentions: numTransversals
theorem LatinSquare.z_zero The $0 \times 0$ Cayley table has exactly $1$ transversal (vacuously) line 106 source
Source documentation
The $0 \times 0$ Cayley table has exactly $1$ transversal (vacuously).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, LatinSquare.z, OfNat.ofNat
Proof uses: id, of_decide_eq_true, Fintype.card, Subtype, Fin, IsTransversal, LatinSquare.mk, Equiv, Matrix, Matrix.of, HAdd.hAdd, Matrix.transpose, Function.Injective, LatinSquare.mat, Bool, Decidable.decide, Bool.true, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem z_zero : z 0 = 1 := by
…
```
Mentions: LatinSquare.z
theorem LatinSquare.z_odd_values 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$ line 114 source
Source documentation
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$.

L4DEL explanation
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$.
Sources and attribution: Pinned Lean source (1646ca16afd6)

extra axioms: _private.0.LatinSquare.z_odd_values._native.native_decide.ax_1 what this means
Statement uses: Eq, List, Nat, List.cons, LatinSquare.z, OfNat.ofNat, List.nil
Proof uses: of_decide_eq_true
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem z_odd_values : [z 1, z 3, z 5, z 7] = [1, 3, 15, 133] := by native_decide
…
```
Mentions: LatinSquare.z
theorem LatinSquare.z_even The Cayley table of $\mathbb{Z}_n$ for positive even $n$ has no transversals line 118 source
Source documentation
The Cayley table of $\mathbb{Z}_n$ for positive even $n$ has no transversals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, LatinSquare.z, HMul.hMul, OfNat.ofNat, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, rfl, LT.lt, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Right.add_pos_of_nonneg_of_pos, LE.le, zero_le, NeZero, NeZero.mk, LT.lt.ne', numTransversals, LatinSquare.mk, Equiv and 107 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
theorem z_even (n : ℕ) : z (2 * (n + 1)) = 0 := by
…
```
Mentions: LatinSquare.z
theorem LatinSquare.numTransversalsZn 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$ sorry line 169 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, LT.lt, Nat, GE.ge, Odd, Membership.mem, Set, Set.Icc, HMul.hMul, HPow.hPow, Nat.factorial, LatinSquare.z
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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) := by
…
```
Mentions: LatinSquare.z
theorem LatinSquare.growthRateZn 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 sorry line 184 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Iff, True, Filter.Tendsto, Nat, Real, HMul.hMul, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, Real.log, LatinSquare.z, Nat.factorial, Filter.atTop, nhds, Neg.neg
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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)) := by
…
```
Mentions: LatinSquare.z
def LatinSquare.T The maximum number of transversals over all latin squares of order n line 191 source
Source documentation
The maximum number of transversals over all latin squares of order n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sup, LatinSquare, Finset.univ, numTransversals
4 instances, coercions and auxiliary constants left out.
```
def T (n : ℕ) : ℕ := Finset.sup Finset.univ (fun L : LatinSquare n => numTransversals L)
…
```
Mentions: LatinSquare, numTransversals
theorem LatinSquare.maxTransversalsBound 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}$ sorry line 202 source
Source documentation
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}$

depends on sorry what this means
Statement uses: Real, HMul.hMul, Real.sqrt, HDiv.hDiv, HSub.hSub, OfNat.ofNat, Nat, Real.exp, GE.ge, Membership.mem, Set, Set.Icc, HPow.hPow, Nat.factorial, LatinSquare.T
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem maxTransversalsBound :
    let c := Real.sqrt ((3 - Real.sqrt 3) / 6) * Real.exp (Real.sqrt 3 / 6)
…
```
Mentions: c
theorem LatinSquare.molsExistenceProblem MOLS existence problem: determine exactly which orders n admit a complete set of n - 1 mutually orthogonal latin squares sorry line 216 source
Source documentation
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.

depends on sorry what this means
Statement uses: Eq, Set, Nat, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Set.ofPred, LatinSquare.HasCompleteMOLS
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem molsExistenceProblem : answer(sorry) = {n : ℕ | HasCompleteMOLS n} := by
…
```
Mentions: LatinSquare.HasCompleteMOLS
theorem LatinSquare.molsOrder12 The smallest unresolved case of the MOLS existence problem: whether there are 11 mutually orthogonal latin squares of order 12 sorry line 224 source
Source documentation
The smallest unresolved case of the MOLS existence problem: whether there are 11 mutually orthogonal latin squares of order 12.

depends on sorry what this means
Statement uses: Iff, True, LatinSquare.HasCompleteMOLS, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem molsOrder12 : answer(sorry) ↔ HasCompleteMOLS 12 := by
…
```
Mentions: LatinSquare.HasCompleteMOLS