---

Claim. Kenta Kitamura's Lean development, announced on 11 September 2026 in the discussion thread of Problem 873, claims a proof that every increasing sequence $A$ has $\liminf_{X\to\infty}F(A,X,3)/X^{1/3}\le6$. So no sequence has $F(A,X,3)\gg X^{1/3}\log X$ for every large $X$, against the suggestion of Erdős in Some of my forgotten problems in number theory (p. 48), repeated in the erdosproblems.com commentary, that some sequence may meet the Erdős–Szemerédi bound $F(A,X,3)\ll X^{1/3}\log X$ for every $X$ and not only for infinitely many. The post names formal-conjectures pull request 5544 as the submission and the repository linked above, at the commit its web type-checker link names, as the development. formal-conjectures registers the development as the formal proof of its variant erdos_873.variants.supplement_all_scale, which states that no increasing sequence and constant $c>0$ have $F(A,X,3)\ge cX^{1/3}\log X$ for all large $X$.

Submission note. Posted to the erdosproblems.com forum by Kenta Kitamura on 11 September 2026:

I have submitted to Formal Conjectures a Lean-verified negative answer to the conjecture stated on this forum page: “There may be a sequence for which this holds for every $X$.” The submission is PR #5544.

The Lean formalization was prepared by Kenta Kitamura (KitaKen1).

GitHub: https://github.com/KitaKen1/erdos-873-lean Formal Conjectures PR: https://github.com/google-deepmind/formal-conjectures/pull/5544 Lean4Web: open the standalone proof

Verification: no 'sorry' or 'admit'; '#print axioms' reports only 'propext', 'Classical.choice', and 'Quot.sound'.

AI Usage Disclosure: This formalization was developed with assistance from ChatGPT and OpenAI Codex, using GPT-6 (Astra).

Why it is rejected. It answers a variant, not the Statement. Problem 873 asks whether, for every $\epsilon>0$, some $k$ gives $F(A,X,k)<X^\epsilon$. The development answers instead the question the erdosproblems.com commentary raises after the Erdős–Szemerédi bound, whether some sequence has $F(A,X,3)\gg X^{1/3}\log X$ for every large $X$, formal-conjectures' variant erdos_873.variants.supplement_all_scale. Its bound, $F(A,X,3)\le(6+o(1))X^{1/3}$ for arbitrarily large $X$, decides no exponent $\epsilon\le1/3$ that the Erdős–Szemerédi bound leaves open, so the development's mathematics answers the variant and does not settle this problem. The value disproved is its answer to that variant.

Standing. Rejected, as answering a variant. This corpus has neither read the repository nor built the development, so it gives a formalization link and no formalized evidence, and the axiom report above is the poster's own statement.

Depends on. No page of this wiki.