Skip to content

Erdős problem 489

If AA is a forbidden-divisor set with ∣A∩[1,x]∣=o(x)|A \cap [1,x]| = o(\sqrt{x}) and B={b1<b2<⋯ }B = \{b_1 < b_2 < \cdots\} the sifted set, must x−1∑bi<x(bi+1−bi)2x^{-1} \sum_{b_i < x} (b_{i+1} - b_i)^2 converge to a finite limit?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/489.lean

Formal Conjectures

FormalConjectures/ErdosProblems/489.leanErdos489.erdos_4894 linesExact file
True ↔  ∀ (A : Set ℕ),    ((fun x => ↑{x ∈ Finset.Icc 1 x | x ∈ A}.card) =o[Filter.atTop] fun x => √↑x) →      (Erdos489.sievedSet A).Infinite → ∃ L, Filter.Tendsto (fun x => Erdos489.GapSumSq A x / ↑x) Filter.atTop (nhds L)
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.

Proof manifests naming this Problem

  • William Blair Lean proofswilliamjblair:Erdos489.erdos489_statement

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