{"id":"palomar/PALOMAR-2026-10-29-000036","url":"https://github.com/TomasOrtega/Sidon/tree/735de6d7c67b81a28b1e07e3f2661dbc17bb89d6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000036-v1.json","repo":"https://github.com/TomasOrtega/Sidon","tags":["math.CO","math.NT","msc:11B13","msc:11B75","msc:05D10"],"score":0,"title":"Extremal Sidon sets: Fourier uniformity and partition regularity","trust":"high","domain":"math.CO","source":"palomar","authors":["Tomas Ortega"],"reviews":0,"subject":"math.CO","summary":"A Lean formalization of Ortega and Prendiville's results on Sidon sets in integer intervals. It proves Fourier bounds for near-maximal and largest Sidon sets, equidistribution in progressions and Bohr sets, and monochromatic solutions to partition regular linear equations in at least five variables. It also proves sharp obstruction constructions and records a correction to the paper's dimension-independent approximation claim.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"Extremal Sidon sets are Fourier uniform, with applications to partition regularity","identifier":"doi:10.5802/jtnb.1239","relationship":"formalizes"}]}