Erdős problem 1057 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1057.lean

Retained formal statement7 of 7

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

FormalConjectures/ErdosProblems/1057.leanErdos1057.erdos_1057.variants.upper_bound4 linesExact file

1∃ c > 0,2  ∀ᶠ (x : ℝ) in Filter.atTop,3    Erdos1057.carmichaelCounting x <4      x * Real.exp (-c * (Real.log x * Real.log (Real.log (Real.log x))) / Real.log (Real.log x))

SolvedStatement only, no proof

Sources

Search problems.science