Conjectures.io

Number theory

Erdős 887 - part ii

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}}).

References

  • [ErRo97] Erdős, Paul and Rosenfeld, Moshe, The factor-difference set of integers. Acta Arith. (1997), 353--359.

No one has attempted this yet.

Formal statement

Lean type

∃ K, ∀ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card ≤ K

What you must prove

import FormalConjectures.ErdosProblems.«887»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos887.erdos_887.parts.ii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/887.lean

Source type SHA-256
sha256:f6dad1724b63c7fb7f9ff163660e91619d28b9a144dd18f7857d668e36e685b9
Task id
fc-379fc029-parts-ii-e6ec37a5e5-formalized-v1
Task commitment
sha256:8f2f1af042da19b6b694dfc029463e717dffb409526462eb731bad56e6c108a3

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.