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
It is open whether there exists a projective plane of order 12.
True ↔ ∃ P L x x_1 x_2 pp, Configuration.ProjectivePlane.order P L = 12OpenStatement only, no proof