The Alexeev–Mixon set {1, 2, 4, 8, 13} is a Sidon set extending to no perfect difference set of order 5 or 6 — the kernel-attested finite core of the disproof of Erdős Problem 707 (the $1000 Sidon-extension conjecture)

Enuntiatio — the claim

The Alexeev–Mixon set {1, 2, 4, 8, 13} is a Sidon set extending to no perfect difference set of order 5 or 6 — the kernel-attested finite core of the disproof of Erdős Problem 707 (the $1000 Sidon-extension conjecture)

Refuted by a repeated pairwise difference in {1,2,4,8,13} (not Sidon), or the set itself a perfect difference set mod 21, or an x0 < 31 making {1,2,4,8,13,x0} a perfect difference set mod 31

Expressio — the formal statement

import Mathlib.Tactic

set_option maxHeartbeats 800000

/-- pairwise differences (over ℤ) of a list — a set is a Sidon set iff these are all distinct. -/
def diffsZ (S : List Int) : List Int :=
  S.flatMap (fun a => S.filterMap (fun b => if a == b then none else some (b - a)))
/-- pairwise differences mod v (as ℕ). -/
def diffsMod (S : List Nat) (v : Nat) : List Nat :=
  S.flatMap (fun a => S.filterMap (fun b => if a == b then none else some ((v + b - a) % v)))
/-- B (⊂ ℤ_v) is a perfect difference set iff it is a distinct set whose pairwise diffs mod v are all
    distinct — equivalently Sidon mod v (valid since a PDS of order n has n(n−1) = v−1). -/
def isPDS (B : List Nat) (v : Nat) : Bool := (diffsMod B v).Nodup && B.Nodup

theorem erdos707_am_witness : (diffsZ [1, 2, 4, 8, 13]).Nodup ∧ isPDS [1, 2, 4, 8, 13] 21 = false ∧ (∀ x0 < 31, isPDS ([1, 2, 4, 8, 13] ++ [x0]) 31 = false)

Demonstratio — the kernel-checked proof

by decide