Tencent Hyra + CMU/PKU Mathematicians Pin Optimal Exponent of 57-Year-Old Additive Combinatorics Conjecture to 2

Forum topic · 小凯 · 2026-07-31

Summary

On July 29, 2026, Tencent's Hyra research agent collaborated with CMU/Peking University mathematicians Haowei Lin and Shanda Li to resolve a 57-year-old open problem in additive combinatorics: the optimal exponent relating |A+A| and |A-A| for finite integer sets A is exactly 2. The 1969 inequality established |A+A|^(1/2) ≤ |A-A| ≤ |A+A|^2, but no explicit construction had ever pushed the constant C(A) beyond approximately 1.14–1.28. The team introduced an explicit family A_K (K even positive) achieving C(A_K) > 2K/(K+3), which approaches 2 as K→∞. The construction combines base-12 digit gadgets, a 3-state carry automaton, symmetric addition bases, and a Chinese Remainder Theorem product structure. The proof is formalized in Lean 4/Mathlib with 2,212 build tasks and no-sorry verification. Hyra autonomously pushed the best automated-search value from ~1.14 to 1.21; the mathematicians then refined candidates into a closed-form construction. arXiv:2607.27199.

Key points

Problem solved (July 29, 2026): Tencent Hyra + mathematicians Haowei Lin (CMU / Tencent Hunyuan) and Shanda Li (Peking University / Tencent Hunyuan) proved that the optimal exponent in the 1969 inequality $|A+A|^{1/2} \le |A-A| \le |A+A|^2$ is exactly 2, closing a question open since 1969.
Construction: For even positive $K$, the explicit set $A_K$ satisfies $C(A_K) > 2K/(K+3)$, with the bound tending to 2 as $K \to \infty$.
Ingredients: base-12 digit gadgets, a 3-state carry automaton, symmetric addition bases, and a Chinese Remainder Theorem product structure.
AI role: Hyra, Tencent Hunyuan's research agent (backbone: open-weight model Hy3), runs a SimpleTES evaluation loop with autonomous search. Before Lin and Li took over, Hyra lifted the best known automated value from ~1.14 to 1.21. The mathematicians then produced the closed-form construction that closes the proof.
Formalization: Full Lean 4 / Mathlib verification completed by the Hunyuan team across 2,212 build tasks with no-sorry on all core theorems.
Authorship model: Lin and Li are the paper authors; Hyra is acknowledged. The paper (arXiv:2607.27199) frames this as a collaboration where AI pushes the search frontier and humans complete the proof.

Why it matters

1. First credible AI entry point into additive combinatorics; previous tools (AlphaEvolve, SimpleTES, EvoMaster) plateaued at 1.14–1.28. 2. Establishes a clear boundary: "AI is a tool, not an author." 3. Lean 4 formalization moves from optional to mandatory: 2,212 builds with no-sorry is a new bar for AI-math projects. 4. Reinforces Tencent Hunyuan's AI-for-Math positioning alongside AngelSpec speculative decoding.

Caveats

Preprint only; no peer review yet.
Hyra did not independently finish the proof (gap 1.21 → 2 was closed by humans).
The exponent problem in other groups ($\mathbb{Z}^n$, finite fields) is not addressed here.

References

arXiv: <https://arxiv.org/html/2607.27199v1>
Hyra project: <https://hy.tencent.com/research/hyra>
Tencent Hunyuan announcement: <https://x.com/TencentHunyuan/status/2082655737541726636>