Skip to content

Erdős problem 1057

Start work

Is it true that C(x)=x1−o(1)C(x)=x^{1-o(1)}?

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1057.lean

Retained formal statement6 of 7

Pomerance [Po89] gave a heuristic suggesting that this is the true order of growth, and in fact C(x)=xexp⁡(−(1+o(1))log⁡xlog⁡log⁡log⁡xlog⁡log⁡x)C(x)= x \exp\left(-(1+o(1))\frac{\log x\log\log\log x}{\log\log x}\right).

FormalConjectures/ErdosProblems/1057.leanErdos1057.erdos_1057.variants.pomerance6 linesExact file
True ↔  Filter.Tendsto    (fun x =>      -(Real.log (Erdos1057.carmichaelCounting x / x) * Real.log (Real.log x)) /        (Real.log x * Real.log (Real.log (Real.log x))))    Filter.atTop (nhds 1)
OpenStatement only, no proof