Proved. Spencer's Theorem 1 [Sp75] (J. Combin. Theory Ser. A 19 (1975), no. 3, 278--286; refereed) gives, for all $k$ and $c$, a $V$-set with no arithmetic progression of length $k+1$, which is the statement with $c=r$. Erdős announced the result in 1975 as "added in proof: Spencer has recently shown that such a sequence exists", without a reference; Spencer's paper is the published proof, from the Hales--Jewett theorem. The site's Lean suffix is a catalog label explained under Formalization: an external Lean proof, generated by Aristotle from the statement and posted to the site's thread by JoshuaB on 25 February 2026, exists in a later repository copy and was not built here. The claim page Spencer 1975 (accepted on the refereed publication and the curator's credit) records the result, its postings, the Aristotle-generated Lean proof behind the site's suffix and the acceptance evidence, and the frontmatter standing derives from it.