The Erdos-Sos Pairwise-Sums Problem

Let $f_3(N)$ be the least size forcing a set $A \subseteq \{1,\ldots,N\}$ to contain distinct $a,b,c$ with $a+b$ , $a+c$ and $b+c$ all in $A$ . The upper bound $f_3(N) \le 5N/8 + O(1)$ matches the standard construction $[N/8,N/4] \cup [N/2,N]$ , so $f_3(N) = 5N/8 + O(1)$ .

Result: Proved
Status: Resolved
AI contribution: AI co-developed
Method: Argument
Field: Additive combinatorics
Posed by: Paul Erdos, Vera T. Sos
Year posed: —
Years open: —
Solved: 2026-06-28
Model: GPT-5.5 Pro, Aristotle
Vendor: OpenAI / Harmonic
Collaborators: Ricky Cipollini
Verification: Lean-verified
Publication: Preprint
Significance: 15 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What the AI did

The paper states that the manuscript was written by GPT-5.5 Pro from a proof developed by the author together with GPT-5.5 Pro, and that the accompanying Lean formalization was carried out with Aristotle. Both the mathematics and the write-up are joint with the model rather than checked by it.

Verification

The paper reports a Lean formalization against Mathlib with no sorries and no added axioms. We have not compiled it. arXiv preprint, not peer-reviewed.

Source

arXiv:2606.29361 - A sharp 5/8 bound for an Erdos-Sos pairwise-sums problem

The Erdos-Sos Pairwise-Sums Problem

What the AI did

Verification

Source

Discussion