Erdős Problem 893

References:

• erdosproblems.com/893
• [KoLu25] V. Kovač and F. Luca, On the number of divisors of Mersenne numbers. arXiv:2506.04883 (2025).

def Erdos893.f (n : ℕ) : ℕ

Definition of function $f(n) := \sum_{1\leq k\leq n}\tau(2^k-1)$. Here $\tau$ is the divisor counting function, which is σ 0 in mathlib.

Equations

• Erdos893.f n = ∑ k ∈ Finset.Icc 1 n, (ArithmeticFunction.sigma 0) (2 ^ k - 1)

theorem Erdos893.erdos_893 : Filter.Tendsto (fun (n : ℕ) => ↑(f (2 * n)) / ↑(f n)) Filter.atTop Filter.atTop ↔ sorry

Does the limit $\lim_{n\to\infty} \frac{f(2n)}{f(n)}$ tend to infinity?

(Other finite limits have been ruled out by [KoLu25], see below)

theorem Erdos893.erdos_893.variants.unbounded : ¬BddAbove (Set.range fun (n : ℕ) => ↑(f (2 * n)) / ↑(f n))

Kovač and Luca [KoLu25] (building on a heuristic independently found by Cambie (personal communication)) have shown that there is no finite limit, in that $\lim_{n\to\infty} \frac{f(2n)}{f(n)}$ is unbounded.