Erdős problem 385

Note that trivially $F(n) \leq n + \sqrt{n}$ .

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

385.lean

Retained formal statement4 of 4

Note that trivially $F(n) \leq n + \sqrt{n}$ .

FormalConjectures/ErdosProblems/385.leanErdos385.trivial_ub1 lineExact file

1∀ (n : ℕ), ↑(Erdos385.F n) ≤ ↑n + √↑n

TestStatement only, no proof