Skip to content

Erdős problem 887

Is there an absolute constant KK such that, for every C>0C > 0, if nn is sufficiently large then nn has at most KK divisors in (n12,n12+Cn14)(n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}}).

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

887.lean

Retained formal statement1 of 4

Is there an absolute constant KK such that, for every C>0C > 0, if nn is sufficiently large then nn has at most KK divisors in (n12,n12+Cn14)(n^{\frac{1}{2}}, n^{\frac{1}{2}} + C n^{\frac{1}{4}}).

FormalConjectures/ErdosProblems/887.leanErdos887.erdos_887.parts.i1 lineExact file
C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, {dFinset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | dn}.cardsorry
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page