Alexeev–Mixon (2025) — a finite Sidon set that cannot be extended to a finite perfect difference set (Erdős #707 disproved)

Statement

Erdős Problem #707 (posed from 1976 onward across a dozen-plus papers and surveys; \$1000 prize, per Erdős's 1980 "A survey of problems in combinatorial number theory," *Ann. New York Acad. Sci.*). Let $A$ be a finite Sidon set (all pairwise differences of distinct elements are distinct — see Sidon sets / B_2 sets / Golomb rulers). Is there always a perfect difference set $B\supseteq A$ — i.e. a set $B$ in some cyclic group $\mathbb Z_v$ such that every nonzero element of $\mathbb Z_v$ is represented as a difference of two elements of $B$ exactly once — with $v=q^2+q+1$ for some prime power $q$ (the necessary form for a perfect difference set to exist, by Singer's construction, Sidon sets / B_2 sets / Golomb rulers)?

Erdős conjectured yes: every finite Sidon set extends to a finite perfect difference set.

Facts

- Source: Alexeev, Boris; Mixon, Dustin G., "Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof," arXiv:2510.19804 (Oct 2025); published *Proc. Natl. Acad. Sci. U.S.A.* 123(21), e2531760123 (2026), DOI 10.1073/pnas.2531760123. - Answer: no. The Sidon set $\{1,2,4,8,13\}$ (labeled "Theorem Q" in the paper) does not extend to a finite perfect difference set modulo any $v>0$ — the conjecture is false, disproved by an explicit finite counterexample. - Small cases were already known to go the "yes" way, which is part of why the conjecture stood for ~50 years: Sawin (MathOverflow) showed every Sidon set of size $\le3$ extends; the case of size $4$ was open with only a *candidate* counterexample ($\{0,1,3,11\}$, due to Mueller) floated but not confirmed. $\{1,2,4,8,13\}$ has size $5$. - A second, older counterexample was found during the writing of this paper. Marshall Hall, Jr. had published a *different* counterexample (a size-5 set, equivalent after translation to $\{1,3,9,10,13\}$) roughly three decades *before* Erdős ever posed the problem — in a 1930s/40s paper on cyclic projective planes, apparently unnoticed by the entire subsequent literature on Erdős's conjecture until Alexeev–Mixon rediscovered it while researching the problem's history. - The proof is a "human-assisted" formal proof: the mathematical argument (projective-plane polarity theory) was worked out and described in natural language by the human authors, then translated into over 6000 lines of Lean 4 proof code by ChatGPT (an LLM), with the Lean kernel providing the actual correctness guarantee — explicitly marketed by the authors as a demonstration that LLM-generated *formal* proofs can be trusted regardless of the code's readability, because the proof checker (not the LLM) is the source of truth. Both the new counterexample and the rediscovered Hall counterexample were independently formally verified this way. - Prior partial machinery this result sits inside: perfect difference sets of order $q+1$ in $\mathbb Z_{q^2+q+1}$ come from Singer's 1938 cyclic-collineation construction on the projective plane $PG(2,q)$ (Sidon sets / B_2 sets / Golomb rulers); this is exactly the class of finite objects the conjecture asked every Sidon set to embed into.

Solution

The transferable technique — turn an extension question into a geometric rigidity question via polarities, then let a forced small "if X is present, Y must collide" chain do the actual disproving; use an LLM only to convert an already-complete human argument into a machine-checked one, not to search for the argument itself.

1. Reinterpret "extend to a perfect difference set" as a projective-plane polarity condition. A perfect difference set $B\subseteq\mathbb Z_v$ ($v=q^2+q+1$) is exactly the point-set on one line of $PG(2,q)$ under a Singer cyclic collineation. Hall's classical theory of polarities of a projective plane gives a correspondence between points and lines; a point $x$ is called absolute with respect to a polarity $\pi$ exactly when $2x\in B$ (for the specific polarity induced by the plane's structure here). This reframes "does $A$ sit inside some perfect difference set $B$" as a question about which points a hypothetical polarity would be forced to mark absolute, purely as a function of $A$'s own elements. 2. Exploit classical structural theorems constraining absolute points. Baer's propositions on projective planes constrain *how many* absolute points a polarity can have and *how they can be distributed across lines*, with genuinely different (and both usable) constraints depending on whether the plane's order $q$ is odd (Proposition 21: too many absolute points cannot concentrate on one line) or even (Proposition 23: absolute points cannot fail to lie on a single line). This gives two independent rigidity levers, one per parity of $q$ — a case split baked directly into 80-year-old finite-geometry theorems, not invented ad hoc for this problem. 3. Force a concrete difference collision from the candidate set's own elements. For $A=\{1,2,4,8,13\}$, membership of $8$ in $B$ forces (via the absoluteness rule) that $2\cdot8=16\in B$ must also hold. But then the two differences $16-13$ and $4-1$ are both equal to $3$ — a repeated difference, directly contradicting the defining "exactly once" property of a perfect difference set. Combined with the Baer-proposition parity case split (needed to rule out the remaining odd/even-order escape routes for $q$), this pins down that no $v=q^2+q+1$ admits a $B\supseteq A$. 4. Only after the full informal argument is complete, hand it to an LLM for formalization, not discovery. The mathematical content (the polarity reduction, the Baer-proposition case split, the $16-13=4-1$ collision) was worked out by the human authors first; ChatGPT's role was purely to translate an already-finished proof sketch into >6000 lines of Lean 4 syntax. The paper's stated point is that this division of labor is safe because Lean's kernel — not the LLM — is what certifies correctness: a human need not read or trust the generated code's *style*, only trust that it type-checks, which is independently and mechanically verifiable. This is the reusable meta-lesson, orthogonal to the number theory: LLM-assisted *formalization* of a human-complete argument is a qualitatively different (and much safer) use of AI than LLM-assisted *search* for the argument itself. 5. A byproduct habit worth reusing: while researching the problem's history to write the paper, the authors found Hall's older, independent counterexample had been sitting unnoticed in the literature for ~90 years — a reminder that for old, well-known open problems, a literature-history pass (not just a fresh attack) can itself turn up a solution that was already implicit in adjacent classical work (here, 1930s–40s finite-geometry papers on cyclic projective planes, written before Erdős even posed the question).

