Problem detail · source-aware
VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Does there exist $A=\{a_1<a_2<\cdots\}\subset \mathbb{N}$ which is a minimal basis of order $2$ (every large integer is the sum of $2$ elements from $A$, and no proper subset of $A$ has this property) such that $\lim_{k\to \infty}a_k/k^2=c$ for some $c\neq 0$? A claimed construction gives a minimal basis with $A(x)=C\sqrt{x}+O(1)$, answering the question affirmatively; Erdős and Graham had conjectured a negative answer.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
Per the author's disclosure, most of the mathematics is his own, with GPT-5.5 used to stress-test ideas, suggest revisions, identify gaps and write up some proofs; the solution was then formalized over several weeks with Aristotle, Codex and GPT-5.5 into a roughly 15,000-line Lean proof confirming all claims in the manuscript.
Provider: OpenAI, Harmonic · Prompt public: unknown · Independence: unknown
The author reports a ~15,000-line Lean formalization, type-checkable online, confirming all claims of the manuscript. It has not been independently audited for statement fidelity, and erdosproblems.com has not accepted the claim: the site's owner found the AI-written exposition hard to digest while stressing that this was not a correctness objection.
Correctness: supported · statement fidelity: audited · peer review: none
Affirmative answer claimed, contrary to the negative answer Erdős and Graham conjectured; erdosproblems.com still lists the problem open
Source-reported tools: construction.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.