Source labels openChecked July 26, 2026

Erdős Problem 326

Let $A \subset \mathbb{N}$ be an additive basis of order 2.

Mathematical statement

Let $A \subset \mathbb{N}$ be an additive basis of order 2.

Must there exist $B = \{b_1 < b_2 < \dots\} \subseteq A$ which is also a basis such that $\lim_{k\to\infty} \frac{b_k}{k^2}$ does not exist?

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

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_326

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_326 : answer(sorry) ↔ ∀ (A : Set ℕ), A.IsAddBasisOfOrder 2 →    ∃ (b : ℕ → ℕ), StrictMono b ∧ ∀ n, b n ∈ A ∧ (Set.range b).IsAddBasis ∧      ∀ (x : ℝ), ¬ Tendsto (fun n ↦ (b n : ℝ) / n ^ 2) atTop (𝓝 x) := 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/326background