Source labels openChecked July 26, 2026

Erdős Problem 489

Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap [1,x]\rvert=o(x^{1/2})$ . Let $B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in A\}$ . If $B=\{b_1 < b_2 < \cdots\}$ then is it true that $$\lim_{x \to \infty} \frac{1}{x}\sum_{b_i < x}(b_{i+1}-b_i)^2$...

Number theory AMS 11

Mathematical statement

Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap [1,x]\rvert=o(x^{1/2})$ . Let $B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in A\}$ . If $B=\{b_1 < b_2 < \cdots\}$ then is it true that $\lim_{x \to \infty} \frac{1}{x}\sum_{b_i < x}(b_{i+1}-b_i)^2$ exists (and is finite)?

For example, when $A=\{p^2: p\textrm{ prime}\}$ then $B$ is the set of squarefree numbers, and the existence of this limit was proved by Erdős.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_489

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_489 : answer(sorry) ↔    ∀ (A : Set ℕ),      (fun x : ℕ => (((Finset.Icc 1 x).filter (· ∈ A)).card : ℝ)) =o[atTop]        (fun x : ℕ => (x : ℝ).sqrt) →      (sievedSet A).Infinite →      ∃ L : ℝ, Tendsto (fun x : ℕ => GapSumSq A x / (x : ℝ)) atTop (𝓝 L) := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization erdosproblems.com/489background