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 statement7 of 7

Erdős [Er56c] proved C(x)<xexp⁡(−clog⁡xlog⁡log⁡log⁡xlog⁡log⁡x)C(x) < x \exp\left(-c \frac{\log x\log\log\log x}{\log\log x}\right) for some constant c>0c>0.

FormalConjectures/ErdosProblems/1057.leanErdos1057.erdos_1057.variants.upper_bound4 linesExact file
∃ c > 0,  ∀ᶠ (x : ℝ) in Filter.atTop,    Erdos1057.carmichaelCounting x <      x * Real.exp (-c * (Real.log x * Real.log (Real.log (Real.log x))) / Real.log (Real.log x))
SolvedStatement only, no proof