Breaking the high-degree barrier in Lehmer's problem with a human-AI discovery loop

Yuri Chervonyi; Sergei Gukov; Thang Luong

cs.AIOct 21, 2026

Breaking the high-degree barrier in Lehmer's problem with a human-AI discovery loop

Authors: Yuri Chervonyi, Sergei Gukov, Thang Luong

Organizations: Google DeepMind · California Institute of Technology

Abstract

While artificial intelligence has made rapid progress in mathematical reasoning, many open problems depend on structure that is revealed only through large-scale computational exploration and analytical synthesis. One such example is Lehmer's problem from 1933. It asks whether the Mahler measure of an integer polynomial, which measures how far its roots stray from the unit circle, can be made arbitrarily small. Previously, constructing irreducible polynomials with integer coefficients and small Mahler measure has been carried out systematically only for even degrees $d \le 180$ . At higher degrees, Boyd's analytical one-parameter family frequently factors, skipping nearly 50% of target degrees and leaving no general construction for arbitrary $d$ . Here, we address the high-degree regime through a human-AI discovery loop, in which we extend the conversational prompting with a fast numerical pipeline, an exact symbolic verifier, and large-scale distributed search. The AI agent prototypes numerical and symbolic solvers locally, launches parallel searches across distributed clusters and works with the human researcher to extract and verify mathematical hypotheses. Through this interactive loop, we derive a five-parameter construction, which we call the Generalized Boyd algorithm. It eliminates degree-skipping and constructs irreducible polynomials with Mahler measure strictly below Boyd's limit point $α_1 \approx 1.255434$ for every target degree. Evaluated across all even degrees up to 2000, our approach improves upon six previously published values and holds 99.6% of all best known records. With this work we release the verified dataset of polynomials with minimal Mahler measure across all studied even degrees.

Figures & tables

Figure 1: Global convergence of univariate Mahler measures at high degree

d

to Boyd’s limit

\alpha_{1}

. (a) Comparison of published Literature Optima (91 degrees, red open circles), the computational Search Ensemble discovered by reinforcement learning, evolutionary search, and periodic defect tiling (824 degrees, blue circles), the 1-Parameter Boyd family (504 degrees, cyan diamonds), and the Generalized Boyd family (995 degrees, green triangles) against the limit

\alpha_{1}\approx 1.255434

(red dashed line) and lower envelope

\alpha_{1}-Ad^{-3/2}

(black dash-dot curve). (b) High-degree regime (

d\geq 100

), showing how the Generalized Boyd family follows the lower envelope

\alpha_{1}-Ad^{-3/2}

strictly below

\alpha_{1}

, whereas the 1-Parameter Boyd family oscillates between the lower and upper envelopes

\alpha_{1}\pm Ad^{-3/2}

Polynomial Family	# of $d$ ’s	Key Empirical & Theoretical Properties
Literature Optima [ 30 ]	91	Known minima for $d\leq 250$ (systematic coverage up to $d\leq 180$ ).
Search Ensemble	824	RL, evolutionary, and defect-tiling optima; matches 85 and beats 6 of the 91 Literature Optima.
1-Parameter Boyd	504	One-parameter specialization; skips nearly $50\%$ of target degrees; beats the Search Ensemble on 118 degrees.
Generalized Boyd	995	Applies to any even $d\geq 12$ ; verified irreducible with $M(P_{d})<\alpha_{1}$ for all $d\in[12,2000]$ ( $99.6\%$ of records).

