Optimal Exponent Relating Sumsets and Difference Sets
For every finite set with , define
Determine the largest possible value of , equivalently the least universal exponent such that
for every such set . The result proves that the supremum is exactly , although no individual admissible set attains it.
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Additive combinatorics
- Posed by
- —
- Year posed
- —
- Years open
- —
- Solved
- 2026-07-29
- Model
- Hy3
- Vendor
- Tencent Hunyuan
- Collaborators
- Haowei Lin, Shanda Li
- Verification
- Lean-verified
- Publication
- Preprint
- Significance
- 20 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
New arXiv preprint with an author-provided Lean formalization; not yet peer-reviewed.
What the AI did
Tencent Hunyuan’s Hyra research agent, powered by the Hy3 model, was used to explore and optimize finite-set constructions. During an approximately 24-hour run, Hyra produced the construction underlying the paper after moving from finite numerical searches toward natural-language proposals of general constructions and supporting arguments.
The human authors independently checked the construction, corrected and rewrote the exposition, and prepared the final mathematical proof manually. GPT-5.6 Sol was used as an exploration judge and later helped translate the natural-language argument into a Lean 4 formalization. The language-model judgments were not used as proof certificates.
Verification
This is a newly released arXiv v1 preprint and has not yet been peer-reviewed. It contains an explicit, self-contained mathematical construction and proof.
The authors also provide a Lean 4/mathlib formalization. The repository reports that `lake build` completes successfully with no `sorry` declarations or warnings. The principal asymptotic and supremum results use three `native_decide` certificates for elementary finite computations concerning a 12-element base-39 digit block. Consequently, those parts additionally trust Lean’s compiler and native execution, rather than relying exclusively on kernel reduction.
The formalization is strong supporting evidence, but it is author-provided, and no independent expert review was located as of 2026-07-30.
Source
Submitted by matthew on
Indeed it is!