Number theory

Erdős 359 - part i

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 \to \infty

References

erdosproblems.com/359

No one has attempted this yet.

Formal statement

Lean type

∀ (A : ℕ → ℕ), Erdos359.IsGoodFor A 1 → Filter.Tendsto (fun k => ↑(A k) / ↑k) Filter.atTop Filter.atTop

What you must prove

import FormalConjectures.ErdosProblems.«359»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/359.lean

Source type SHA-256: sha256:635c639b1c592f92081bdce30eeb599c00f3d01032e21c9b242675b2be654e7a
Task id: fc-379fc029-parts-i-d26eadd5f5-formalized-v1
Task commitment: sha256:94cb1fdf2fab1eef783673de6221e18ce0ac5e16df4a8868b4248160f090787c

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.