Skip to content

Erdős problem 450

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/450.lean

Formal Conjectures

FormalConjectures/ErdosProblems/450.leanErdos450.erdos_4502 linesExact file
True ↔  ∃ Y, Erdos450.IsSufficientScale Y ∧ ∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun n => ↑(Y ε n) / ↑n) Filter.atTop (nhds 0)
OpenStatement only, no proof

Proof manifests naming this Problem

  • William Blair Lean proofswilliamjblair:Erdos450.turanLinearAnswer_isSufficientScale

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • argument

    VibeMathed

    Machine
    GPT-5.6 starships (Claude Fable 5 reviewer)
    Reported outcome
    candidate
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page