Companion code and data for “A finiteness theorem for geodesic Leech wheels”: labelings of W_5–W_13, exact-arithmetic verification of the bound n ≤ 40, and the spoke-frame search
-
Updated
Sep 3, 2026 - TeX
#
sidon-sets
Here are 6 public repositories matching this topic...
Erdos problem 1191 and Sidon sets: Lean 4 formulations, supporting lemmas, finite formalizations, and computational experiments. Research in progress.
computational-mathematics formalization formal-verification erdos mathlib lean4 additive-combinatorics erdos-problems sidon-sets erdos-1191
-
Updated
Oct 1, 2026 - Python
formalization formal-mathematics mathlib lean4 additive-combinatorics proof-verification singer-theorem sidon-sets
-
Updated
May 11, 2026 - Lean
Erdos problem #40: for which g(N) -> infinity must a set A with >> sqrt(N)/g(N) elements in {1,...,N} have limsup 1_A*1_A(n) = infinity? Open. Lean: some g works iff the strong form of the Erdos-Turan conjecture holds. Written, after Erdos and Renyi: no power of N works. Computed: the greedy B2[2] set from the #158 thread, to 10,000 terms.
mathematics formal-verification number-theory open-problems lean4 additive-combinatorics erdos-problems sidon-sets
-
Updated
Oct 16, 2026 - Python
ARCHIVED: historical Sidon-set scientific custody; not a current Vela product.
-
Updated
Aug 7, 2026 - C++
Erdos 39: formal Sidon density bounds, infinite greedy construction, computational controls and original receipts
-
Updated
Sep 18, 2026 - Lean
Add this topic to your repo
To associate your repository with the sidon-sets topic, visit your repo's landing page and select "manage topics."