Proved, the site's label, which records the answer as yes; the explicit threshold is $n\ge18$. The accepted claim is Barber's verification with a SAT solver, which the site reports as a personal communication, that the statement holds for every $n\ge18$; a check at $n=18$ suffices by restricting a graph to its first eighteen vertices, as the claim page explains. It is recorded on its claim page (Barber, 2025) with the curator's acceptance as its only evidence; no paper or certificate of Barber's is known (see the search scope below). Hajnal's stronger question, whether a large triangle-free graph must have an independent Hindman set, which the site's commentary records, remains open and is separate from the stated problem.