Erdős problem 323

Is it true that $f_{k,k}(x) \gg_\epsilon x^{1-\epsilon}$ for all $\epsilon>0$ ?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

323.lean

Retained formal statement3 of 4

The case $k=2$ was resolved by Landau, who showed $f_{2,2}(x) \sim \frac{cx}{\sqrt{\log x}}$ for some constant $c>0$ .

FormalConjectures/ErdosProblems/323.leanErdos323.erdos_323.variants.k_eq_21 lineExact file

1∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun x => ↑(Erdos323.f 2 2 x)) fun x => c * ↑x / √(Real.log ↑x)

SolvedStatement only, no proof