TY - RPRT TI - Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4 AU - David B. Hulak AU - Arthur F. Ramos AU - Ruy J. G. B. de Queiroz PY - 2026 UR - https://arxiv.org/abs/2605.03274 ID - 2605.03274 ER -