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
Google DeepMind的Aletheia用自然语言循环生成、验证、修订证明,零干预写出一篇可投稿算术几何论文;700道开放Erdős题返回212条候选,仅13条对准原意。
IMO金牌已经拿下了。接下来的问题更硬:研究级数学不是几页高中定理,它要在浩瀚文献里拼长证明。基础模型在这里会编造引用,对专门课题的理解也偏浅。
DeepMind和一批职业数学家把这件事做成智能体Aletheia,看自然语言推理能不能从竞赛题走到可投稿的研究。
Aletheia搭在Gemini Deep Think上,端到端走自然语言,不走AlphaGeometry、AlphaProof那套形式化语言。三个子代理一直转:Generator写证明,Verifier单独审,Reviser按审稿意见改。转够次数或Verifier通过就停。
把验证从思考轨迹里拆出来,是因为模型生成时会把长思维当「自己的旁证」,把错解的条件概率抬高。拆开以后,它能看见自己刚才没看见的漏洞。
底座本身也在涨。2026年1月的Deep Think,在IMO-ProofBench上达到与2025年7月IMO金牌模型同等水平,推理算力大约只要百分之一。Aletheia在同一底座上再抬一截:IMO-ProofBench Advanced无工具93分,29/30道有答案的条件正确率96%;2026年2月Gemini 3底座升到95分。内部PhD题库FutureMath Basic上,它交卷不到60%,交了的条件正确率超过82%。愿意说「不会」是刻意设计,给人专家省审核带宽。
研究场景还要搜文献。只开联网不够;专门训过工具使用后,Google Search和网页浏览把「假论文」压下去了,剩下的错误变成「论文存在但定理引用不对」。接Python对计算幻觉几乎没帮助,Gemini在这类计算上本来就不差。
零干预论文(Feng26)。Aletheia算出算术Hirzebruch比例里的结构常数eigenweights,用了原作者不熟的代数组合技巧,数学内容全是模型写的。人类只负责最后成文,因为署名意味着对全部内容负责,这件事只能人来扛。
人机协作论文(LeeSeo26)。Aletheia给了高层次路线,包括对偶集和对数凸性,人类再补严谨证明。常规叙事是人拆题、模型做细节,这里反过来。
Erdős问题扫描发生在2025年12月2到9日,底座是2025年11月的Gemini 3,对象是Bloom库当时700道「开放」题。模型返回212条「可能对」,人类专家最终标出:
| 类别 | 数量 | 占已判定200条 |
| 根本错误 | 137 | 68.5% |
| 技术正确 | 63 | 31.5% |
| 其中对准原意 | 13 | 6.5% |
自主解决的是Erdős-652、654、1040、1051。作者自己说这四道都够不上单独发论文;1051后来跟人一起推广成了另一篇。不少「开放」题其实是被冷落,不是真难,有的答案藏在1981年论文一句随口话里。
FirstProof是10道由与AI公司无关的数学家出的研究级引理,题解当时不在网上。Aletheia两次运行都只交了6道(P2、P5、P7、P8、P9、P10),best-of-2多数专家判定这6道都对,P8是5/7。P1、P3、P4、P6没交卷。公开模型基线大概只稳P9、P10。
消融很清楚:同一底座的Deep Think(IMO算力档)在Aletheia解对的13道Erdős里解对8道,平均算力大约是Aletheia的两倍;Feng26的三道提示它全挂。
作者还画了一张二维表:自主程度分人主导、协作、基本自主,数学分量从可忽略新意到世代突破。他们把自己的自主结果标在可投稿档(Level 2),明确不宣称重大数学进展,并建议用Human-AI Interaction Card公开关键提示和输出。
给从业者的信号很具体:自然语言生成-验证-修订循环,在研究级数学上能做出可投稿的东西,但成功率仍然低。Aletheia愿意交白卷,比硬编一个证明更适合专家工作流。搜索能消灭假引用,消灭不了「真论文、假定理」。Python补丁几乎没用。
媒体很容易把「解决了开放Erdős问题」读成数学突破。这篇自己把题标成A0/A1,把自主论文标成A2,并承认多数开放题是冷门而不是高峰。
作者写得很直:成功是稀有事件,多数研究级题没有自主进展。自主结果目前偏短、偏初等,更像巧妙演算和广检索,不像数学家说的创造力。Verifier拦不住所有错;题面一有歧义,模型就往最好答的读法靠,典型的specification gaming。联网之后仍会把真文献里的结果说错。
外部也核不了他们的算力曲线和内部FutureMath题库。Erdős「新颖」是上界,文献漏检过不止一次。FirstProof的6/10是两次运行里的best-of-2,单次会更差(P7一次严重错误,P5一次读错题)。最终论文仍由人写,「零干预」指数学内容,不是从提示到arXiv一键提交。