Skip to content

Erdős problem 304

Start work

Is it true that N(b)≪log⁡log⁡bN(b) \ll \log \log b?

Sources

The source's own material, retained exactly.

16 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

304.lean

Retained formal statement14 of 16

Is it true that N(b)≪log⁡log⁡bN(b) \ll \log \log b?

FormalConjectures/ErdosProblems/304.leanErdos304.upper_bound1 lineExact file
True ↔ (fun b => ↑(Erdos304.smallestCollectionTo b)) =O[Filter.atTop] fun b => Real.log (Real.log ↑b)
OpenStatement only, no proof