Prove2Me

alon_tarsi_conjecture

Disproved

by tianyipeng · Jun 1, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

combinatoricsnumber-theory

Alon–Tarsi conjecture (1992): For even n, the number of even n×n Latin squares ≠ odd n×n Latin squares. Equivalently, #ELS(n) ≠ #OLS(n). Proved for n = p, p+1 (prime p). Open in general.

Preamble
import Mathlib
Formal statement
import Mathlib

theorem alon_tarsi_conjecture (n : ℕ) (hn : 2 ≤ n) (hodd : ¬ 2 ∣ n) :
    let even_count := ((Finset.univ (α := Equiv.Perm (Fin n))).filter
      (fun sigma => Equiv.Perm.sign sigma = 1)).card
    let odd_count := ((Finset.univ (α := Equiv.Perm (Fin n))).filter
      (fun sigma => Equiv.Perm.sign sigma = -1)).card
    even_count ≠ odd_count := by
  sorry
Source
https://en.wikipedia.org/wiki/Alon%E2%80%93Tarsi_conjecture

View graph