xinjiegit/ben_27_formalization

Xinjie He

Palomar Registrypalomar/PALOMAR-2026-08-18-000003Aug 18, 2026math.COscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-18-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-18-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-18-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'