Erdős problem 419 · problems.science

If $\tau(n)$ counts the number of divisors of $n$ , then what is the set of limit points of $\frac{\tau((n+1)!)}{\tau(n!)}?$

Sources

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

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

419.lean

Retained formal statement1 of 1

If $\tau(n)$ counts the number of divisors of $n$ , then what is the set of limit points of $\frac{\tau((n+1)!)}{\tau(n!)}?$

The limit points are exactly $\{1\} \cup \{1+1/k : k \geq 1\}$ .

FormalConjectures/ErdosProblems/419.leanErdos419.erdos_4191 lineExact file

1{x | MapClusterPt x Filter.atTop Erdos419.factorialDivisorRatio} = Erdos419.limitPointSet

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.