Erdős Problem 723

Also known as the prime power conjecture.

Reference: erdosproblems.com/723

theorem Erdos723.erdos_732 {P L : Type} [Membership P L] : (∀ (pp : Configuration.ProjectivePlane P L), IsPrimePow (Configuration.ProjectivePlane.order P L)) ↔ sorry

If there is a finite projective plane of order $n$ then must $n$ be a prime power?

theorem Erdos723.erdos_732.prime_pow_is_projplane_order {P L : Type} [Membership P L] (n : ℕ) : IsPrimePow n → ∃ (pp : Configuration.ProjectivePlane P L), Configuration.ProjectivePlane.order P L = n

These always exist if $n$ is a prime power.

theorem Erdos723.erdos_732.leq_11 {P L : Type} [Membership P L] (pp : Configuration.ProjectivePlane P L) : Configuration.ProjectivePlane.order P L ≤ 11 → IsPrimePow (Configuration.ProjectivePlane.order P L)

This conjecture has been proved for $n \leq 11$.

theorem Erdos723.bruck_ryser {P L : Type} [Membership P L] (n : ℕ) (pp : Configuration.ProjectivePlane P L) (hpp : Configuration.ProjectivePlane.order P L = n) : n ≡ 1 [MOD 4] ∨ n ≡ 2 [MOD 4] → ∃ (a : ℕ) (b : ℕ), n = a ^ 2 + b ^ 2

Bruck and Ryser have proved that if $n \equiv 1 (\mod 4)$ or $n \equiv 2 (\mod 4)$ then $n$ must be the sum of two squares.