Erdős problem 697 · problems.science

For each $m$ and $\alpha$ , the density of the set of integers which are divisible by some $d \equiv 1 \pmod{m}$ with $1 < d < \exp (m ^ \alpha)$ exists.

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

697.lean

Retained formal statement1 of 4

For each $m$ and $\alpha$ , the density of the set of integers which are divisible by some $d \equiv 1 \pmod{m}$ with $1 < d < \exp (m ^ \alpha)$ exists.

FormalConjectures/ErdosProblems/697.leanErdos697.density_exists1 lineExact file

1∀ (m : ℕ) (α : ℝ), ∃ δ, {n | ∃ d, d ≡ 1 [MOD m] ∧ ↑d ∈ Set.Ioo 1 (Real.exp (↑m ^ α)) ∧ d ∣ n}.HasDensity δ

SolvedStatement only, no proof

Sources

Search problems.science