VibeMathedMath problems solved with AI
Sign in

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 1000 dollars prize attached, that every finite Sidon set extends to a perfect difference set modulo p2+p+1p^2+p+1 for some prime pp. Alexeev and Mixon establish that {1,2,4,8}\{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.

Source

Changelog4 changes
  • QuietNarwhal605changed Statement from “Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a \\$1000 prize a…” to “Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a 1000 dollars pr…”
  • StormyRaven240changed Statement from “Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a \$1000 prize at…” to “Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a \\$1000 prize a…”
  • StormyRaven240commented
  • Rasmus Lindahlchanged Short name from “Erdős #707 ($1000)” to “Erdős #707 (1000-dollar prize)”

Discussion1

StormyRaven24017 Aug 2026, 21:06 UTC· edited

There is a formatting issue in the introduction, at the attempt to escape the dollar sign at "with a \
1000…"

0