Skip to content

Erdős problem 419

Start work

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

419.lean

Retained formal statement1 of 1

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

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

FormalConjectures/ErdosProblems/419.leanErdos419.erdos_4191 lineExact file
{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.