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 statement2 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 $f(n)=o(n)$ for almost all $n$ ?

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

1sorry ↔ ∃ A, A.HasDensity 1 ∧ (fun n => ↑(Erdos1054.f ↑n)) =o[Filter.atTop] fun n => ↑↑n

OpenStatement only, no proof

Sources

Search problems.science