DISPROVED (LEAN), the site's label. Three constructions, each on its own claim page, give a Sidon set meeting every infinite arithmetic progression: the successive selection the site writes out and credits to Baumgartner (claim page (Baumgartner, 1975)), the factorial set that Google DeepMind's AlphaProof found (claim page (DeepMind, 2025)), formalized in Lean in November 2025 and linked by the catalog, and Dutta's power sequences (claim page (Dutta, 2025)). The factorial and power-sequence claims are accepted on the site's curator's documented credit, and the successive selection stays claimed, since the curator wrote it out himself; the natural-language proofs on the linked library pages are author-recorded, and the Lean files behind the label's Lean mark, linked on Google DeepMind's claim page, were not built by this corpus. The site's answer changed between November 2024 and mid-May 2025 while its label stayed SOLVED: it had answered yes, crediting Baumgartner [Ba75], and it switched to no, wrote out the successive selection as implicit in [Ba75] and credited the factorial construction to AlphaProof after Google DeepMind reported the counterexample to the curator, as the Baumgartner and Google DeepMind claim pages record with their evidence. Web archive captures first show the label DISPROVED on 2025-09-17 and DISPROVED (LEAN) on 2025-12-06.