Skip to content

Erdős problem 920

Start work

Is it true that, for k≥4k\geq 4, fk(n)≫n1−1k−1(log⁡n)ckf_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}} for some constant ck>0c_k>0?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

920.lean

Retained formal statement1 of 5

Is it true that, for k≥4k\geq 4, fk(n)≫n1−1k−1(log⁡n)ckf_k(n) \gg \frac{n^{1-\frac{1}{k-1}}}{(\log n)^{c_k}} for some constant ck>0c_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
True ↔  ∀ 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