VibeMathedMath problems solved by AI
All problems

Erdős Problem #326

Erdős problem #326 · erdosproblems.com/326

Does there exist A={a1<a2<⋯ }⊂NA=\{a_1<a_2<\cdots\}\subset \mathbb{N} which is a minimal basis of order 22 (every large integer is the sum of 22 elements from AA, and no proper subset of AA has this property) such that lim⁡k→∞ak/k2=c\lim_{k\to \infty}a_k/k^2=c for some c≠0c\neq 0? A claimed construction gives a minimal basis with A(x)=Cx+O(1)A(x)=C\sqrt{x}+O(1), answering the question affirmatively; Erdős and Graham had conjectured a negative answer.

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-assisted
Method
Construction
Field
Number Theory, Additive Bases
Posed by
Paul Erdős, Ronald Graham
Year posed
1980
Years open
46y
Solved
2026-06-14
Model
GPT-5.5, Aristotle, Codex
Vendor
OpenAI, Harmonic
Collaborators
Aron Bhalla
Verification
Lean-verified
Publication
Announced
Significance
10 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Affirmative answer claimed, contrary to the negative answer Erdős and Graham conjectured; erdosproblems.com still lists the problem open

What the AI did

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.

Verification

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.

Sources

erdosproblems.com/326

Discussion