---

Claim. $A=\{(n+1)!+n : n\ge 0\}$ is a Sidon set meeting every infinite arithmetic progression in $\mathbb{N}$, so its complement contains no infinite arithmetic progression and the answer is no.

Each term exceeds twice the one before, which makes two-term sums distinct, so $A$ is Sidon; and for $a\ge 0$ and $d\ge 1$ the term with $n=a+d$ lies in the progression $\{a+td : t\ge 0\}$, since it equals $a+d+(a+d+1)!$ and $d$ divides $(a+d+1)!$. The library's construction page writes the proof out.

Postings. The claimant is Google DeepMind, whose system AlphaProof found the construction. The site's page credits it to AlphaProof and writes it out; the construction is absent from a web archive capture of the page of 2024-11-07 and present in one of 2025-05-30. Its first dated records are in the formal-conjectures catalog, Google DeepMind's project: an issue of 2025-05-13 asks to update the catalog's Problem 198 with the information added to the site after contact with the curator, and a pull request opened on 2025-05-15 and merged on 2025-05-27, linked above with the catalog file at the merge, names the counterexample that AlphaProof found, reports that the site's answer changed from yes to no after Google DeepMind reported it to the curator, and adds the constructions $\{n!+n : n\ge 0\}$ and $\{(n+1)!+n : n\ge 0\}$ to the catalog; the page is named by the pull request's date, the first record naming AlphaProof. On 2025-11-24 Alexeev posted in the site's discussion thread a Lean formalization of this construction, produced from a ChatGPT exposition by Aristotle with the catalog's statement erdos_198 as target, in Alexeev's lean-proofs repository, linked above; its header names Baumgartner as the original human prover, citing his unrelated 1975 paper on canonical partition relations, and notes that the proof used is AlphaProof's. The catalog's 198.lean marks erdos_198 solved with two formal_proof links, one to that file, which it describes as Alexeev's Lean formalization made with Aristotle, and one into the GitHub user XC0R's fork of formal-conjectures at a pinned commit that GitHub does not serve. The catalog's pull request of 2026-04-13 that added that link carried the proof in its first commit, which GitHub serves and which is linked above: it proves erdos_198 without sorry from the set $\{(n+1)!+n\}$, which the pull request names as AlphaProof's construction, and the pull request says Claude assisted the Lean translation. The catalog separately records the variant $\{n!+n : n\ge 0\}$, which it says AlphaProof found and proved, with a formal_proof link into a fork whose file at the pinned commit, linked above, proves that variant in full: the set is Sidon and meets every infinite arithmetic progression. The library's source record separates the text of Alexeev's file from the builds its postings report; this corpus has built none of these Lean files, so they give no formalized evidence.

Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem disproved, credits the construction to AlphaProof, thanks its team and writes the construction out on the problem page, a documented acceptance outside this project and independent of the claimant. The formal-conjectures catalog marks its statement solved with the formalizations linked, but it is Google DeepMind's own project, so its mark is not independent acceptance. No refereed publication exists, so refereed is not listed; the Lean files were not built or audited by this corpus, so formalized is not listed although the site's label reads DISPROVED (LEAN).

Depends on. No wiki page; the claim rests on the construction stated above.