Skip to content

Erdős problem 253

Let a1<a2<a_1 < a_2 < \dotsc be an infinite sequence of positive integers such that ai+1ai1\frac{a_{i+1}}{a_i} \to 1. If every arithmetic progression contains infinitely many integers which are the sum of distinct aia_i then every sufficiently large integer is the sum of distinct aia_i.

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

253.lean

Retained formal statement1 of 1

Let a1<a2<a_1 < a_2 < \dotsc be an infinite sequence of positive integers such that ai+1ai1\frac{a_{i+1}}{a_i} \to 1. If every arithmetic progression contains infinitely many integers which are the sum of distinct aia_i then every sufficiently large integer is the sum of distinct aia_i.

FormalConjectures/ErdosProblems/253.leanErdos253.erdos_2535 linesExact file
¬∀ (a : ℕ → ℕ),    0 < a 0 →      Erdos253.RepresentsAPs a        Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 1) →          subsetSums (Set.range a) ∈ Filter.cofinite
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page