MOLS Existence Problem: Completeness of mutually orthogonal Latin square sets

### What is the conjecture

A **Latin square** of order $n$ is an $n \times n$ array filled with $n$ different symbols, with each symbol appearing exactly once per row and column.

Two Latin squares $A$ and $B$ of the same order are **orthogonal** if, when superimposed cell by cell, all $n^2$ ordered pairs $(A[i,j], B[i,j])$ are distinct.

A **complete set of Mutually Orthogonal Latin Squares (MOLS)** of order $n$ is a collection of $n - 1$ Latin squares, all mutually orthogonal to one another. This is the maximum possible size.

**MOLS Existence Problem**: For which orders $n$ does a complete set of $n - 1$ MOLS exist? As of now, the smallest undetermined case is $n = 12$.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Problems_in_Latin_squares | https://en.wikipedia.org/wiki/Mutually_orthogonal_Latin_squares

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-02-12)

Building blocks (1-3; from search results):
- Latin square definitions
- Ordered pair collections and distinctness (Mathlib)
- Cardinality and finiteness predicates

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of orthogonality for Latin squares
- Complete set characterization and maximum completeness properties

Rating justification (1-2 sentences): Beyond Latin square definitions, this requires formalizing the orthogonality relation (comparing two squares element-wise) and defining completeness as a maximum-size family. The problem itself is stated as an existence/decision problem over order values, requiring moderate additional infrastructure.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)