PROVED (LEAN). The status-defining source is Theorem 1.1 of a seven-page arXiv preprint, R. Cipollini, A sharp 5/8 bound for an Erdős--Sós pairwise-sums problem, arXiv:2606.29361v1 (28 June 2026): there is a constant $C>0$ such that for all $N$, not only large $N$, every $A\subseteq[1,N]$ with $|A|\ge\tfrac58N+C$ contains a pairwise-sum triple, with the explicit form $|A|\le\tfrac54H+6$ for every triple-free $A\subseteq[1,2H]$. The manuscript's first page declares that it was written by an AI model, GPT-5.5 Pro, from a proof developed by the author together with that model, and that the Lean formalization was carried out with the prover Aristotle; the site's commentary credits the solution to Cipollini and GPT Pro, and the site accepted it on 2 July 2026 with the label PROVED (LEAN); Stijn Cambie, a contributor the paper's acknowledgments thank for feedback and improvements, reported in the site's thread on 27 June 2026 that he had read a version of the paper in detail and confirmed it. This is a source-supported solution accepted by the site, distinct from a claim of journal refereeing: no refereed publication, no later arXiv version, no citing paper and no written expert review beyond the thread were found. Two external Lean developments prove the theorem for their own definitions; the corpus holds no build of either, so they give no formalized evidence. The refereed content behind the label is the density bound $f_k(N)\le(\tfrac23-\epsilon_k)N$ of Choi, Erdős and Szemerédi (1975), and the folklore $k=2$ fact the site states. The standing is derived from the claim page (Cipollini, 2026), accepted on the site's documented review with these qualifications.