Erdős problem 723 · problems.science

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

Sources

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

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

723.lean

Retained formal statement2 of 5

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.

FormalConjectures/ErdosProblems/723.leanErdos723.erdos_723.variants.bruck_ryser2 linesExact file

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

SolvedStatement only, no proof

Sources

Search problems.science