Erdős Problem 647

Reference: erdosproblems.com/647

theorem Erdos647.erdos_647 : sorry ↔ ∃ n > 24, ⨆ (m : Fin n), ↑m + (ArithmeticFunction.sigma 0) ↑m ≤ n + 2

Let $\tau(n)$ count the number of divisors of $n$. Is there some $n > 24$ such that $$ \max_{m < n}(m + \tau(m)) \leq n + 2? $$

theorem Erdos647.erdos_647.variants.twenty_four : ⨆ (m : Fin 24), ↑m + (ArithmeticFunction.sigma 0) ↑m ≤ 26

This is true for $n = 24$.

theorem Erdos647.erdos_647.variants.lim : sorry ↔ Filter.Tendsto (fun (n : ℕ) => ⨆ (m : Fin n), (ArithmeticFunction.sigma 0) ↑m + ↑m - n) Filter.atTop Filter.atTop

Erdős says 'it is extremely doubtful' that there are infinitely many such $n$, and in fact suggests that $$ lim_{n\to\infty} \max_{m < n}(\tau(m) + m − n) = \infty. $$

theorem Erdos647.erdos_647.variants.infinite : sorry ↔ ∀ (k : ℕ), {n : ℕ | ⨆ (m : ↑(Set.Ioo (n - k) n)), ↑m + (ArithmeticFunction.sigma 0) ↑m ≤ n + 2}.Infinite

Erdős says it 'seems certain' that for every $k$ there are infinitely many $n$ for which $$ \max_{n−k < m < n}(m + \tau(m)) ≤ n + 2. $$