Erdős problem 359
Suppose monotone sequence satisfies the following: A 0 = 1 and for all j, A (j + 1) is the smallest natural number that cannot be written as a sum of consecutive terms of A 0, ..., A j. Then it is conjectured that .
Sources
FormalConjectures/ErdosProblems/
359.lean
Retained formal statement
Suppose monotone sequence satisfies the following: A 0 = 1 and for all j, A (j + 1) is the smallest natural number that cannot be written as a sum of consecutive terms of A 0, ..., A j. Then it is conjectured that .
∀ (A : ℕ → ℕ), Erdos359.IsGoodFor A 1 → Asymptotics.IsEquivalent Filter.atTop (fun k => ↑(A k)) fun k => ↑k * Real.log ↑k / Real.log (Real.log ↑k)OpenStatement only, no proof