← All papers
A sharp 5/8 bound for an Erdős-Sós pairwise-sums problem
math.CO
Jun 28, 2026 · v1
math.NT
TL;DR
Formalizes a key reduction for the Erdős-Sós pairwise-sums problem in Lean 4 with Mathlib, no sorries or added axioms.
Abstract
Let $f_3(N)$ be the least integer such that every set $A\subseteq\{1,\ldots,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)\le 5N/8+O(1)$. Together with the standard construction $[N/8,N/4]\cup[N/2,N]$, this gives $f_3(N)=5N/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.
Problem
Erdős Problem 865 asks for the least integer f_3(N) such that every subset A of {1,...,N} of that size contains distinct a, b, c with a+b, a+c, b+c all in A. The sharp value was previously unknown.
Approach
The proof is self-contained and combinatorial. It reduces the problem to bounding a quantity |B| - |C(B)| for certain sets B in a cyclic group, then applies an inclusion-exclusion argument on four derived sets. An earlier conditional version of the reduction was formalized in Lean 4 with Mathlib.
Results
The paper proves f_3(N) = 5N/8 + O(1), matching the known lower bound from the construction [N/8, N/4] ∪ [N/2, N] and resolving Erdős Problem 865. The Lean formalization compiles with no sorries and no added axioms.