projective_plane_order_6
Provedcombinatoricsdesigntheoryfinitegeometryproved
Non-existence of projective plane of order 6: No projective plane of order 6 exists. Proved by exhaustive search using computers (Lam–Thiel–Swiercz 1989). The next open case is order 12: does a projective plane of order 12 exist? The Bruck-Ryser theorem eliminates some orders but not 12.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem projective_plane_order_6 :
¬∃ (points lines : Finset (Fin 43)),
points.card = 43 ∧ lines.card = 43 ∧
∃ (incident : Fin 43 → Fin 43 → Prop),
(∀ i j : Fin 43, i ≠ j → ∃! l : Fin 43, incident i l ∧ incident j l) ∧
(∀ l : Fin 43, {i : Fin 43 | incident i l}.ncard = 7) := by
sorrySource