Erdős problem 142 · problems.science

Prove an asymptotic formula for $r_k(N)$ , the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$ -term arithmetic progression.

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

142.lean

Retained formal statement2 of 4

Show that $r_k(N) = o_k(N / \log N)$ , where $r_k(N)$ the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$ -term arithmetic progression.

FormalConjectures/ErdosProblems/142.leanErdos142.erdos_142.variants.lower1 lineExact file

1∀ (k : ℕ), 1 < k → (fun N => ↑(Erdos142.r k N)) =o[Filter.atTop] fun N => ↑N / Real.log ↑N

OpenStatement only, no proof

Sources

Search problems.science