We resolve a $1000 Erdős problem, with a Lean proof vibe coded using ChatGPT (borisalexeev.com)

A long-standing Erdős prize problem — whether every finite Sidon set can be extended to a finite perfect difference set — has been resolved: the five-element set {1, 2, 4, 8, 13} is a concrete counterexample. The authors show this Sidon set (one with distinct pairwise sums) cannot be enlarged to a finite perfect difference set, settling a question Erdős repeatedly raised over decades. In preparing the work the team also uncovered an earlier counterexample published by Marshall Hall Jr. before Erdős posed the conjecture; to remove any doubt they produced machine-checkable Lean proofs for both Hall’s example and their own, with the formalization generated via a human-assisted ChatGPT “vibe coding” workflow and verified in Lean. This result matters on two fronts: combinatorial number theory gains a definitive negative answer to a half-century question (and a simple explicit counterexample), while the AI/formal-methods angle demonstrates practical LLM-assisted theorem-proving. The authors provide the formal Lean code as ancillary material, illustrating a reproducible pipeline where an LLM helps generate proof scripts that humans review and a proof assistant checks. That workflow highlights both the promise and the care required when using LLMs for formal verification — accelerating formalization while still needing human oversight for correctness and literature context.