OP-00019 Open

The prime power conjecture for finite projective planes

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

Source: Folklore; open since Veblen and Bussey (1906) constructed projective planes of every prime-power order. Listed by Erdős (1981); erdosproblems.com/723.

Classification

Primary: CO — Combinatorics
Keywords: Erdős problems, finite projective planes

References

@article{veblenbussey1906,
  author = {Veblen, Oswald and Bussey, W. H.},
  title = {Finite projective geometries},
  journal = {Transactions of the American Mathematical Society},
  volume = {7},
  pages = {241--259},
  year = {1906}
}

@article{bruckryser1949,
  author = {Bruck, R. H. and Ryser, H. J.},
  title = {The nonexistence of certain finite projective planes},
  journal = {Canadian Journal of Mathematics},
  volume = {1},
  pages = {88--93},
  year = {1949}
}

@article{lam1989,
  author = {Lam, C. W. H. and Thiel, L. and Swiercz, S.},
  title = {The non-existence of finite projective planes of order 10},
  journal = {Canadian Journal of Mathematics},
  volume = {41},
  pages = {1117--1123},
  year = {1989}
}

@article{erdos1981,
  author = {Erd{\H{o}}s, Paul},
  title = {On the combinatorial problems which I would most like to see solved},
  journal = {Combinatorica},
  volume = {1},
  pages = {25--42},
  year = {1981}
}

@misc{erdosproblems723,
  title = {Erdős Problem \#723},
  howpublished = {erdosproblems.com},
  url = {https://www.erdosproblems.com/723}
}

@misc{formalconjectures,
  author = {{The Formal Conjectures Authors}},
  title = {Formal Conjectures},
  url = {https://github.com/google-deepmind/formal-conjectures/blob/0771383387505c96d1b2f6a3d35088ad00892c5c/FormalConjectures/ErdosProblems/723.lean#L32},
  note = {Lean statement under Apache-2.0; problem text under CC BY 4.0, or CC BY-SA 4.0 where it is based on Wikipedia}
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00019.

/-- OP-00019: The prime power conjecture for finite projective planes -/
def Problem_OP_00019 : Prop :=
  ∀ {P L : Type} (x : Membership P L) (x_1 : Fintype P) (x_2 : Fintype L)
      (pp : Configuration.ProjectivePlane P L), IsPrimePow (Configuration.ProjectivePlane.order P L)

Formalised by The Formal Conjectures Authors (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "<published revision>"

In your proof:

import RegistryProblems.OP_00019

theorem resolution : RegistryProblems.Problem_OP_00019 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it:

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00019"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:

theorem disproof : ¬ RegistryProblems.Problem_OP_00019 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.

OP-00019, "The prime power conjecture for finite projective planes", clopen.solutions.