Tagewerk XV

Independent kernel verification of the finite core of Erdős Problem 707 (Sidon-Extension Conjecture)

An independent kernel verification of the finite core of a freshly-resolved $1000 Erdős problem. Erdős Problem 707, the Sidon-Extension Conjecture, asserts that every finite Sidon set (a set of integers whose pairwise differences are all distinct) extends to a finite perfect difference set — a set B in ℤ_v of size n, with v = n²−n+1, in which every nonzero residue is a difference exactly once. Erdős posed it repeatedly from 1976 with a $1000 reward, and it stood for nearly 50 years. Alexeev and Mixon (arXiv:2510.19804, October 2025) disproved it: the size-5 Sidon set {1,2,4,8,13} extends to no perfect difference set (as does Hall's 1947 set {1,3,9,10,13}, which predates the conjecture). Niu (arXiv:2604.25214) then exhibited size-4 candidates {0,1,3,11} and {0,1,4,11} that fail to extend for every modulus v ≤ 133, evidence that the smallest non-extending Sidon set has size 4. LLMs propose nothing here; the Lean 4.31 kernel decides. The key reduction is that a perfect difference set of order n satisfies n(n−1) = v−1, so a size-n set in ℤ_v is a perfect difference set precisely when its pairwise differences mod v are all distinct; hence non-extension at a given order is a bounded, decidable fact — no size-n superset of S is Sidon mod v. We kernel-decide, for each of the four counterexample sets and with no axioms: that it is a Sidon set; that it does not extend to a perfect difference set at order |S| (the set reduced mod v is not one); and that it does not extend at order |S|+1 (adjoining any single residue never yields one). Our instrument additionally reproduces the non-extension for all orders with v ≤ 43, a faithful slice of the papers' unconditional exhaustion. Honest scope: non-extension to ANY finite perfect difference set is an infinite claim, established non-finitely by the polarity argument (the size-4 case remains conjectural); we certify the finitely-checkable core.