Chapter 37, Corollary: Latin square asymptotic

Proved

BookSixth.latin_asymptotic

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

As the order n tends to infinity, L(n)^(1/n²)/n tends to exp(−2), where L(n) counts labeled Latin squares. The totalized value at n=0 has no effect on this limit.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.latin_asymptotic  :
    Filter.Tendsto (fun n : ℕ => (latinCount n : ℝ) ^ (1 / (n : ℝ)^2) / (n : ℝ))
      Filter.atTop (nhds (Real.exp (-2))) := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 37, Corollary: Latin square asymptotic, p. 266. https://doi.org/10.1007/978-3-662-57265-8_37

View graph