Erdős Problem 1073

Reference: erdosproblems.com/1073

noncomputable def Erdos1073.A (x : ℕ) : ℝ

Let $A(x)$ count the number of composite $u < x$ such that $n!+1 \equiv 0 (\mod u)$ for some $n$.

Equations

• Erdos1073.A x = ↑{u : ℕ | u.Composite ∧ ∃ (n : ℕ), n.factorial + 1 ≡ 0 [MOD u] ∧ u < x}.ncard

theorem Erdos1073.erdos_1073 : (∃ (o : ℕ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ (x : ℕ), A x ≤ ↑x ^ o x) ↔ sorry

Is it true that $A(x) \le x^{o(1)}$?