The board / additive combinatorics / #895
Erdős Problem #895
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Is it true that, for all sufficiently large \(n\), if \(G\) is a triangle-free graph on \(\{1,\ldots,n\}\) then there must exist three independent points \(a,b,a+b\)? A problem of Erdős and Hajnal [Er95d]. The stated problem has been resolved by Barber (personal communication) who verified using a SAT solver that this is true for all \(n\geq 18\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/895.Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.