Erdős problem 723
If there is a finite projective plane of order then must be a prime power?
Sources
FormalConjectures/ErdosProblems/
723.lean
Retained formal statement
This conjecture has been proved for .
∀ {P L : Type} [inst : Membership P L] [Fintype P] [Fintype L] (pp : Configuration.ProjectivePlane P L), Configuration.ProjectivePlane.order P L ≤ 11 → IsPrimePow (Configuration.ProjectivePlane.order P L)SolvedStatement only, no proof