Documentation

FormalConjectures.ErdosProblems.«1074»

Erdős Problem 1074 #

Reference: erdosproblems.com/1074

source
@[reducible, inline]
abbrev Nat.EHSNumbers :
Set ℕ

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}$.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Nat.PillaiPrimes :
    Set ℕ

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

    Equations
    Instances For
      source
      theorem Erdos1074.erdos_1074.parts.i.i :
      (∃ (c : ℝ), Nat.EHSNumbers.HasDensity c) ↔ sorry

      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?

      source
      theorem Erdos1074.erdos_1074.parts.i.ii :
      Nat.EHSNumbers.HasDensity sorry

      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}? $$

      source
      theorem Erdos1074.erdos_1074.parts.ii.i :
      (∃ (c : ℝ), Nat.PillaiPrimes.HasDensity c {p : ℕ | Nat.Prime p}) ↔ sorry

      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?

      source
      theorem Erdos1074.erdos_1074.parts.ii.ii :
      Nat.PillaiPrimes.HasDensity sorry {p : ℕ | Nat.Prime p}

      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)}? $$

      source
      theorem Erdos1074.erdos_1074.variants.mem_pillaiPrimes :
      23 ∈ Nat.PillaiPrimes

      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}$.

      source
      theorem Erdos1074.erdos_1074.variants.EHSNumbers_infinite :
      Nat.EHSNumbers.Infinite

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

      source
      theorem Erdos1074.erdos_1074.variants.PillaiPrimes_infinite :
      Nat.PillaiPrimes.Infinite

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

      source
      theorem Erdos1074.erdos_1074.variants.EHSNumbers_init :
      Nat.nth Nat.EHSNumbers '' Set.Icc 0 6 = {8, 9, 13, 14, 15, 16, 17}

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

      source
      theorem Erdos1074.erdos_1074.variants.PillaiPrimes_init :
      Nat.nth Nat.PillaiPrimes '' Set.Icc 0 5 = {23, 29, 59, 61, 67, 71}

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

      source
      theorem Erdos1074.erdos_1074.variants.EHSNumbers_one_half :
      Nat.EHSNumbers.HasDensity (1 / 2)

      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."