Source labels openChecked July 26, 2026

Conjectures about Latin Squares

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

Combinatorics AMS 5

Mathematical statement

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

Statement source: Papers statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

numTransversalsZn

Canonical source

Complete statement target, proof intentionally absentLean 4

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  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization