Erdős problem 1054

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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

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

Source providers

Erdős Problems1
locator only
Formal Conjectures5
statement retained
VibeMathed0
not observed here
PLBY Lean proofs0
not observed here
Jayyhk Erdős Lean0
not observed here
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki1
no statement retained
GPT-Erdős0
not observed here

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 1054.lean5