Erdős problem 920 · problems.science

Is it true that, for $k\geq 4$ , $f_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}}$ for some constant $c_k>0$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

920.lean

Retained formal statement3 of 5

The lower bound $R(4,m) \gg m^3/(\log m)^4$ of Mattheus and Verstraete [MaVe23] (see [erdosproblems.com/166]) implies $f_4(n) \gg \frac{n^{2/3}}{(\log n)^{4/3}}$ .

FormalConjectures/ErdosProblems/920.leanErdos920.erdos_920.variants.lower_bound_k_eq_41 lineExact file

1(fun n => ↑n ^ (2 / 3) / Real.log ↑n ^ (4 / 3)) =O[Filter.atTop] fun n => ↑(Erdos920.f 4 n)

SolvedStatement only, no proof

Sources

Search problems.science