Number theory

Erdős 359 - isGoodFor 1 asymptotic

Suppose monotone sequence

A

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_k ~ \frac{k \log k}{\log \log k}

References

erdosproblems.com/359

No one has attempted this yet.

Formal statement

Lean type

∀ (A : ℕ → ℕ),
  Erdos359.IsGoodFor A 1 →
    Asymptotics.IsEquivalent Filter.atTop (fun k => ↑(A k)) fun k => ↑k * Real.log ↑k / Real.log (Real.log ↑k)

What you must prove

import FormalConjectures.ErdosProblems.«359»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos359.erdos_359.variants.isGoodFor_1_asymptotic" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/359.lean

Source type SHA-256: sha256:e8d3274560c69189522bcba232b7c4eed67b4ba51c1bfeb8843d7ee8293f764f
Task id: fc-379fc029-variants-isgoodfor-1-asymptotic-352d1a6275-formalized-v1
Task commitment: sha256:a53c9aa5311e23abd841499ec647a4cb6e797e913eccd2322f86a8ec77650698

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.