Claims

../

1959_09_03_cassels: Cassels's 1960 Theorem I: a set whose dyadic increments outgrow log log n and whose squared distance sums diverge at every theta in (0,1) represents every large integer as a sum of distinct elements; refereed.

2026_07_15_fan: Fan's 2026 preprint: divergent distance sums at every non-integer angle and five elements in every large dyadic interval give strong completeness; accepted on a Lean formalization of its six-per-interval version built here.

2026_07_15_snyder: Snyder's Lean 4 proof of the site's statement, produced with GPT 5.6 and posted on 15 July 2026 with a write-up and a Lean project; formal-conjectures registers it as the formal proof.

---