Table 1: Summary of polynomial families evaluated on the high-degree benchmark (

d\leq 2000

Panel of Figure 2 — Figure 2: Interactive human–AI discovery loop built on Gemini and Google Antigravity. A continuous validation loop connects local agentic reasoning and tool-building with large-scale cloud experiments and automated verification on Google Cloud (CPU and GPU clusters), while human–AI collaboration distills empirical patterns into general analytical models.

Discovery Paradigm	Representative Works	AI Role in Loop	Primary Output & Limitation
Standalone RL / Neural Sampling	Wagner [ 17 ] , AlphaTensor [ 10 ] , PatternBoost [ 18 ]	Fixed-reward policy optimization	Isolated finite counterexamples; no closed-form symbolic law.
ML-Guided Human Intuition	Davies et al. [ 15 ] , Shehper et al. [ 16 ]	Feature attribution & pattern guidance	Human-formulated conjecture; AI does not run iterative experiments.
Closed-Loop Code Evolution	FunSearch [ 19 ] , AlphaEvolve [ 20 ]	Automated heuristic mutation	Evolved search scripts against a static pre-written evaluator.
Formal Proving & Local Neurosymbolic	AlphaGeometry [ 22 , 23 ] , Co-Scientist [ 13 ] , Xia et al. [ 95 ]	Deductive search & local solver steering	Formal proofs or bounds derived from single-node / small- $n$ solver exploration; no distributed cloud scale or asynchronous symbolic verification at scale.
Interactive Cloud Experiment–Hypothesis–Verification	This Work (Gemini + Antigravity)	Co-designs domain solvers, scales cloud sweeps, and runs exact symbolic checks	Synthesizes large-scale numerical optima into closed-form analytical constructions.

Table 2: Comparison of Human–AI Mathematical Discovery Paradigms.

Figure 3: Minimal known Mahler measure. (a) Prior literature covers 91 even degrees up to

d\leq 250

[ 33 , 36 , 30 ] . (b) Our numerical search methods establish 824 even degree optima across

d\leq 2000

, strictly improving 6 prior literature bounds at

d\leq 250

and establishing the upper bounds across 733 additional degrees.

Algorithm	Wins	Share	Degrees
Periodic Tiling + Defect	447	$54.2\%$	$d\in[10,1846]$
RL Cross-Entropy Policy	186	$22.6\%$	$d\in[14,800]$
Direct Sparse Search	111	$13.5\%$	$d\in[44,1996]$
Priority Search	57	$6.9\%$	$d\in[20,290]$
Evolutionary Search	23	$2.8\%$	$d\in[12,300]$
Total	824	100.0%	$d\in[10,2000]$

Table 3: Our leaderboard entries (

d\leq 2000

) by search method.

Degree $d$	Literature $M_{\mathrm{lit}}$	New Bound $M(P_{d}^{*})$	Improvement $\Delta M$
$178$	$1.25204881$	$1.25162839$	$-0.00042$
$188$	$1.28309200$	$1.25207822$	$-0.03101$
$190$	$1.28518461$	$1.25198376$	$-0.03320$
$202$	$1.25478722$	$1.25253255$	$-0.00225$
$242$	$1.28571755$	$1.25305628$	$-0.03266$
$250$	$1.28497453$	$1.25316520$	$-0.03181$

Table 4: Strict improvements over literature for

d\leq 250

Family	Degrees Covered	Best / Tied Records	Max $M$	All $M<\alpha_{1}$ ?
Search Ensemble	824	163	$1.255965$	No
One-parameter Boyd	504	19	$1.311999$	No
Generalized Boyd	995	991 ( $99.6\%$ )	$\mathbf{1.255358}$	Yes

Table 5: Comparative performance of our search algorithms, One-parameter Boyd family

Q_{n}(x)

, and the Generalized Boyd algorithm

Q_{a,b,k,s_{0},s_{1}}(x)

evaluated on the benchmark (

d\leq 2000

), alongside several explicit examples.

Figure 4: Scale invariance of unit-circle root condensation established via exact root counting over

\mathbb{Q}

. (a) Unit-circle root percentage

100\times N_{\mathrm{uc}}(P_{d})/d

across all 824 optimal polynomials, showing that optimal polynomials remain tightly concentrated within

77.0\%\text{--}88.0\%

(global mean

82.51\%

) on

|z|=1

. (b) Linear scaling of the unit-circle root count

N_{\mathrm{uc}}(P_{d})\approx 0.8251\,d

with polynomial degree

d

across two orders of magnitude.

Figure 5: Complex-plane root distributions for representative polynomials (

d\in\{10,100,164,300,600,1846\}

). Most roots lie on the unit circle

|z|=1

(cyan circles), while the remaining roots form reciprocal pairs outside (

|z|>1

, red triangles) and inside (

|z|<1

, orange triangles) the circle. At

d=10

(Lehmer’s polynomial), only a single pair lies off the circle; at higher degrees, off-circle roots either concentrate near

z=-1

(

d=164

and

d=600

a=1

) or split into

a

evenly spaced clusters around the circle (

d=100,300,1846

with

a=5,13,31

). Radial distances from

|z|=1

are magnified for visibility.

Deg $d$	Best $M(P_{d}^{*})$	Lit. $M_{\mathrm{lit}}$	Method	Tuple $(a,b,k,s_{0},s_{1})/\Phi$ or Form	$N_{\mathrm{uc}}(P_{d}^{*})/d$
$10$	$1.17628082$	$1.17628082$	Tiling / Lit	Lehmer’s polynomial $L(x)$ ( 2 )	$80.0\%$
$12$	$1.22778556$	$1.22778556$	Evol. / Lit	$x^{12}+x^{11}+x^{10}-x^{8}-x^{7}-x^{6}-x^{5}-x^{4}+x^{2}+x+1$	$66.7\%$
$14$	$1.20002652$	$1.20002652$	Gen. Boyd	$(3,4,0,-1,-1)$ (7-term, $\delta=0$ )	$85.7\%$
$18$	$1.18836815$	$1.18836815$	Gen. Boyd / RL	$(1,10,0,-1,-1)/\Phi_{12}$ ( $\delta=4$ )	$88.9\%$
$178$	$1.25162839$	$1.25204881$	Gen. Boyd	$(4,89,0,-1,-1)/\Phi_{15}$ ( $\delta=8,\Delta M=-0.00042$ )	$85.4\%$
$188$	$1.25207822$	$1.28309200$	Gen. Boyd / RL	$(11,86,0,+1,+1)/\Phi_{7}$ ( $\delta=6,\Delta M=-0.03101$ )	$83.0\%$

Table 6: Selected Benchmark Records from the 996-Degree Dataset (

d\in[10,2000]

) , illustrating small-degree optima, all 6 strict improvements over published Literature Optima, and high-degree records in compact cyclotomic-quotient form.

Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

Degree Regime	Polys	Total Roots	Unit-Circle $N_{\mathrm{uc}}$	Unweighted Mean $N_{\mathrm{uc}}/d$	Interdecile Range
Degrees $10\text{--}100$	46	2,530	2,020	$79.84\%$	$[75.0\%,84.6\%]$
Degrees $102\text{--}300$	100	20,100	16,708	$83.12\%$	$[79.2\%,86.4\%]$
Degrees $302\text{--}700$	199	99,700	82,212	$82.46\%$	$[78.5\%,86.1\%]$
Degrees $702\text{--}1500$	306	336,800	278,130	$82.58\%$	$[78.8\%,86.3\%]$
Degrees $1502\text{--}2000$	173	293,950	243,358	$82.78\%$	$[79.1\%,86.5\%]$
Global Ensemble	824	753,080	622,428	$\mathbf{82.51\%}$	$\mathbf{[77.0\%,88.0\%]}$

Appendix

Table 7: Exact Unit-Circle Root Statistics Across Degree Regimes computed via exact root counting over

\mathbb{Q}

Figure 6: Angular and radial distribution of off-circle roots ( $|z_{j}|>1$ ). (a) Log modulus $\log|z_{j}|$ versus angle $\theta_{j}\in[-\pi,\pi]$ grouped by discovery method, showing radial contraction $\log|z_{j}|=\mathcal{O}(1/d)$ across all angles. (b) Polar view of exterior roots ( $|z_{j}|>1$ ) around the unit circle $|z|=1$ , colored by degree $d$ . Note that by reciprocal symmetry, every exterior root at $z_{j}$ is paired with an interior root at $1/\overline{z_{j}}$ at the same angle $\theta_{j}$ with $\log|1/\overline{z_{j}}|=-\log|z_{j}|$ .

AI-Assisted Mathematical Discovery

See all 21 papers

Advancing Mathematics Research with AI-Driven Formal Proof Search
May 21, 2026George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18Large Language Model-Guided Theorem Proving Automated Theorem Proving
1Google DeepMind1 · 2Aarhus University · 3Google
Constrained PSLQ Search for Machin-like Identities Achieving Record-Low Lehmer Measures
Aug 8, 2025Nick Craig-Wood
Iteris: Agentic Research Loops for Computational Mathematics
Jun 1, 2026Leheng Chen, Zihao Liu, Wanyi He +1Mathematical Reasoning Large Language Model-Guided Scientific Discovery
School of Mathematical Sciences, Peking University · 5Zhongguancun Academy · 2Beijing International Center for Mathematical Research and the New Cornerstone Science Laboratory, Peking University +2

May 21, 2026J/K move · Enter open · S save

Advancing Mathematics Research with AI-Driven Formal Proof Search

George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina+17

1Google DeepMind1 · 2Aarhus University · 3Google

Large Language Model-Guided Theorem Proving Automated Theorem Proving AI Agent Evaluation Lean Theorem Proving LLM Mathematical Reasoning Autonomous Research Agents

Open paper AskPDF arXiv

Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.

Abstract

AI-Assisted Mathematical Discovery

Explore similar work

Advancing Mathematics Research with AI-Driven Formal Proof Search

Constrained PSLQ Search for Machin-like Identities Achieving Record-Low Lehmer Measures

Iteris: Agentic Research Loops for Computational Mathematics