Let $a_1 < a_2 < \dotsc$ be an infinite sequence of positive integers such that
$\frac{a_{i+1}}{a_i} \to 1$. If every arithmetic progression contains infinitely many
integers which are the sum of distinct $a_i$ then every sufficiently large integer is
the sum of distinct $a_i$.
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_253 : ¬ ∀ a : ℕ → ℕ, 0 < a 0 →
RepresentsAPs a → (Filter.atTop.Tendsto (fun n ↦ (a <| n + 1 : ℝ) / a n) (𝓝 1)) →
subsetSums (Set.range a) ∈ Filter.cofinite
