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 statement6 of 16

In 1950, Erdős [Er50c] proved the upper bound N(b)≪log⁡b/log⁡log⁡bN(b) \ll \log b / \log \log b. [Er50c] Erdős, P., Az 1/x1+1/x2+…+1/xn=A/B{1}/{x_1} + {1}/{x_2} + \ldots + {1}/{x_n} =A/B egyenlet egÉsz szÁmú megoldÁsairól. Mat. Lapok (1950), 192-210.

FormalConjectures/ErdosProblems/304.leanErdos304.erdos_304.variants.upper_19501 lineExact file
(fun b => ↑(Erdos304.smallestCollectionTo b)) =O[Filter.atTop] fun b => Real.log ↑b / Real.log (Real.log ↑b)
SolvedStatement only, no proof