Source-linked AI summary
Towards Autonomous Mathematics Research
Tony Feng, Trieu H. Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang-hyun Kim, Federico Pasqualotto, Sergei Gukov, Jonathan N. Lee, Junsu Kim, Kaiying Hou, Golnaz Ghiasi, Yi Tay, YaGuang Li, Chenkai Kuang, Yuan Liu, Hanzhao Lin, Evan Zheran Liu, Nigamaa Nayakanti, Xiaomeng Yang, Heng-Tze Cheng, Demis Hassabis, Koray Kavukcuoglu, Quoc V. Le, Thang Luong
TL;DR
Research mathematics requires literature synthesis and long-horizon proof construction beyond competition-level problem solving. The paper introduces Aletheia, an agent that generates, verifies, and revises natural-language solutions using advanced reasoning, inference-time scaling, and research tools, and reports milestones including AI-generated and human-AI mathematics research. It also proposes transparency-oriented taxonomies for AI autonomy and mathematical significance while emphasizing that reliable autonomous research remains uncommon.
Problem
The paper addresses whether AI can autonomously discover and prove new mathematical theorems despite research mathematics requiring extensive literature synthesis and long-horizon proofs.
Method
Aletheia combines advanced Gemini Deep Think, inference-time scaling beyond Olympiad problems, iterative generation-verification-revision, and intensive search and browsing.
Results
Aletheia produced an AI-generated paper on eigenweights, supported a human-AI paper on independent sets, evaluated 700 Erdős problems with four autonomous solutions, and achieved leading performance on FirstProof.
Takeaways & Limitations
The work provides milestones for AI-assisted mathematics while proposing autonomy and significance taxonomies to make such contributions more transparent.
Takeaways & Limitations
Autonomous research success cases are rare, and the reported autonomous Erdős solutions were not individually judged to reach research-paper level.
Abstract
from arXiv · showhide
Recent advances in foundational models have yielded reasoning systems capable of achieving a gold-medal standard at the International Mathematical Olympiad. The transition from competition-level problem-solving to professional research, however, requires navigating vast literature and constructing long-horizon proofs. In this work, we introduce Aletheia, a math research agent that iteratively generates, verifies, and revises solutions end-to-end in natural language. Specifically, Aletheia is powered by an advanced version of Gemini Deep Think for challenging reasoning problems, a novel inference-time scaling law that extends beyond Olympiad-level problems, and intensive tool use to navigate the complexities of mathematical research. We demonstrate the capability of Aletheia from Olympiad problems to PhD-level exercises and most notably, through several distinct milestones in AI-assisted mathematics research: (a) a research paper (Feng26) generated by AI without any human intervention in calculating certain structure constants in arithmetic geometry called eigenweights; (b) a research paper (LeeSeo26) demonstrating human-AI collaboration in proving bounds on systems of interacting particles called independent sets; and (c) an extensive semi-autonomous evaluation (Feng et al., 2026a) of 700 open problems on Bloom's Erdos Conjectures database, including autonomous solutions to four open questions. In order to help the public better understand the developments pertaining to AI and mathematics, we suggest quantifying standard levels of autonomy and novelty of AI-assisted results, as well as propose a novel concept of human-AI interaction cards for transparency. We conclude with reflections on human-AI collaboration in mathematics and share all prompts as well as model outputs at https://github.com/google-deepmind/superhuman/tree/main/aletheia.
1. Introduction
Aletheia targets the gap between Olympiad-level problem solving and research mathematics by combining advanced reasoning, iterative verification, literature-oriented tool use, and transparent evaluation of AI contributions.
- Aletheia iteratively generates, verifies, and revises natural-language solutions for research-level mathematics.It combines advanced Gemini Deep Think, inference-time scaling beyond Olympiad problems, and intensive search and browsing.
- The paper reports an AI-generated research paper on eigenweights and a human-AI collaboration proving bounds for independent sets.
- 700 open problems from Bloom’s Erdős Conjectures database were evaluated semi-autonomously, including four autonomous solutions.The evaluation used AI grading and human experts for verification.
- Aletheia also achieved leading performance on FirstProof, a collection of ten research-level mathematics problems.
- The paper proposes standard axes for mathematical significance and AI contribution to communicate AI-generated mathematics more transparently.The proposed taxonomy is intended to contextualize autonomy and novelty without claiming that the autonomous Erdős results are major mathematical advances.
2. The Aletheia agent: From Olympiads to Research-level Mathematics
Aletheia extends reasoning systems from contest mathematics toward research by combining generator-verifier-reviser orchestration, inference-time scaling, and research-oriented tool use. Its benchmark results show strong gains, but research-level accuracy remains uneven and citation hallucinations persist in subtler forms.
- Agent design: Aletheia uses Generator, Verifier, and Reviser subagents that interact until approval or a preset attempt limit.The system operates end-to-end in natural language rather than formal language.
- Inference-time scaling: Inference-time compute produced substantial Olympiad accuracy gains before plateauing, while a January 2026 model reduced equivalent IMO-ProofBench compute by approximately 100x.Human experts graded the outputs, and the stronger model solved exceptionally difficult reasoning tasks at extreme scale.
- Benchmark results: Aletheia achieved a 93% overall score on IMO-ProofBench Advanced without tools, with 96% conditional accuracy on the 29 problems it answered.
- Benchmark results: On FutureMath Basic, Aletheia outperformed Deep Think at all tested compute scales, but returned solutions for fewer than 60% of problems.Conditional accuracy on the answered subset exceeded 82%.
- Caveats: The model’s reported IMO results have a knowledge-cutoff caveat because it may have been exposed to IMO 2024 problems.
- Tool use: Tool-use training reduced obvious fictitious citation hallucinations, but shifted errors toward misreporting results from references that actually exist.
3. Summary of Mathematical Research Results
Aletheia produced mathematical research contributions spanning autonomous theorem development, human-AI collaboration, and evaluation on Erdős problems, while the authors distinguish technical correctness from novelty and human accountability.
- Autonomous research: Aletheia-generated Feng26 resolved eigenweight questions in arithmetic geometry without human intervention, using techniques unfamiliar to the original authors.The paper states that all mathematical content of Feng26 was fully generated by AI.
- Human-AI collaboration: Aletheia contributed high-level strategies to LeeSeo26, while human authors supplied rigorous execution in a reversed human-AI workflow.The agent suggested using specific dual sets for a deep result, leaving human authors to complete the proof.
- Erdős problems: 63 solutions were technically correct, but only 13 correctly addressed the intended Erdős problem statements.The remaining technically correct solutions were often mathematically vacuous because the statements were interpreted without capturing Erdős’s intent.
- Erdős problems: Aletheia found four autonomous Erdős solutions, but experts judged none individually to reach research-paper level.The four solutions were Erdős-652, Erdős-654, Erdős-1040, and Erdős-1051; Erdős-1051 was later generalized collaboratively into BKKKZ26.
- Erdős problems: The Erdős classification is at best an upper bound on novelty because earlier human solutions may have been missed during literature review.The authors state that the categories may be revised after further public investigation.
- Additional contribution: Aletheia independently devised an argument using Siegel’s Lemma that achieved the best bound among human and autonomous attempts for Robust MDPs.The argument significantly improved Pagano’s original bound and was adopted for the eventual publication.
4. FirstProof
FirstProof provides a relatively clean comparison setting for research-capable mathematics agents, although research problems remain difficult to retest after solutions enter the literature. Aletheia was evaluated through two runs and expert assessment, with its results contextualized against other systems and prior claims.
- Evaluation setting: Research problems are effectively single-use benchmarks because public solutions can contaminate later evaluations by internet-equipped AI systems.FirstProof was introduced as a rare opportunity for a clean comparison because its ten problems were curated specifically to assess AI mathematical capability.
- Evaluation setting: FirstProof’s ten research-level problems were sampled from active mathematicians’ question distribution and assembled by academics without AI-company connections.These design choices were presented as strengths of the benchmark.
- Results: Aletheia achieved a leading performance on FirstProof, a collection of ten research-level mathematics problems.The paper identifies FirstProof as an assessment of current AI capabilities proposed by academic mathematicians.
- Method: Aletheia was run twice with different Gemini base models, using unmodified FirstProof problem statements and a predetermined verification-and-extraction prompt.The outputs were filtered without intermediate alteration.
- Comparisons: The authors note that other systems solved or claimed solutions to several FirstProof problems, but some claims involved undisclosed human guidance or a flawed solution.They report no credible autonomous solutions beyond the baseline of Problems 9 and 10 aside from the cited instances.
5. Analysis and Discussion
Ablations and evaluations show that Aletheia can outperform or match baseline agents on selected research-level tasks, but success remains inconsistent and publication-grade results are rare.
- Ablation studies: Deep Think correctly solved 8 of 13 Erdős problems while using almost twice Aletheia’s average compute per problem.Both agents used the same base model.
- Ablation studies: On research-paper prompts, Deep Think reproduced some results but failed all Feng26 prompts and the crucial second LeeSeo26 prompt at comparable total compute.It essentially succeeded on BKKKZ26 and produced a less sharp bound for ACGKMP26.
- Weaknesses of AI: The authors caution that autonomous success cases are rare, with no autonomous progress on most research-level benchmark problems.Human-language verification also involves subjectivity.
- Accuracy: 31.5% of 200 evaluated Erdős solutions were technically correct under some interpretation, but only 6.5% were meaningfully correct under the intended interpretation.The 200 candidates were filtered from 700 open problems.
- Accuracy: Aletheia produced candidates for 6 of 10 FirstProof problems, with expert majorities judging all six correct under a publishable-after-minor-revisions standard.Assessment on P8 was not unanimous: 5 of 7 experts rated it Correct.
- Accuracy: Only 1 of 10 FirstProof problems yielded a publication-grade result, and four problems received no solution from either agent.Most FirstProof problems were intended as technical lemmas rather than standalone publication-worthy results.
6. Representing AI contributions to mathematics
The paper proposes documenting AI-assisted mathematics along separate axes for autonomy and mathematical significance, supplemented by interaction records that expose essential AI contributions.
- Motivation: Frontier mathematics is difficult to evaluate because few specialists can assess highly technical work, and correctness alone may not distinguish major advances from trivialities.Research papers may exceed 100 pages and peer review typically exceeds a year.
- Taxonomy: The proposed taxonomy uses separate axes for the degree of AI autonomy and the mathematical significance of the result.The autonomy axis measures relative human and AI contributions, while significance is assessed independently of how the result was produced.
- Levels of Autonomy: The authors classify Feng26 as Level A, LeeSeo26 and BKKKZ26 as Level C, and FYZ26 and ACGKMP26 as Level H.Level A denotes predominantly autonomous work, Level C essential contributions from both humans and AI, and Level H AI contributions that humans could have supplied.
- Levels of Mathematical Significance: The significance scale deliberately remains coarse because mathematical significance is subjective and human research is difficult to compare consistently.Level 2 spans work from very minor to extremely influential, so A2 or C2 does not indicate human-mathematician-level capability.
- Examples: The authors classify their results as A0, A1, A2, C2, or H2, including Erdős solutions at A0/A1 and research papers at A2, C2, or H2.The within-Level-2 range is intentionally broad.
- Interaction Cards: Human-AI interaction cards are proposed as a transparency baseline for documenting AI-assisted mathematics.For Level C or Level A results, the authors suggest exposing the most important raw prompts and outputs containing essential new AI-generated insights.
7. Reflections on the Impact of AI in Mathematics
The authors argue that current AI mathematics results show limited impact overall but reveal comparative advantages that may matter for particular problem types.
- Impact: Current AI results do not indicate that artificial intelligence has matched or will match human mathematicians, despite solving some problems that eluded experts.The authors characterize AI’s impact on pure mathematics research as limited to date.
- Impact: AI may be useful for problems suited to its comparative advantages over humans, rather than as a general replacement for human mathematical ability.The paper presents this as a direction where human researchers may expect near-term impact.
- Comparative strengths: Frontier models combine shallower subject-specific knowledge than experts with superhuman breadth of knowledge, potentially helping unlock certain problems.The paper frames this as a difference between AI and human intelligence.
- Comparative strengths: AI is less constrained by human physical limitations, and its different bottlenecks may be advantageous when open questions require time and attention rather than new techniques.The authors connect this observation to their Erdős-problem results.
8. Related Work
Related work spans advances in mathematical reasoning, existing AI-assisted research applications, and architectures for human-AI collaboration.
- Advances in Mathematical Reasoning: Recent reasoning systems have reached gold-medal standards at the IMO and performed well on difficult benchmarks such as IMO-ProofBench.These advances motivate extending AI evaluation toward research-grade mathematics.
- AI-Assisted Research Results: Prior AI-assisted research includes work on moduli spaces, motivic classes, Nesterov’s method, discrete analysis, convex analysis, and combinatorics.Other studies also examine AI for accessible mathematical problems.
- Frameworks for Human-AI Collaboration: Human-AI collaboration frameworks range from self-verifying agentic architectures to exploration systems and research-assistant interaction protocols.The cited approaches differ in how directly they structure collaboration between humans and AI.
9. Conclusion
The work positions AI as a tool to enhance mathematicians, while presenting Aletheia as a specialized agent for mathematical reasoning and verification. Its evaluation includes advanced exercises, though Gemini 3 Deep Think made negligible progress on one example.
- Aletheia incorporates informal natural-language verification to help address current language-model reliability problems.The authors contrast this with formal systems that generally cannot formulate questions on most research frontiers.
- The authors envision AI enhancing rather than replacing mathematicians.
- Aletheia was evaluated on an internally curated benchmark of advanced Ph.D.-level exercises.
- Gemini 3 Deep Think made negligible progress on one FutureMath Basic problem example.
Large Deviation Analysis of the Phase Transition in the Mean-Field Potts Model
The analysis reduces the mean-field Potts model’s free-energy optimization to a one-dimensional problem and identifies the exact threshold for symmetry breaking. Below the threshold the uniform distribution is optimal; above it, a non-uniform state has greater free energy.
- Large-deviation reduction: The free-energy density is obtained by applying Sanov’s Theorem and Varadhan’s Lemma to the empirical measure.This converts the asymptotic problem into maximizing energy minus entropy over the probability simplex.
- Critical-point structure: Critical points have at most two distinct component values, and local-maximizer analysis leaves the uniform state and one-large-component distributions as global candidates.The latter has one component x and q−1 equal components y, with x + (q−1)y = 1.
- Critical inverse temperature: For q≥3, a secondary local maximum eventually overtakes the uniform state, producing a first-order phase transition at βmax.The threshold is defined where the secondary peak matches the uniform state’s height.
- Critical inverse temperature: The algebraic system has the unique non-trivial solution x_c = (q−1)/q in (1/q, 1].
- Phase-transition regime: For β≤βmax, the uniform distribution globally maximizes Fβ and the limiting free-energy density is β/(2q) + log q.
- Phase-transition regime: For β>βmax, a non-uniform configuration has strictly larger free energy, so the stated equality fails.
- AI-assisted solution: Aletheia solved this FutureMath Basic problem using the search tool, whereas Gemini Deep Think made little progress.
Large Deviation Analysis of the Phase Transition in the Mean-Field Potts Model
The analysis converts the Potts-model free-energy problem into optimization over empirical distributions, then reduces the maximization to a one-dimensional symmetric family. It identifies the exact critical point separating uniform and non-uniform phases.
- Reduction to free-energy optimization: Large deviation theory and Varadhan’s Lemma express the asymptotic free energy density as a supremum of energy minus entropy over the probability simplex.The energy depends on the empirical measure, whose large deviations have rate function given by negative Shannon entropy.
- Critical-point structure: Strict convexity of f(z)=βz−log z implies that any interior critical point has at most two distinct coordinate values.The stationarity condition is βp_k−log p_k−1=λ for every coordinate.
- Critical-point structure: Hessian stability restricts non-uniform local maxima to distributions with one large component and q−1 equal small components, up to permutation.The candidate has the form p=(x,y,…,y) with x+(q−1)y=1.
- Critical temperature: The critical inverse temperature is obtained by equating the non-uniform stationary peak with the uniform state after solving the resulting algebraic system.The unique non-trivial solution satisfies x_c=(q−1)/q in the interval (1/q,1].
- Phase-transition conclusion: For β≤β_max, the uniform distribution globally maximizes the free-energy functional; for β>β_max, a non-uniform configuration has strictly larger free energy.The latter regime marks the first-order phase transition and invalidates the uniform-distribution equality.
2. The Optimal Tiling Construction
The construction attains the theoretical lower bound of 2112 tiles for the 2025×2025 grid. It uses a 45×45 macro-block pattern whose hole permutation simultaneously controls increasing and decreasing subsequences.
- The Optimal Tiling Construction: 2112 tiles are achieved by a symmetric macro-block arrangement with both subsequence lengths restricted to 45.The construction uses k=45 and places one uncovered hole in each macro-block.
- The Optimal Tiling Construction: The cyclically shifted hole pattern guarantees exactly one uncovered square in every absolute row and column.Its interlaced structure creates unbroken orthogonal channels of free space.
- The Optimal Tiling Construction: The remaining squares partition into exactly 2112 non-overlapping rectangles, including 1936 central 45×45 tiles.The central tiles occupy the spaces between diagonal hole chains.
- Proof refinement: The initial model solution found the correct construction but received only a partial unofficial score because it relied on unproved advanced results.A subsequent prompt required elementary, self-contained Olympiad reasoning.
- Theoretical Lower Bound: A corner-counting identity relates the tile count to internal horizontal segments, vertical segments, crossings, and the number of holes.The formula is T=H+V+I+1−N.
4. The Optimal Construction
The sequence problem is analyzed as a deterministic finite-state dynamical system. After separating recurring from transient values, the argument proves that one gender’s sequence eventually becomes periodic.
- 4. The Optimal Construction: The combined sequence simplifies the recurrence: every term after the N-th equals the current occurrence count of the immediately preceding term.Boys’ and girls’ sequences are the odd- and even-indexed subsequences.
- 4. The Optimal Construction: Values larger than M_0 occur at most M_0 times, so the set S of values appearing infinitely often is finite and non-empty.If S were empty, repeated generation of 1 would yield a contradiction.
- 4. The Optimal Construction: Every sufficiently large value outside S appears exactly L=|S| times, causing the sequence eventually to alternate between S and large values.One gender therefore eventually chooses only from S, while the other chooses values above M_2.
- 4. The Optimal Construction: The proof’s finite-maximum argument requires restricting the relevant values to a finite set before taking the maximum over frequencies.The authors explicitly flag this qualification in a comment.
- 4. The Optimal Construction: The recurring subsequence is represented by occurrence-count vectors whose updates form a self-contained deterministic dynamical system.The next selected element is determined by the rank of the newly incremented value.
- 4. The Optimal Construction: A strictly finite state space forces eventual repetition, so at least one of the boys’ or girls’ sequences is eventually periodic.The state is X_n=(s_{n+1},v_n−min(v_n)1).
D.2. Problem 5: Success at 28 Scale
For the robustified IMO 2024 Problem 5 game, the model derives a lower bound of two unavoidable penalties and a strategy that finishes before a third. The resulting smallest threshold is 3.
- D.2. Problem 5: Success at 28 Scale: The model required inference scale 28 to solve the robustified IMO 2024 Problem 5 variant.The reported solution concerns the game on a 3002×3001 table with 3000 traps.
- 1. Lower Bound: Peter can force at least 2 penalties (n≥3): Peter can force two penalties by placing traps at James’s first visited cells in rows 2 and 3, using distinct columns.After the first teleport, James’s revised path must enter row 3 in a different column.
- 1. Lower Bound: Peter can force at least 2 penalties (n≥3): Therefore James cannot guarantee success with zero or one penalty, implying n≥3.The lower-bound argument establishes n>2.
- 2. Upper Bound: James can guarantee success before 3 penalties: James’s row-by-row safe-probing strategy uses undiscovered columns and stops probing a row immediately after finding its trap.The strategy takes at most one penalty per row while learning trap locations.
- 2. Upper Bound: James can guarantee success before 3 penalties: After the second penalty, James uses the known trap columns to reach the last row without further probing.The drop-to-finish maneuver combines a safe available column with the column of the first penalty.
- Conclusion: The strategy limits James to exactly two penalties, so the smallest valid threshold is 3.The final answer is the least positive integer whose penalty is not reached before completion.