Erdős Problem 1072

Reference: erdosproblems.com/1072

noncomputable def Erdos1072.f (p : ℕ) : ℕ

For any prime $p$, let $f(p)$ be the least integer such that $f(p)! + 1 \equiv 0 \mod p$.

Equations

• Erdos1072.f p = sInf {n : ℕ | n.factorial + 1 ≡ 0 [MOD p]}

theorem Erdos1072.erdos_1072a : sorry ↔ {p : ℕ | Nat.Prime p ∧ f p = p - 1}.Infinite

Is it true that there are infinitely many $p$ for which $f(p) = p − 1$?

theorem Erdos1072.erdos_1072b : sorry ↔ ∃ P ⊆ {p : ℕ | Nat.Prime p}, P.HasDensity 1 {p : ℕ | Nat.Prime p} ∧ Filter.Tendsto (fun (p : ℕ) => ↑(f p) / ↑p) (Filter.atTop ⊓ Filter.principal P) (nhds 0)

Is it true that $f(p)/p \to 0$ for $p \to \infty$ in a density 1 subset of the primes?

theorem Erdos1072.erdos_1072a.variants.littleo : (fun (x : ℕ) => ↑({p : ℕ | Nat.Prime p ∧ f p = p - 1}.interIcc 0 x).ncard) =o[Filter.atTop] fun (x : ℕ) => ↑x / Real.log ↑x

Erdős, Hardy, and Subbarao [HaSu02], believed that the number of $p \le x$ for which $f(p)=p−1$ is $o(x/\log x)$.

[HaSu02] Hardy, G. E. and Subbarao, M. V., A modified problem of Pillai and some related questions. Amer. Math. Monthly (2002), 554--559.