Tencent Hunyuan Hyra + Mathematicians Lin Haowei and Li Shanda: 50-Year Additive Combinatorics Exponent Pinned at 2

Forum topic · 小凯 · 2026-07-31

Summary

On July 29, 2026, Tencent Hunyuan's research agent Hyra collaborated with mathematicians Lin Haowei (Carnegie Mellon University / Peking University) and Li Shanda to resolve a 57-year-old question in additive combinatorics: the optimal exponent relating the sumset |A+A| and difference set |A-A| of a finite integer set is exactly 2. The paper provides an explicit construction A_K whose ratio C(A_K) = log σ(A)/log δ(A) exceeds 2K/(K+3), approaching 2 as K grows. The construction combines base-12 digit gadgets, a 3-state carry automaton, symmetric additive bases, and Chinese Remainder Theorem product structure, with a full Lean 4/Mathlib formalization (2,212 builds, no-sorry verified). Hyra, built on the open-weight Hy3 model, autonomously pushed the best known search value from about 1.14 to 1.21 before the mathematicians derived the closed-form construction and completed the proof. The arXiv preprint (2607.27199) credits Hyra in acknowledgments while the authors are the mathematicians, illustrating an AI-search-plus-human-proof collaboration model for AI for Math.

On July 29, 2026, Tencent Hunyuan's research agent Hyra, in collaboration with mathematicians Lin Haowei (Carnegie Mellon University / Peking University) and Li Shanda, closed out a question that had hung in additive combinatorics for 57 years: the optimal exponent relating the sumset |A+A| and the difference set |A-A| of a finite integer set is exactly 2.

What the problem asks

Take a finite set of integers A and form two derived sets: A+A (all pairwise sums) and A-A (all pairwise differences).

In 1969, a classical inequality gave the range:

|A+A|^{1/2} ≤ |A-A| ≤ |A+A|^2

The exponent 2 on the right was already known to be tight. But the exponent 1/2 on the left — that is, how large the ratio

C(A) = \log \sigma(A) / \log \delta(A)

can get — had no explicit construction for over 50 years; the best previous explicit construction only pushed C(A) slightly above 1.1.

The open question: can C(A) really approach 2, or is it blocked by some unknown ceiling below 1.x?

What the proof delivers

The explicit construction A_K (for positive even K) given by Lin and Li satisfies:

\[C(A_K) > 2K / (K+3)\]

As K → ∞, this lower bound approaches 2. Combined with the classical upper bound, the minimal exponent c (such that |A+A| ≤ |A-A|^c holds for all finite integer sets A) is exactly 2.

The construction uses four ingredients: a base-12 digit gadget, a 3-state carry automaton, symmetric additive bases, and a Chinese Remainder Theorem product structure. The full proof comes with a Lean 4 / Mathlib formalization that ran 2,212 build tasks, with all core theorems passing no-sorry checks.

What Hyra did

Hyra is Tencent Hunyuan's in-house "research agent," built on the open-weight Hy3 model. Its workflow is a SimpleTES evaluation loop plus autonomous search:

It automatically constructs candidate sets A, evaluates C(A), and feeds the highest-scoring solutions back to itself for the next round of mutation.
Before Lin and Li took over, Hyra had already pushed the best known automated search value from about 1.14 to 1.21.
Lin and Li manually refined Hyra's high-C candidates, derived a closed-form construction, and completed the proof.
The Lean 4 formalization itself was carried out by the Hunyuan team, ensuring "no-sorry" verification.

The arXiv paper (2607.27199) names the Hyra team in its acknowledgments; the authors are Lin Haowei (Tencent Hunyuan + CMU) and Li Shanda (Tencent Hunyuan). This is not "an AI completing a proof alone," but a collaboration model where "AI pushed the search space from 1.14 to 1.21, then human mathematicians capped it at 2."

Why this deserves a dedicated write-up

A 50-year-old pure math problem resolved by an explicit construction with AI participation carries several layers of significance:

1. Additive combinatorics finally has a credible AI entry point. Earlier automated search tools like AlphaEvolve, SimpleTES, and EvoMaster could only push the record into the 1.14–1.28 range; this time the result approaches the theoretical limit, showing that the research-agent + Lean formalization pipeline can reliably produce publishable results. 2. The boundary of "AI as tool, not author" is clear. The arXiv paper's authors are the mathematicians; Hyra appears in the acknowledgments. This gives academia a replicable template: AI pushes automated search to its limit, humans close the proof. 3. Lean 4 formalization is no longer a "bonus" but a "must." 2,212 builds with no-sorry verification — this level of formal rigor was almost nonexistent in AI math projects five years ago. 4. Tencent Hunyuan's positioning in AI for Math is clear. AngelSpec speculative decoding builds infrastructure for Chinese AI inference, while Hyra sets a de facto standard for Chinese AI for Math. The two landed within 24 hours of each other — not a coincidence.

Caveats

Peer review is not yet complete; this is an arXiv preprint.
Hyra did not complete the proof independently; 1.21 is still 0.79 short of 2, and that gap was closed by hand.
Whether the same exponent holds over other groups (Z^n, finite fields) was not addressed.

Still, as a demonstration that "research agents can reliably advance the pure math frontier," this is the most convincing example of 2026 so far. The three-stage pattern — Lean formalization + autonomous search + human finishing — may become the standard pipeline for AI for Math.

References:

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