Skip to content

Erdős problem 946

Start work

There are infinitely many nn such that τ(n)=τ(n+1)τ(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

Open selected source

FormalConjectures/ErdosProblems/

946.lean

Retained formal statement4 of 5

There are infinitely many nn such that τ(n)=τ(n+5040)τ(n) = τ(n + 5040). Proved in [Sp81].

FormalConjectures/ErdosProblems/946.leanErdos946.erdos_946.variants.spiro_50401 lineExact file
{n | (ArithmeticFunction.sigma 0) n = (ArithmeticFunction.sigma 0) (n + 5040)}.Infinite
SolvedStatement only, no proof