If there is a finite projective plane of order $n$ then must $n$ be a prime power?A finite projective plane of order $n$ is a collection of subsets of ${1, \dots, n^{2} + n + 1}$ of size $n + 1$ such that every pair of elements is contained in exactly one set.

Worked, still open.

combinatorics · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is **not known in general**. The statement

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 · open (literature)

theorem erdos_723 :
    answer(sorry) ↔ ∀ {P L : Type} (_: Membership P L) (_ : Fintype P) (_ : Fintype L),
      ∀ pp : ProjectivePlane P L, IsPrimePow pp.order

formal-conjectures/723.lean ↗

links

finite projective plane · reference

proved · reference

status

open

evidence

formal

links

status

Search Vela