VibeMathedMath problems solved with AI
Sign in

Erdős Problem #126: prime divisors of pairwise sums

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

Let f(n)f(n) be maximal such that for every nn-element set A⊆NA\subseteq\mathbb N,∏a,b∈Aa≠b(a+b) \prod_{\substack{a,b\in A\\a\ne b}}(a+b) has at least f(n)f(n) distinct prime factors. Erdős asked whetherf(n)log⁡n→∞. \frac{f(n)}{\log n}\to\infty. The answer is yes.

Result
Proved(see note)
Status
Resolved
AI contribution
AI-discovered
Method
Argument
Field
Elementary number theory
Posed by
Paul Erdős
Year posed
1934
Years open
92y
Solved
2026-08-28
Model
GPT-6 Astra (pre-release)
Vendor
OpenAI
Collaborators
Tom Adamczewski
Verification
Lean-verified
Publication
Announced
Significance
35 / 100
Disclosed cost
$247
Wikipedia
No dedicated article

What was actually shown

Forf(n)=min⁡∣A∣=n∣{p prime:p∣a+b for some distinct a,b∈A}∣, f(n)=\min_{|A|=n}\left|\left\{p\text{ prime}:p\mid a+b\text{ for some distinct }a,b\in A\right\}\right|, Astra formally provesf(n)log⁡n→∞. \frac{f(n)}{\log n}\to\infty.
The repository contains substantially stronger proofs. In particular, one verified alternate resolution establishesn≤3r2, n\le 3r^2, where rr is the number of supporting primes, yieldingf(n)≫n1/2. f(n)\gg n^{1/2}. Other independent resolutions give exponents 1/31/3, 1/51/5, and 1/81/8. Thus the formal work goes well beyond the qualitative conjecture, although only the limit statement is the registered benchmark theorem.

What the AI did

GPT-6 Astra autonomously solved the Formal Conjectures benchmark statement and wrote the Lean proofs, with no human seeing or steering the proof search. Remarkably, four independent successful runs produced polynomial lower bounds by apparently three distinct elementary arguments. The primary proof gives f(n)≫n1/8f(n)\gg n^{1/8}; alternate proofs give f(n)≫n1/3f(n)\gg n^{1/3}, f(n)≫n1/2f(n)\gg n^{1/2}, and f(n)≫n1/5f(n)\gg n^{1/5}. Only the weaker limit f(n)/log⁡n→∞f(n)/\log n\to\infty is advertised and Comparator-checked as the benchmark theorem.

Verification

Lean-verified. Checked here on 6 September 2026 from a clone of tadamcz/erdos126 at abd4239: 7,866 lines of Lean, zero sorry outside the statement stubs, zero axiom declarations, no native_decide, unsafe or implemented_by; Comparator configuration present and CI runs it with only propext, Quot.sound and Classical.choice. The statement is copied verbatim from Formal Conjectures' ErdosProblems/126.lean at commit 488aade2. Only the qualitative limit f(n)/log n -> infinity is the compared theorem; the polynomial bounds (exponents 1/8, 1/3, 1/2, 1/5 across four runs) are stronger internal results, and erdosproblems.com's page records the n^(1/2) one. erdosproblems.com, the field's own record, marks the problem PROVED (LEAN) with a proof exposition by Thomas Bloom, which is why this is Resolved rather than Candidate: the canonical tracker has accepted it.

Sources

Submitted by VibeGene on

Changelog2 changes

Discussion