A sharp 5/8 bound for an Erdős-Sós pairwise-sums problem

Ricky Cipollini

paper

A sharp 5/8 bound for an Erdős-Sós pairwise-sums problem

arXiv:2606.29361

Abstract

Let $f_{3} (N)$ be the least integer such that every set $A \subseteq {1, \dots, N}$ of size at least $f_{3} (N)$ contains distinct elements $a, b, c \in A$ such that $a + b \in A$ , $a + c \in A$ , and $b + c \in A$ . We prove that $f_{3} (N) \leq 5 N /8 + O (1)$ . Together with the standard construction $[N /8, N /4] \cup [N /2, N]$ , this gives $f_{3} (N) = 5 N /8 + O (1)$ , resolving Erdős Problem 865. The proof is self-contained. An earlier conditional version of the reduction has also been formalized in Lean 4/Mathlib with no sorries and no added axioms.