Prime power conjecture: does a finite projective plane of order $n$ force $n$ to be a prime power? (Erdős #723)

If there is a finite projective plane of order $n$, must $n$ be a prime power? Here a finite projective plane of order $n$ is a collection of subsets ('lines') of $\{1,\ldots,n^2+n+1\}$, each of size $n+1$, such that every pair of elements is contained in exactly one line. (Equivalently: an incidence structure with $n^2+n+1$ points and $n^2+n+1$ lines in which each line has $n+1$ points, each point lies on $n+1$ lines, and any two distinct points lie on exactly one common line.) A single explicit projective plane of non-prime-power order would disprove the conjecture; the first order for which existence is undecided is $n=12$.

Acceptance. FULLY RESOLVES: (a) a counterexample — an explicit incidence structure of stated non-prime-power order $n$ (the full list of $n^2+n+1$ lines or the incidence matrix) with a verification program a reviewer can run confirming every pair of points lies in exactly one line; or (b) a proof that every finite projective plane has prime-power order — machine-checkable (Lean, building on the existing formal statement) preferred, else a complete written proof. ADVANCES: (a) a proof (computational with reproducible certificates, or theoretical) that no projective plane of order 12 exists — this settles the first open case and would be a landmark even though the general conjecture remains; (b) exclusion of order-12 planes admitting specific automorphism groups or substructures strictly beyond the exclusions cited in the submission's own literature review, with search code and exhaustiveness certificates; (c) a new number-theoretic non-existence criterion applicable to orders not excluded by the Bruck–Ryser condition, with proof; (d) an independently reproducible certified re-verification of a major existing exclusion, with published certificates, where none exists. Deliver the incidence data plus checking code, or the proof file, or the search code with certificates and the precisely stated excluded class.