{"id":"palomar/PALOMAR-2026-10-21-000023","url":"https://github.com/AItoBit/ma-tang-sidon-lean/tree/5b60244934f6f220007f549ecff4e94bb5f2ee65","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000023-v1.json","repo":"https://github.com/AItoBit/ma-tang-sidon-lean","tags":["math.CO","math.NT","msc:11B75","msc:05C65","additive-combinatorics","sidon-sets","lean","density"],"score":0,"title":"Selected Sidon subset theorems of Ma–Tang (partial paper formalization)","trust":"high","domain":"math.CO","source":"palomar","authors":["AItoBit"],"reviews":0,"subject":"math.CO","summary":"Lean 4 proofs of the exact largest-Sidon-subset guarantee g(n)=ceil((n+1)/2) for finite weak Sidon sets, its asymptotic density 1/2, convergence and the optimal-constant characterization for finite (4,5)-sets, and the upper bound cStar<=4/7. The project also proves the finite three-uniform transversal bound 4tau<=n+m used in the exact guarantee. This is a partial formalization of Ma–Tang, arXiv:2602.23282v2: Theorem5.3 and the lower9/17 bound in Theorem1.6 remain unproved.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"Largest Sidon Subsets in Weak Sidon Sets","identifier":"arXiv:2602.23282v2","relationship":"formalizes"}]}