Erdős Problem #198 — Sidon Sets and Disjoint Infinite Arithmetic Progressions

The problem asks whether every infinite Sidon set has a complement containing an infinite arithmetic progression. The negative answer is attributed to Baumgartner, reportedly through Erdős and Graham.

Known results

• Baumgartner, 1975: enumerate all infinite arithmetic progressions, choose one rapidly increasing element from each, and the resulting lacunary set is Sidon while meeting every progression.

Explicit factorial construction and formalization

The set $A=\{(n+1)!+n:n\geq 0\}$ is reported to be Sidon and to meet every arithmetic progression, hence its complement contains none. AlphaProof is credited with finding this construction; Alexeev formalized it in Lean using Aristotle, with Claude assisting only with Lean translation. The formalization is public, but no peer-reviewed or arXiv proof was found.

Current status (as of June 2026): The conjecture has an explicit counterexample, supported by a public Lean formalization; the historical attribution and recent AI-associated account lack a peer-reviewed or arXiv publication.