Erdős problem 253

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$ .

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

253.lean

Retained formal statement1 of 1

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$ .

FormalConjectures/ErdosProblems/253.leanErdos253.erdos_2535 linesExact file

1¬∀ (a : ℕ → ℕ),2    0 < a 0 →3      Erdos253.RepresentsAPs a →4        Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 1) →5          subsetSums (Set.range a) ∈ Filter.cofinite

SolvedStatement only, no proof