Number theory

Erdős 359 - part ii

Let

a_1< a_2 < ⋯

be an infinite sequence of integers such that

a_1=1

and

a_{i+1}

is the least integer which is not a sum of consecutive earlier

a_j

s. Show that

a_k / k ^ {1 + c} \to 0

for any

c > 0

References

erdosproblems.com/359

No one has attempted this yet.

Formal statement

Lean type

∀ (A : ℕ → ℕ),
  Erdos359.IsGoodFor A 1 → ∀ (c : ℝ), 0 < c → Filter.Tendsto (fun k => ↑(A k) / ↑k ^ (1 + c)) Filter.atTop (nhds 0)

What you must prove

import FormalConjectures.ErdosProblems.«359»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos359.erdos_359.parts.ii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/359.lean

Source type SHA-256: sha256:3b9ae2f344dc05104dafce9f974cd9e104efe01249cf250a137aaa58f541062f
Task id: fc-379fc029-parts-ii-718b97cc63-formalized-v1
Task commitment: sha256:0b1b6cd328d7a07c3c30daf0d9f758fe64f30e32359c56e9e8f2487bc3d48dc5

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.