FormalConjectures.ErdosProblems.«1074»

/-
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 1074

Reference: erdosproblems.com/1074


namespace Erdos1074


open scoped Nat

open Nat

The EHS numbers (after Erdős, Hardy, and Subbarao) are those $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$.

abbrev EHSNumbers : Set ℕ := {m | 1 ≤ m ∧ ∃ p, p.Prime ∧ ¬p ≡ 1 [MOD m] ∧ p ∣ m ! + 1}

The Pillai primes are those primes $p$ such that there exists an $m \ge 1$ with $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$

abbrev PillaiPrimes : Set ℕ := {p | p.Prime ∧ ∃ m ≥ 1, ¬p ≡ 1 [MOD m] ∧ p ∣ m ! + 1}


@[category test, AMS 11]
theorem two_not_mem_pillaiPrimes : ¬ 2 ∈ PillaiPrimes := by⊢ 2 ∉ PillaiPrimes
  norm_num⊢ ∀ (x : ℕ), 1 ≤ x → ¬2 ≡ 1 [MOD x] → (x ! + 1) % 2 = 1
  intro m hmm:ℕhm:1 ≤ m⊢ ¬2 ≡ 1 [MOD m] → (m ! + 1) % 2 = 1 hm:ℕhm:1 ≤ mh:¬2 ≡ 1 [MOD m]⊢ (m ! + 1) % 2 = 1
  exact (Nat.dvd_factorial (bym:ℕhm:1 ≤ mh:¬2 ≡ 1 [MOD m]⊢ 0 < succ 1 decideAll goals completed! 🐙) (hm.lt_of_ne (bym:ℕhm:1 ≤ mh:¬2 ≡ 1 [MOD m]⊢ 1 ≠ m boundAll goals completed! 🐙))).modEq_zero_nat.add_right 1


@[category test, AMS 11]
theorem twentyThree_mem_pillaiPrimes : 23 ∈ PillaiPrimes := by⊢ 23 ∈ PillaiPrimes
  norm_num⊢ ∃ m, 1 ≤ m ∧ ¬23 ≡ 1 [MOD m] ∧ 23 ∣ m ! + 1
  use 14h⊢ 1 ≤ 14 ∧ ¬23 ≡ 1 [MOD 14] ∧ 23 ∣ 14! + 1
  decideAll goals completed! 🐙

Let $S$ be the set of all $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$. Does $$ \lim\frac{|S\cap[1, x]|}{x} $$ exist?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_1074.parts.i : answer(sorry) ↔ ∃ c, EHSNumbers.HasDensity c := by⊢ True ↔ ∃ c, EHSNumbers.HasDensity c
  sorryAll goals completed! 🐙

Let $S$ be the set of all $m\geq 1$ such that there exists a prime $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$. What is $$ \lim\frac{|S\cap[1, x]|}{x}? $$

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_1074.parts.ii : EHSNumbers.HasDensity answer(sorry) := by⊢ EHSNumbers.HasDensity sorry
  sorryAll goals completed! 🐙

Similarly, if $P$ is the set of all primes $p$ such that there exists an $m$ with $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$, then does $$ \lim\frac{|P\cap[1, x]|}{\pi(x)} $$ exist?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_1074.parts.iii : answer(sorry) ↔ ∃ c, PillaiPrimes.HasDensity c {p | p.Prime} := by⊢ True ↔ ∃ c, PillaiPrimes.HasDensity c {p | Nat.Prime p}
  sorryAll goals completed! 🐙

Similarly, if $P$ is the set of all primes $p$ such that there exists an $m$ with $p\not\equiv 1\pmod{m}$ such that $m! + 1 \equiv 0\pmod{p}$, then what is $$ \lim\frac{|P\cap[1, x]|}{\pi(x)}? $$

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_1074.parts.iv :
    PillaiPrimes.HasDensity answer(sorry) {p | p.Prime} := by⊢ PillaiPrimes.HasDensity sorry {p | Nat.Prime p}
  sorryAll goals completed! 🐙

Pillai [Pi30] raised the question of whether there exist any primes in $P$. This was answered by Chowla, who noted that, for example, $14! + 1 \equiv 18! + 1 \equiv 0 \pmod{23}$.

@[category test, AMS 11]
theorem erdos_1074.variants.mem_pillaiPrimes : 23 ∈ PillaiPrimes := by⊢ 23 ∈ PillaiPrimes
  norm_num⊢ ∃ m, 1 ≤ m ∧ ¬23 ≡ 1 [MOD m] ∧ 23 ∣ m ! + 1
  exact ⟨14, by⊢ 1 ≤ 14 ∧ ¬23 ≡ 1 [MOD 14] ∧ 23 ∣ 14! + 1 decideAll goals completed! 🐙⟩

Erdős, Hardy, and Subbarao proved that $S$ is infinite.

Formal proof linked here provided by AlphaProof.

@[category research solved, AMS 11, formal_proof using formal_conjectures at
"https://github.com/mzhorvath1/formal-conjectures/blob/3dec597bd1a73778760b761712a1fc5fb24bc5d7/FormalConjectures/ErdosProblems/1074.lean#L99"]
theorem declaration uses 'sorry'erdos_1074.variants.EHSNumbers_infinite : EHSNumbers.Infinite := by⊢ EHSNumbers.Infinite
  sorryAll goals completed! 🐙

Erdős, Hardy, and Subbarao proved that $P$ is infinite.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_1074.variants.PillaiPrimes_infinite : PillaiPrimes.Infinite := by⊢ PillaiPrimes.Infinite
  sorryAll goals completed! 🐙

The sequence $S$ begins $8, 9, 13, 14, 15, 16, 17, ...$

@[category test, AMS 11]
theorem declaration uses 'sorry'erdos_1074.variants.EHSNumbers_init :
    nth EHSNumbers '' (Set.Icc 0 6) = {8, 9, 13, 14, 15, 16, 17} := by⊢ nth EHSNumbers '' Set.Icc 0 6 = {8, 9, 13, 14, 15, 16, 17}
  sorryAll goals completed! 🐙

The sequence $P$ begins $23, 29, 59, 61, 67, 71, ...$

@[category test, AMS 11]
theorem declaration uses 'sorry'erdos_1074.variants.PillaiPrimes_init :
    nth PillaiPrimes '' (Set.Icc 0 5) = {23, 29, 59, 61, 67, 71} := by⊢ nth PillaiPrimes '' Set.Icc 0 5 = {23, 29, 59, 61, 67, 71}
  sorryAll goals completed! 🐙

Regarding the first question, Hardy and Subbarao computed all EHS numbers up to $2^{10}$, and write "...if this trend conditions we expect [the limit] to be around 0.5, if it exists."

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_1074.variants.EHSNumbers_one_half : EHSNumbers.HasDensity (1 / 2) := by⊢ EHSNumbers.HasDensity (1 / 2)
  sorryAll goals completed! 🐙


end Erdos1074