Why this is the reusable part. The general shape — (i) recast a "can a partial structure X be completed to a full combinatorial design" question as a rigidity condition on an auxiliary geometric object (here, a polarity of a projective plane) attached to that design; (ii) invoke classical structural theorems about that auxiliary object (Baer's absolute-point propositions) to get free case splits; (iii) chase the case split down to an explicit small numeric collision using the candidate structure's own elements; (iv) formalize only after the informal proof is complete, treating the proof assistant's kernel (not the LLM) as the trust anchor — is directly transferable to any "does every small instance of combinatorial structure $S$ extend to a full instance of the richer, rigidly-constrained structure $S'$" question where $S'$ has a known auxiliary-geometry/polarity/incidence-structure characterization (e.g. partial Sidon sets vs. full difference sets, partial Steiner systems vs. full designs, partial Latin squares vs. full ones with extra algebraic structure).

Related

- Sidon sets / B_2 sets / Golomb rulers — Sidon sets and their finite-field/perfect-difference-set constructions (Singer 1938); the parent object class this problem asks an extension question about. - Erdős #28 — additive basis forces unbounded representations — a different, still-open Erdős conjecture in the same additive-basis/representation-function cluster, illustrating the contrast: #707 was a finite, algorithmically-checkable extension question amenable to an explicit-counterexample-plus-formal-verification attack, whereas #28 is a genuinely infinitary $\limsup$ statement no finite computation (LLM-assisted or not) can settle either way. - Erdős #42 — every Sidon set has a same-scale Sidon set with disjoint differences, Erdős #43 — Sidon-pair size bound (disproved) — sibling finite Sidon-set problems in the same wiki area recently solved/disproved with heavy AI assistance (per wiki/concepts/sidon-sets.md's Related section), part of the same emerging pattern of AI-formalization-assisted resolutions of finite, checkable Erdős problems. - Marshall Hall, Jr., "Cyclic projective planes" — the independently-discovered, decades-earlier counterexample source; Baer's propositions on absolute points of polarities are the classical finite-geometry machinery both Hall's original work and Alexeev–Mixon's disproof route through. - erdosproblems.com/707 and erdosproblems.com/forum/thread/707 — the problem's catalog entry (not independently re-fetched this session, HTTP 403 on direct fetch; content triangulated via WebSearch snippets, flagged in provenance above). - github.com/google-deepmind/formal-conjectures, FormalConjectures/ErdosProblems/707.lean — the community Lean-formalization repository's own record of the problem and its resolved status.