---

Boris Alexeev and Dustin G. Mixon, Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof, Proc. Natl. Acad. Sci. USA 123 (2026), no. 21, e2531760123; arXiv:2510.19804 (version 1 of 2025-10-22, version 2 of 2026-01-16); library card. Theorem 8: the Sidon set $\{1,2,4,8\}$ extends to no perfect difference set modulo $p^2+p+1$ for any prime $p$. Theorem 9: the Sidon set $\{1,2,4,8,13\}$ extends to no perfect difference set modulo any $v$. Both sets are initial segments of the greedy (Mian–Chowla) Sidon sequence. Theorem 8 alone answers Problem 707 as stated, with modulus $p^2+p+1$ for a prime $p$, in the negative; Theorem 9 refutes the form with an arbitrary modulus as well. Section 3 gives a short direct proof of Theorem 8; Sections 4 and 5 prove both theorems along Hall's 1947 argument, through the projective plane of a perfect difference set and the polarity $x\leftrightarrow B-x$, and show on the way that Hall's set (claim page) was a counterexample three decades before Erdős posed the question.

The Lean file Erdos707.lean, an ancillary file of the arXiv record (Lean 4.24.0, Mathlib v4.24.0), defines erdos_707_prime (the problem as stated), erdos_707 (any modulus) and erdos_707_integer (integer sets), and proves not_erdos_707P : ¬ erdos_707_prime from $\{1,2,4,8\}$ and not_erdos_707AM : ¬ erdos_707 from $\{1,2,4,8,13\}$, closing with a printed axiom line of propext, Classical.choice and Quot.sound. The authors write that the proof code was generated by ChatGPT and that they checked the formal statements themselves; they chose the formal route because Hall's remark had gone unnoticed for so long. Alexeev re-posted the version-1 ancillary file, which lacks version 2's toolchain header and closing axiom line, in Alexeev's repository of formalized Erdős problems on 2025-11-27 (the second formalization link, pinned). Section 8 asks for the smallest size $s$ of a Sidon set that extends to no perfect difference set and shows only $3\leq s\leq 5$. The site's problem page records a MathOverflow argument of Sawin that every Sidon set of size $3$ extends; its remarks (last edited 2025-10-26) record size $4$ as open.

Acceptance. The site's curator, T. F. Bloom, records the disproof on the problem page (last edited 2025-10-26) under the label DISPROVED (LEAN), which is the reviewed evidence named here. The paper is refereed: Proc. Natl. Acad. Sci. USA 123 (2026), no. 21, e2531760123. This corpus has not built the Lean file or audited its statements, so formalized is not listed.

Depends on. Nothing beyond the cited paper.