Erdős problem 946 · problems.science

There are infinitely many $n$ such that $τ(n) = τ(n+1)$ . Proved in [He84]. Here τ is the divisor counting function, which is σ 0 in mathlib.

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

946.lean

Retained formal statement3 of 5

Improved lower bound in [Hi85]: $Ω(x / (\log \log x)^3)$ .

FormalConjectures/ErdosProblems/946.leanErdos946.erdos_946.variants.hildebrand_lower_bound1 lineExact file

1(fun x => x / Real.log (Real.log x) ^ 3) =O[Filter.atTop] Erdos946.erdos946Count

SolvedStatement only, no proof