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
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
True ↔ (fun n => 3 ^ n) =O[Filter.atTop] fun n => ↑(Erdos817.g 3 n)OpenStatement only, no proof