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

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

This is discussed in problem A13 of Guy's collection [Gu04].

FormalConjectures/ErdosProblems/1057.leanErdos1057.erdos_10571 lineExact file
True ↔ Filter.Tendsto (fun x => Real.log (Erdos1057.carmichaelCounting x) / Real.log x) Filter.atTop (nhds 1)
OpenStatement only, no proof