Erdős problem 1054 · problems.science

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$ . Show that $f$ is undefined at $n=2$ , i.e. we get the junk value $0$ .

Sources

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

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1054.lean

Retained formal statement3 of 5

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$ . Is it true that $\limsup f(n)/n=\infty$ ?

FormalConjectures/ErdosProblems/1054.leanErdos1054.erdos_1054.parts.iii1 lineExact file

1sorry ↔ ∃ A, A.HasDensity 1 ∧ Filter.limsup (fun n => ↑(Erdos1054.f n) / ↑n) Filter.atTop = ⊤

OpenStatement only, no proof

Sources

Search problems.science