Erdős problem 450 · problems.science

How large must $y(\varepsilon, n)$ be so that every interval $(x, x+y)$ contains at most $\varepsilon y$ integers having a divisor in $(n, 2n)$ ? The candidate proof gives the sharp fixed- $\varepsilon$ order $y = \Theta_\varepsilon(n)$ , uniformly in the translate.

Sources

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

450.lean

Retained formal statement2 of 2

A translate-uniform linear scale suffices: there is a sufficient window length Y with Y ε n ≤ C(ε) · n. This is an upper bound on the optimal scale, not the exact threshold asked for in erdos_450.

FormalConjectures/ErdosProblems/450.leanErdos450.erdos_450.linear_scale_suffices1 lineExact file

1∃ Y, (∀ (ε : ℝ), 0 < ε → ∃ C, ∀ (n : ℕ), ↑(Y ε n) ≤ C * ↑n) ∧ Erdos450.IsSufficientScale Y

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science