Erdős Problem #707: Sidon Sets and Perfect Difference Sets
Erdős problem #707 · erdosproblems.com/707
Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a \p^2+p+1p\{1,2,4,8\}$ is a counterexample - and discovered along the way that Marshall Hall, Jr. had published a different counterexample three decades before Erdős first posed the problem, unnoticed by the community for half a century.
- Result
- Disproved(see note)
- Status
- Resolved
- AI contribution
- AI-assisted
- Method
- Construction
- Field
- Combinatorial number theory
- Posed by
- Paul Erdős
- Year posed
- 1976
- Years open
- 49y
- Solved
- 2025-10-22
- Model
- ChatGPT (GPT-5)
- Vendor
- OpenAI
- Collaborators
- Boris Alexeev, Dustin G. Mixon
- Verification
- Lean-verified
- Publication
- Preprint
- Significance
- 20 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Hall's 1947 counterexample predates the problem itself; this paper's counterexample is independent, smaller, and Lean-certified.
What the AI did
The mathematics is the humans'; the paper is candid that LLMs failed at the two things they are usually praised for here - they never located Hall's paywalled prior solution, and "even after we knew what exactly to prove, it couldn't help us close the gap." What ChatGPT did do: write the complete Lean formalization of both counterexamples ("we decided to vibe code the whole proof... about a week... somehow it succeeded"). Earlier versions of the paper listed ChatGPT and Lean as authors until arXiv policy required their removal.
Verification
Both Hall's and the new counterexample are formalized and kernel-checked in Lean, with the formalization written by ChatGPT and audited by the authors; erdosproblems.com marks the problem disproved with the proof verified in Lean.