Skip to content

Erdős problem 142

Start work

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

142.lean

Retained formal statement2 of 4

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

FormalConjectures/ErdosProblems/142.leanErdos142.erdos_142.variants.lower1 lineExact file
∀ (k : ℕ), 1 < k → (fun N => ↑(Erdos142.r k N)) =o[Filter.atTop] fun N => ↑N / Real.log ↑N
OpenStatement only, no proof