Optimal exponent relating sumsets and difference sets determined
The least universal exponent c with |A+A|/|A| bounded by (|A-A|/|A|)^c for every finite integer set A is determined, settling the extremal question with a Lean 4 formalization.
- Model
- Hy3 (Hyra research agent)
- Field
- Mathematics
- Date
- 2026-07-29
- Human collaborators
- Haowei Lin, Shanda Li
Sources
Original work
Independent commentary
What was found
For a finite set A of integers with at least two elements, the ratio of log(|A+A|/|A|) to log(|A-A|/|A|) measures how far sumset growth can outrun difference-set growth. Determining its largest possible value fixes the least universal exponent c such that |A+A|/|A| is at most (|A-A|/|A|)^c for every such A. Tencent Hunyuan's Hyra research agent, powered by the Hy3 model, explored and optimized finite-set constructions over roughly a 24-hour run, moving from finite numerical searches to natural-language proposals of general constructions and supporting arguments, and produced the construction underlying the paper. The human authors independently checked the construction, corrected and rewrote the exposition, and prepared the final proof manually.
Novelty check
The relationship between sumset and difference-set growth is a standard question in additive combinatorics with a long record of partial bounds on the exponent; the extremal value was recorded as undetermined. The paper states the prior bounds it improves on. The construction is new, not a retrieval of a known extremal family.
Caveats and known objections
A newly released arXiv v1 preprint, not peer-reviewed. The Lean 4 and Mathlib formalization is author-provided; the repository reports lake build completing with no sorry declarations or warnings, but the principal asymptotic and supremum results rely on three native_decide certificates for elementary finite computations over a 12-element base-39 digit block, so those steps are trusted to the Lean kernel's decision procedure rather than proved term by term. Autonomy graded ai-led rather than autonomous: the agent produced the construction, but humans posed the problem, checked it and wrote the final proof.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Optimal exponent relating sumsets and difference sets determined. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-07-29-sumset-difference-exponentBibTeX
@misc{whataifound-tencenthunyuan-2026-exponent,
title = {Optimal exponent relating sumsets and difference sets determined},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Tencent Hunyuan. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-07-29-sumset-difference-exponent}
}