Erdős Problem 359: Is Good For 1 Asymptotic
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_k ~ \frac{k \log k}{\log \l...
Mathematical 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 .
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_359.variants.isGoodFor_1_asymptotic
theorem erdos_359.variants.isGoodFor_1_asymptotic (A : ℕ → ℕ) (hA : IsGoodFor A 1) : (fun k ↦ (A k : ℝ)) ~[atTop] (fun k ↦ k * (k : ℝ).log / (k : ℝ).log.log) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References