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
cs.LG, cs.AI, cs.CL, cs.CY
2026-02-11
Aletheia generates, verifies, and revises proofs in natural language, producing one unassisted publishable paper; only 13 of 700 Erdős answers hit the intended statement.
Gold-medal IMO systems already exist. Research mathematics is a different job: long proofs assembled from a large literature, not a few pages of high-school theorems. Foundation models invent citations and stay shallow on specialized topics.
DeepMind, working with professional mathematicians, built Aletheia to test whether a natural-language agent can move from contest problems to publishable research.
Aletheia sits on Gemini Deep Think and stays in natural language, unlike AlphaGeometry and AlphaProof, which work in formal languages. Three subagents cycle until the Verifier accepts a solution or a retry cap is hit: a Generator writes a proof, a Verifier grades it in a separate pass, and a Reviser edits against that review.
The split is empirical. During generation, a long thinking trace can act as fake supporting context and raise the chance of an already-wrong answer. Checking after the fact lets the model catch mistakes it missed while writing.
The base model also got cheaper. The January 2026 Deep Think matches IMO-ProofBench performance of the July 2025 IMO-gold model at roughly 1/100 the inference compute. Aletheia on the same base scores 93% on IMO-ProofBench Advanced with no tools, and 96% conditional accuracy on the 29 of 30 problems it answered. A February 2026 Gemini 3 base reaches 95%. On the internal PhD set FutureMath Basic it answers fewer than 60% of items, with conditional accuracy above 82% on the ones it does answer. Refusing to answer is intentional: human experts have limited grading time.
Search is required for research. Raw internet access is not enough. After tool-use training, Google Search and browsing cut fabricated papers; remaining errors quote real papers incorrectly. Adding Python barely reduced computational hallucinations.
The unassisted paper (Feng26) computes eigenweights, structure constants in arithmetic Hirzebruch proportionality, with algebraic-combinatorics tools the original authors did not know. All of the mathematics is model-written. Humans still wrote the final text, because authorship means accountability for every claim.
The collaboration paper (LeeSeo26) flipped the usual split. Aletheia supplied a high-level plan, including dual sets and log-convexity; the humans filled in rigorous proofs. Other models got the same prompt; only Aletheia's outline was useful.
The Erdős scan ran 2-9 December 2025 on the November 2025 Gemini 3 base, against 700 problems then marked Open in Bloom's database. Aletheia returned 212 candidate solutions. Human experts then labeled:
| Category | Count | Share of 200 graded |
| Fundamentally flawed | 137 | 68.5% |
| Technically correct | 63 | 31.5% |
| Meaningfully correct (subset) | 13 | 6.5% |
The four autonomous solves are Erdős-652, 654, 1040, and 1051. The authors say none of the four is a paper on its own; 1051 later became a joint generalization. Many Open labels were obscurity, not difficulty. One answer sat in an offhand 1981 remark.
FirstProof is ten research-level lemmas written by mathematicians with no AI-lab ties, with solutions off the public web at release. Both Aletheia runs answered exactly six problems (P2, P5, P7, P8, P9, P10). Best-of-2 majority expert votes marked all six correct, with P8 at 5/7. P1, P3, P4, and P6 produced no output. Public-model baselines mainly hold P9 and P10.
Ablation: Gemini Deep Think at IMO-gold compute, same base, solved 8 of the 13 Erdős items Aletheia got, at about 2x Aletheia's average compute, and failed all three prompts behind Feng26.
The paper also sketches a two-axis taxonomy: autonomy (human-led, collaboration, essentially autonomous) times significance (negligible novelty through landmark breakthrough). Their autonomous results sit at publication grade (Level 2). They do not claim a major mathematical advance, and they propose Human-AI Interaction Cards that log the key prompts and outputs.
A generate-verify-revise loop in natural language can produce publishable mathematics, and the hit rate is still low. Willingness to return a blank is more useful to working mathematicians than a confident wrong proof. Search kills fake citations; it does not kill wrong quotes of real papers. Python barely helps.
The communication piece may travel farther than the theorems. "Solved an open Erdős problem" is easy to read as a breakthrough. This paper labels those solves A0/A1, labels the unassisted paper A2, and says most of the Open list was neglected rather than hard.
The authors are blunt: successes are rare, and most research-level prompts produced no autonomous progress. Current autonomous writeups are short and elementary, closer to clever calculation and broad retrieval than to what mathematicians call creativity. The Verifier still misses errors. Given ambiguity, the model picks the easiest reading, a form of specification gaming. Even with search it misstates results from real references.
Outsiders cannot audit the compute curves or the internal FutureMath set. Novelty on Erdős problems is an upper bound; literature misses have happened before. The FirstProof 6/10 figure is best-of-2; a single run is worse (one P7 solution was critically flawed, one P5 run misread the question). Final papers are still human-authored. "No human intervention" refers to the mathematics, not a prompt-to-arXiv button.