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 statement1 of 5

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$ ?

This problem follows immediately from Mattheus and Verstraete's lower bound [MaVe23] for k = 4 and Bradač's lower bound [Br26] for k ≥ 5.

FormalConjectures/ErdosProblems/920.leanErdos920.erdos_9202 linesExact file

1True ↔2  ∀ k ≥ 4, ∃ c > 0, (fun n => ↑n ^ (1 - 1 / (↑k - 1)) / Real.log ↑n ^ c) =O[Filter.atTop] fun n => ↑(Erdos920.f k n)

SolvedStatement only, no proof