Open. The site's label is OPEN. Three pending partial claims answer the question yes for a range of exponents: the bound $F(A,X,3)\ll X^{1/3}\log X$ that Erdős reports with Szemerédi in 1992 (claim page (Erdős and Szemerédi, 1992)), Ritvik Nayak's note of April 2026 with exponents below $1/3$ for $k=6$ and $k=11$ (claim page (Nayak, 2026)), and two notes posted by old-bielefelder in April and August 2026, written by ChatGPT 5.5 Thinking and ChatGPT 5.6 Sol, covering every exponent above $1/4$ (claim page (Old Bielefelder, 2026)). No claim covers exponents at most $1/4$, and the standing in the frontmatter is derived from the claim pages.

Kenta Kitamura's Lean development (thread post of 11 September 2026; developed with ChatGPT and OpenAI Codex using GPT-6 (Astra), as the post discloses) proves that every increasing sequence has $\liminf_{X\to\infty}F(A,X,3)/X^{1/3}\le6$. This refutes Erdős's suggestion in [Er92c], p. 48, repeated in the site's commentary, that some sequence satisfies $F(A,X,3)\gg X^{1/3}\log X$ for every $X$. Formal-conjectures registers the development as the formal proof of its variant erdos_873.variants.supplement_all_scale. It settles no instance of the question asked, so it has no claim page; it was not built or audited here.