Skip to content

Erdős problem 723

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

723.lean

Retained formal statement4 of 5

This conjecture has been proved for n11n \leq 11.

FormalConjectures/ErdosProblems/723.leanErdos723.erdos_723.variants.leq_112 linesExact file
∀ {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

Search problems.science

Find a Problem, Result, source, or page