Erdős problem 139 · problems.science

Erdős Problem 139: Let $r_k(N)$ be the size of the largest subset of ${1,...,N}$ which does not contain a non-trivial $k$ -term arithmetic progression. Prove that $r_k(N) = o(N)$ .

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

139.lean

Retained formal statement1 of 1

Erdős Problem 139: Let $r_k(N)$ be the size of the largest subset of ${1,...,N}$ which does not contain a non-trivial $k$ -term arithmetic progression. Prove that $r_k(N) = o(N)$ .

FormalConjectures/ErdosProblems/139.leanErdos139.erdos_1391 lineExact file

1∀ (k : ℕ), 1 < k → Filter.Tendsto (fun N => ↑(Erdos139.r k N) / ↑N) Filter.atTop (nhds 0)

SolvedStatement only, no proof

Sources

Search problems.science