Erdős problem 817
Let . Define to be the minimal such that contains some of size such that contains no non-trivial -term arithmetic progression. Estimate . In particular, is it true that
Sources
FormalConjectures/ErdosProblems/
817.lean
Retained formal statement
A problem of Erdős and Sárközy who proved
∃ O > 0, (fun n => 3 ^ n / ↑n ^ O) =O[Filter.atTop] fun n => ↑(Erdos817.g 3 n)SolvedStatement only, no proof