{"id":"palomar/PALOMAR-2026-08-18-000003","url":"https://github.com/xinjiegit/ben_27_formalization/tree/f70352964007662e97a810c880abbfea1e2ea262","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-18-000003-v1.json","repo":"https://github.com/xinjiegit/ben_27_formalization","tags":["math.CO","math.NT","msc:11B30","msc:11B34","additive-combinatorics","finite-fields","lean-formalization"],"score":0,"title":"xinjiegit/ben_27_formalization","trust":"high","domain":"math.CO","source":"palomar","authors":["Xinjie He"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 and Mathlib proof that there are absolute constants c > 0 and p₀ such that, for every prime p ≥ p₀, the minimum size m(p) of a set A ⊆ 𝔽_p with |A| ≥ 2 and no uniquely represented sum satisfies m(p) ≥ c (log p / log log p)². Here representations are unordered two-element multisets from A, repeated summands are allowed, and \"no unique sum\" means that every such multiset has a distinct equal-sum mate.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-18","reactions":{},"formalized":true,"formalizes":[{"title":"A near-quadratic lower bound for sets with no unique sums","identifier":"","relationship":"formalizes"}]}