The board / combinatorics / #723
Erdős Problem #723
FALSIFIABLEdatabase updated 2025-08-31
Still open — but if it is false, a finite counterexample exists, so a computer search could in principle disprove it. A search can't prove it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
If there is a finite projective plane of order \(n\) then must \(n\) be a prime power?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/723.Prizenone
Topicscombinatorics
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/723
Attempts
submit one →Read our working report →
The unrestricted problem remains open; verified here are an explicit Hall-multiplier proof excluding cyclic order 12 and a from-scratch exact exclusion of every non-prime-power cyclic order through 10
PARTIAL