Erdős problem 142

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

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

142.lean

Retained formal statement1 of 4

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.

FormalConjectures/ErdosProblems/142.leanErdos142.erdos_1421 lineExact file

1∀ (k : ℕ), (fun N => ↑(Erdos142.r k N)) =Θ[Filter.atTop] sorry

OpenStatement only, no proof

Source providers

Erdős Problems1
locator only
Formal Conjectures4
statement retained
VibeMathed0
not observed here
PLBY Lean proofs0
not observed here
Jayyhk Erdős Lean0
not observed here
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki0
not observed here
GPT-Erdős1
no statement retained

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 142.lean4