FormalConjectures.ErdosProblems.«723»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 723: The prime power conjecture.

Reference: erdosproblems.com/723


open Configuration


namespace Erdos723

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

@[category research open, AMS 5]
theorem declaration uses 'sorry'erdos_723 :
    answer(sorry) ↔ ∀ {P L : Type} (_: Membership P L) (_ : Fintype P) (_ : Fintype L),
      ∀ pp : ProjectivePlane P L, IsPrimePow pp.order := by⊢ True ↔
  ∀ {P L : Type} (x : Membership P L) (x_1 : Fintype P) (x_2 : Fintype L) (pp : ProjectivePlane P L),
    IsPrimePow (ProjectivePlane.order P L)
  sorryAll goals completed! 🐙

These always exist if $n$ is a prime power.

@[category research solved, AMS 5]
theorem declaration uses 'sorry'erdos_723.variants.prime_power_is_projplane_order :
    ∀ n, IsPrimePow n → ∃ (P L : Type) (_ : Membership P L) (_ : Fintype P) (_ : Fintype L)
      (pp : ProjectivePlane P L), pp.order = n := by⊢ ∀ (n : ℕ), IsPrimePow n → ∃ P L x x_1 x_2 pp, ProjectivePlane.order P L = n
  sorryAll goals completed! 🐙

This conjecture has been proved for $n \leq 11$.

@[category research solved, AMS 5]
theorem declaration uses 'sorry'erdos_723.variants.leq_11 {P L : Type} [Membership P L] [Fintype P] [Fintype L] :
    ∀ pp : ProjectivePlane P L, pp.order ≤ 11 → IsPrimePow pp.order := byP:TypeL:Typeinst✝²:Membership P Linst✝¹:Fintype Pinst✝:Fintype L⊢ ∀ (pp : ProjectivePlane P L), ProjectivePlane.order P L ≤ 11 → IsPrimePow (ProjectivePlane.order P L)
  sorryAll goals completed! 🐙

It is open whether there exists a projective plane of order 12.

@[category research open, AMS 5]
theorem declaration uses 'sorry'erdos_723.variants.eq_12 : answer(sorry) ↔
    ∃ (P L : Type) (_ : Membership P L) (_ : Fintype P) (_ : Fintype L) (pp : ProjectivePlane P L),
      pp.order = 12 := by⊢ True ↔ ∃ P L x x_1 x_2 pp, ProjectivePlane.order P L = 12
  sorryAll goals completed! 🐙

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.

@[category research solved, AMS 5]
theorem declaration uses 'sorry'erdos_723.variants.bruck_ryser {P L : Type} [Membership P L] [Fintype P] [Fintype L]
    (n : ℕ) (pp : ProjectivePlane P L) (hpp : pp.order = n) :
    (n ≡ 1 [MOD 4] ∨ n ≡ 2 [MOD 4]) → ∃ a b, n = a ^ 2 + b ^ 2 := byP:TypeL:Typeinst✝²:Membership P Linst✝¹:Fintype Pinst✝:Fintype Ln:ℕpp:ProjectivePlane P Lhpp:ProjectivePlane.order P L = n⊢ n ≡ 1 [MOD 4] ∨ n ≡ 2 [MOD 4] → ∃ a b, n = a ^ 2 + b ^ 2
  sorryAll goals completed! 🐙


end Erdos723