Optimal Exponent Relating Sumsets and Difference Sets
resolvedconfidence 70%
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
For every finite set $A\subset\mathbb Z$ with $|A|\ge 2$, define
$$C(A)=\frac{\log\left(|A+A|/|A|\right)}
{\log\left(|A-A|/|A|\right)}.$$
Determine the largest possible value of $C(A)$, equivalently the least universal exponent $c$ such that
$$\frac{|A+A|}{|A|}
\le
\left(\frac{|A-A|}{|A|}\right)^c$$
for every such set $A$. The result proves that the supremum is exactly $2$, although no individual admissible set attains it.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
Hy3
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.
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.