Does there exist $A = {a_{1} < a_{2} < \dots} \subset N$ which is a minimal basis of order $2$ (i.e. every large integer is the sum of $2$ elements from $A$ , and no proper subset of $A$ has this property), such that $k \to \infty lim \frac{a _{k}}{k ^{2}} = c$ for some $c \neq = 0$ ?

Open — best to date is a honest null, not yet sealed.

number theory · open · formalized (Lean) · 1 attempt

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

honest null

needs verification

attempted via frontier 'sidon/B2' (transfer_strength=none) -> no_progress

No solve/partial on this pass. Transfer into the owned frontier was 'none'. Do not re-attack cold; needs a new idea or richer accumulated context.

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

* Erdős originally asked the stronger version with **$B=A$**, i.e. whether an additive basis (A={a_k}) of order $2$ must satisfy that (\lim_{k\to\infty} a_k/k^2) **fails to exist**. That stronger statement is **false**: Cassels constructed a basis (C={c_n}) of order $2$ with [ c_n=\lambda n^2+O(n), ] so in particular (…

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 11 · open (literature)

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)

formal-conjectures/326.lean ↗

status

open

evidence

formal

status

Search Vela