---

Claim. For every $n\ge18$, every triangle-free graph on the vertex set $\{1,\ldots,n\}$ contains three pairwise nonadjacent vertices of the form $a$, $b$, $a+b$. This answers Problem 895 yes with the explicit threshold $18$: a triangle-free graph on $\{1,\ldots,n\}$ with $n\ge18$ induces a triangle-free graph on $\{1,\ldots,18\}$, and an independent triple there is independent in the whole graph, so the check at $n=18$ settles every larger $n$. The result is a finite computation: the site's page reports that Barber checked the statement with a SAT solver for every $n\ge18$ and communicated the result to the site's curator in a personal communication; the site does not say which $n$ were checked, and the reduction to the single case $n=18$ is the restriction argument above, which the Lean developments described below also make. No paper, preprint, code or certificate of Barber's is known (the problem page records the search scope); the site's page is the only posting, and its date is bounded by the earliest web-archive capture of the page (2025-04-06), which names this page. The site's "Additional thanks" line names Ben Barber. The threshold $18$ is the one the site reports; the site does not state whether it is sharp, that is, whether some triangle-free graph on $\{1,\ldots,17\}$ has no independent such triple.

The question of Hajnal that the site's commentary records, whether a triangle-free graph on $\{1,\ldots,n\}$ must have an independent set that is a Hindman set, $\{\sum_{i\in S}a_i : S \text{ a nonempty subset of } \{1,\ldots,k\}\}$ for some distinct $a_1,\ldots,a_k$, once $n$ is large in terms of $k$, is a separate, stronger question and remains open; this claim says nothing about it.

Postings. Boris Alexeev's lean-proofs repository holds a Lean 4 file, added 2026-08-17 and linked above at the revision the formal-conjectures catalog pins, whose header declares it a formalization of Barber's solution (Barber as informal author, the systems Codex and GPT-5.6 Sol as formal authors). It encodes the case $n=18$ as a propositional formula on the $153$ pairs of $\{1,\ldots,18\}$ ($816$ triangle clauses and $72$ clauses saying that each triple $a<b$, $a+b\le18$ contains an edge), reconstructs its unsatisfiability from an LRAT certificate through Mathlib's kernel-checked lrat_proof command, restricts a general graph to its first eighteen vertices, and proves erdos_895, the existence of a threshold $N$ (namely $18$) beyond which every triangle-free graph on Fin n has an independent Schur triple; its closing line prints the axioms of that theorem. The formal-conjectures catalog's statement file, whose own theorems are sorry, states the question with a SimpleGraph on Set.Icc 1 n, marks it solved with a formal_proof link to that file, records Barber's sharp form at $n\ge18$ as a solved variant, and records Hajnal's Hindman-set question as open.

Three further Lean verifications credit the result to Barber and were posted on 2026-09-16. The first, attached to an issue of the Justin Sun Prize awards repository (prepared with assistance from OpenAI Codex, as the issue says), translates a CaDiCaL LRAT certificate for the same $n=18$ formula into Lean proof terms without Mathlib, and also claims a Lean check of an explicit $42$-edge triangle-free graph on $\{1,\ldots,17\}$ with no independent triple $a$, $b$, $a+b$, which would make $18$ sharp. The second, in a repository linked from a pull request on that tracker (prepared with assistance from OpenAI Codex, as its README says), proves the result for Mathlib's SimpleGraph from an LRAT trace. The third, a supplementary package prepared with OpenAI Codex assistance, proves it again without Mathlib and says that it does not prove $18$ smallest. None of these files, and neither file above, is among the Lean the corpus has built and audited; the site's page marks the statement as formalised.

Depends on. No wiki page; the claim rests on the reported computation and the restriction argument stated above.

Acceptance. Reviewed: the site's curator, Thomas Bloom, marks the problem proved on erdosproblems.com and credits Barber's SAT verification for all $n\ge18$ with the resolution, and the formal-conjectures catalog marks its statement solved with the formalization linked; the curator's acceptance is the documented acceptance. No publication exists, so refereed is not listed; the Lean file is not among the Lean the corpus has built and audited, so formalized is not listed. The acceptance therefore rests on the curator's report of an unpublished computation and on Lean reconstructions by others outside the corpus's audited Lean; the problem's thread and proof-claim tab are empty.