Erdős problem 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 for some prime . Alexeev and Mixon establish that 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.
Sources
FormalConjectures/ErdosProblems/
707.lean
It is false that any finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1 for some prime p.
As described in [arxiv/2510.19804], a counterexample is provided in [Ha47], see below. The proof of this has been formalized.
(∀ (A : Set ℕ), A.Finite → IsSidon A → ∃ B p, Nat.Prime p ∧ A ⊆ B ∧ IsPerfectDifferenceSet B (p ^ 2 + p + 1)) ↔ False