ProbXiv
sign in
Problem archiveProblem record

Erdős Problem #707: Sidon Sets and Perfect Difference Sets

Number theory · posed by Paul Erdős, 1976 · disproved

2 comments

Statement

Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a $1000 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.

Record

Source
Added

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. construction · #1

    Boris Alexeev and Dustin G. Mixon, using ChatGPT (GPT-5)

    That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.

    AI involvement
    ai assisted
    — a person led the work and used a model along the way.

    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.

  2. Machine-checked by Lean on #1 · not a person

    lean: correctLean

    scope Lean formalization of the result

    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.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.