Erdős problem 946

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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

946.lean

Retained formal statement2 of 5

The number of $n \le x$ with $τ(n) = τ(n+1)$ is at least $x / (\log x)^7$ for all sufficiently large $x$ . Proved in [He84].

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

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

SolvedStatement only, no proof