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
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/817.leanTrue ↔ (fun n => 3 ^ n) =O[Filter.atTop] fun n => ↑(Erdos817.g 3 n)OpenStatement only, no proof