Lean 4 formalization proves Singer's Sidon-set construction for every prime power and builds a library that yields unconditional two-sided bounds h(N)=Θ(√N) plus a conditional route to the full Erdős Problem 30 asymptotic.
Bertrand, Mémoire sur le nombre de valeurs que peut prendre une fonction quand on y permute les lettres qu’elle renferme,J
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
fields
math.CO 1years
2026 1verdicts
ACCEPT 1representative citing papers
citing papers explorer
-
Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4
Lean 4 formalization proves Singer's Sidon-set construction for every prime power and builds a library that yields unconditional two-sided bounds h(N)=Θ(√N) plus a conditional route to the full Erdős Problem 30 asymptotic.