Settling the Optimal Exponent Relating Sumsets and Difference Sets

Haowei Lin, Shanda Li

math.CO Jul 29, 2026 · v1

Read PDF arXiv abstract Code

TL;DR

The main theorem's proof was converted by an LLM into a Lean 4 formal proof, which is released in a public GitHub repository.

Abstract

For a finite nonempty subset $A$ of an abelian group, let $σ(A)=|A+A|/|A|$ and $δ(A)=|A-A|/|A|$. The classical sum-difference inequalities state that $$σ(A)^{1/2}\leqδ(A)\leqσ(A)^2.$$ The exponent $2$ in the second inequality is known to be optimal, whereas it has remained open whether the exponent $1/2$ in the first inequality can be improved. We settle this question by constructing an explicit family of finite sets $A_K\subset\mathbb{Z}$ such that $$\frac{\logσ(A_K)}{\logδ(A_K)}\longrightarrow 2,$$ hence the exponent $1/2$ in the first inequality is also optimal. The construction and its proof were developed with the assistance of Hyra, an AI research agent based on the open-weights Hy3 model.

Problem

For finite sets A of integers, the sum-difference inequalities state σ(A)^{1/2} ≤ δ(A) ≤ σ(A)^2. The exponent 2 in the second inequality was known to be optimal. It was open whether the exponent 1/2 in the first inequality could be improved, equivalently whether sup log σ(A)/log δ(A) equals 2.

Approach

An explicit family A_K ⊂ ℤ is built from four ingredients: a base-12 digit gadget W={0,1,2,4,5,9}, a three-state carry automaton that counts modular differences, a symmetric additive basis in a cyclic group, and a Chinese remainder construction. The construction was found with the AI research agent Hyra (Hy3 model), guided by an LLM judge. The authors checked the proof by hand, and GPT-5.6 Sol converted the natural-language proof into Lean 4.

Results

For every positive even K, C(A_K) > 2K/(K+3), so C(A_K) → 2 and the exponent 1/2 is optimal. This exceeds prior constructions and agent-search results, including Penman–Wells at 1.1259 and SimpleTES at 1.1449. A Lean 4 formal proof is released.

Method	Value
Freiman–Pigarev (1973)	1.0598
Penman–Wells family	1.1259
AlphaEvolve	1.1219
SimpleTES with post-training	1.1449
Explicit family A_K (this work)	sup = 2

Selected best values of C(A)

Papers With

Settling the Optimal Exponent Relating Sumsets and Difference Sets