Erdős Problem 456

References:

• erdosproblems.com/456
• [Er79e] Erdős, Paul, Some unconventional problems in number theory. Astérisque (1979), 73--82.

noncomputable def Erdos456.p (n : ℕ) : ℕ

Let $p_n$ be the smallest prime $\equiv 1\pmod{n}$.

Equations

• Erdos456.p n = sInf {k : ℕ | Nat.Prime k ∧ k ≡ 1 [MOD n]}

noncomputable def Erdos456.m (n : ℕ) : ℕ

Let $m_n$ be the smallest integer such that $n\mid \phi(m_n)$.

Equations

• Erdos456.m n = sInf {k : ℕ | 0 < k ∧ n ∣ k.totient}

theorem Erdos456.erdos_456.parts.i : sorry ↔ Filter.Tendsto (fun (N : ℕ) => ↑(Nat.count {n : ℕ | m n < p n} N) / ↑N) Filter.atTop (nhds 1)

Is it true that $m_n<p_n$ for almost all $n$?

theorem Erdos456.erdos_456.parts.ii : sorry ↔ ∃ (A : Set ℕ), Filter.Tendsto (fun (N : ℕ) => ↑(Nat.count A N) / ↑N) Filter.atTop (nhds 1) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(p n) / ↑(m n)) (Filter.atTop ⊓ Filter.principal A) Filter.atTop

Does $p_n/m_n \to \infty$ for almost all $n$?

theorem Erdos456.erdos_456.parts.iii : sorry ↔ {q : ℕ | Nat.Prime q ∧ ∀ (n : ℕ), m n = q ↔ n = q - 1}.Infinite

Are there infinitely many primes $p$ such that $p-1$ is the only $n$ for which $m_n=p$?

theorem Erdos456.erdos_456.variants.linniks_theorem : ∃ (L : ℝ), (fun (n : ℕ) => ↑(p n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ L

Linnik's theorem implies that $p_n\leq n^{O(1)}$.

theorem Erdos456.erdos_456.variants.mn_leq_pn (n : ℕ) : m n ≤ p n

It is trivial that $m_n \leq p_n$ always.

theorem Erdos456.erdos_456.variants.infinitely_many_n : {n : ℕ | m n < p n}.Infinite

Erdős [Er79e] writes it is 'easy to show' that for infinitely many $n$ we have $m_n < p_n$.

theorem Erdos456.erdos_456.variants.m_div_n : ∃ (A : Set ℕ), Filter.Tendsto (fun (N : ℕ) => ↑(Nat.count A N) / ↑N) Filter.atTop (nhds 1) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(m n) / ↑n) (Filter.atTop ⊓ Filter.principal A) Filter.atTop

Erdős [Er79e] writes it is 'easy to show' that $m_n/n \to \infty$ for almost all $n$.