Erdős problem 920

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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

920.lean

Retained formal statement5 of 5

Graver and Yackel [GrYa68] proved that $f_k(n) \ll \left(n\frac{\log\log n}{\log n}\right)^{1-\frac{1}{k-1}}.$

FormalConjectures/ErdosProblems/920.leanErdos920.erdos_920.variants.upper_bound3 linesExact file

1∀ k ≥ 3,2  (fun n => ↑(Erdos920.f k n)) =O[Filter.atTop] fun n =>3    (↑n * Real.log (Real.log ↑n) / Real.log ↑n) ^ (1 - 1 / (↑k - 1))

SolvedStatement only, no proof