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

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)\le 5N\mathrm{/}8+O(1)$. Together with the standard construction $[N\mathrm{/}8,N\mathrm{/}4]\cup [N\mathrm{/}2,N]$, this gives $f_3(N)=5N\mathrm{/}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.