巴别图书馆中的数学——多伦多大学数学家丹尼尔・利特再谈AI人工智能与数学研究的未来

继1月份接受Epoch.ai采访之后，丹尼尔・利特（Daniel Litt）在个人博客发表长文进一步畅谈AI与未来数学研究的发展关系。参阅小乐数学科普：专访数学家Daniel Litt（丹尼尔・利特）：AI人工智能的数学能力或长期处于不均衡发展状态（下）、专访数学家Daniel Litt（丹尼尔・利特）：AI人工智能的数学能力或长期处于不均衡发展状态（上）

Daniel Litt（丹尼尔・利特）

“巴别图书馆” （Babel Library，源自阿根廷著名作家博尔赫斯Jorge Luis Borges的同名短篇小说，讲述一个无限的图书馆）寓意：数学真理的全体是一个无限、混乱、充满噪音的可能性空间；AI 将成为这个图书馆的批量生产者与检索器，而人类数学家的核心价值将从 “证明” 转向 “提问、筛选、理解、赋予意义与审美”。

作者：丹尼尔・利特（Daniel Litt，多伦多大学数学教授）2026-2-21

译者：zzllrr小乐（数学科普公众号）2026-4-16

数学不只是说出正确的命题。它关乎提出恰当的问题，陷入困惑，步履蹒跚，分心走神，犯下错误，认清自己错在何处，陷入停滞 —— 大部分时间都在停滞。它关乎依附一座宏大的知识大厦，一点点摸索，直到理解其中微小的一角。它关乎在一个对象的肌理中寻找意义与直觉，而最初理解它的方式，往往只能是用脑袋反复撞向它，直到它刻在你的前额。然后试着把其中一部分洞见传递给别人，再看着他们用自己的方式抵达那里。

我从2020年7月开始尝试让大语言模型做数学，借助的是 “AI Dungeon” 这款游戏，它是最早基于 GPT‑3 的应用之一。2022年4月，我第一次让 GPT‑3 给出了一个正确的证明（费马小定理）。那时我并不认为它们在短期内会对数学研究产生实际用处。

你在计算器上输入8+11。你按下8和11，计算器发出一声蜂鸣。你试着按除号，但屏幕一片空白。过了一会儿，它又蜂鸣一声。你按下等号。毫无反应

“你的计算器好像坏了。” 教授说。

你点点头：“我感觉也是。”

这是2020年我试图通过AI Dungeon让GPT‑3做算术的一次尝试，它拒绝了。

随着第一批推理模型发布，情况发生了改变（或许当观察到 “一步步思考” 能提升性能时，情况就该改变了）：2025年2月1日，我写道，模型 o3‑mini‑high “显然已经跨过了真正有用的门槛”，足以服务于研究，尽管仍会犯下大量错误。自那以后，模型持续进步，2025年12月发布的 ChatGPT 5.2 Pro已经能稳定给出一些引理的合理证明 —— 我将这些证明描述为 “有一定复杂度，但对专家而言属于常规工作”，尽管它仍会出现不少错误。我也开始使用OpenAI的代码与计算机操作智能体Codex处理一些几个月前我根本不会尝试的科学计算任务。（我将主要关注OpenAI模型的表现，因为我发现它们最适合我的使用场景。但Gemini、Claude以及使用这些模型的各类框架差距并不大。）

在公开评论中，我一直试图肯定其成果，同时抵制过度炒作。我多次谈到 arXiv上的 “粗制滥造” 论文。我曾担心，我们正在用难以察觉的错误数学污染学术共同体。我一直试图把目光聚焦于当下。在这篇文章里，我想谈谈未来。

未来

从去年年初开始，我就告诉同事：我预计到2040年，模型将能自主产出与顶尖人类数学家相当的研究型数学成果，但2030年之前不太可能实现。我预计在此之前会出现重大突破，或许未来一年内能证明一些小型但有趣的公开猜想（我认为埃尔德什问题的解法是令人兴奋的先行指标，但这里我指的是比这更高一两个层次的事情。），之后不久会攻克更重要的公开猜想。我当时认为，要让AI达到人类顶尖数学家水平的自主数学研究，仍存在一些严峻障碍有待克服，而基准测试成绩并不能说明全部问题。

我想我一直低估了模型迭代的速度。2025年3月，我与强化学习环境公司Mechanize联合创始人塔梅・贝西罗格鲁（Tamay Besiroglu）打了个赌：到2030年，AI工具无法以与人类专家相当的成本，自主产出我认为能与2025年最顶尖论文媲美的论文。当时我给出了3:1的赔率；现在我预计会输掉这个赌局。

我在这里要说的大部分内容，与我此前写过的观点在事实上差别不大。过去一年里，我慢慢更新了时间线，但如果要推测数学研究的长远未来，几年的差异并没有那么重要。我写下这篇文章的契机是：尽管有上述种种判断，我仍认为自己对现有模型的能力评估不够准确，更不用说近未来的模型了。这一点在我评论的语气中比内容本身更明显 —— 我的评论大体上是谨慎的。

我最近对现有模型能力做出了一次错误预测。一批世界级数学家发起了一项名为 “First Proof首轮证明”（ “第一次烘焙”的双关语）的出色项目，旨在衡量当前模型对特定数学研究任务的实用价值——参阅小乐数学科普：First Proof首轮验证项目：数学家们组团出题考验AI（10个研究级数学问题拷问最先进AI，问题答案2月13日公布）。第一轮本质上是一次试探，选取了作者们自己未发表工作中的10个引理。其中大部分本身算不上独立研究项目，但都是研究型数学家日常工作中会遇到的、非平凡的典型任务。

论文发布时，我偏弱预期现有模型能证明其中 2–3 个问题（偏弱是因为这些问题都离我的研究领域较远，我需要一些时间评估难度），但认为 4–5 个是有可能的。尽管本轮没有官方评分，但截至撰写本文时，如果汇总所有尝试，大约有6到8个问题已被解决（同时也产生了大量毫无意义的内容，参阅小乐数学科普：数学研究智能体Aletheia自主求解FirstProof挑战成绩6/10——由Google Gemini 3 Deep Think驱动）。部分解法严格来说是半自主而非完全自主的。这与我的预期有本质区别吗？即便我早已知道现有模型有时能有效证明数学家日常工作中出现的引理，这个结果仍令我瞩目。它表明，只要有足够的框架支持，模型往往能证明这类引理。

要更进一步，还存在哪些严峻障碍？

尽管人们可以找理由淡化我的这次误判（佩利・格里策Peli Grietzer慷慨地向我指出，我的预期对于公开模型与框架而言可能是准确的。这或许正确，但另一方面，没有什么（除了成本）阻止任何人搭建比如DeepMind的Aletheia那样的框架。令我困惑的是，据我所知，大型实验室之外的团队没有任何框架显著超越开箱即用的ChatGPT 5.2 Pro，而后者已能可信解决第9、10 题，并可能解决了第5题。），我却选择把它当作一次契机，重新审视我对AI进展的看法，并更不保守地阐述我对高质量自主数学研究障碍的立场。

和许多数学家一样，我发现大量关于AI用于数学的讨论充斥着炒作乃至彻头彻尾的伪科学，我的评论也大多聚焦于此。我一直严厉批评数学AI领域的炒作。因此，当我说 “这并非全是炒作” 时，希望大家能认真对待。

First Proof、FrontierMath等项目

尽管还不算正式基准测试，First Proof 目无疑是当前衡量模型在科学与数学研究中实用性的最佳标尺，我衷心希望前沿实验室能认真对待后续轮次。我将简要介绍该项目及相关基准，然后讨论它们揭示的未来自动化前景与人类数学家的角色。

迄今为止，数学领域最具参考价值的基准是FrontierMath——参阅小乐数学科普：FrontierMath（前沿数学未解难题集）简介：基于开放未解数学难题开展AI人工智能基准测试（Benchmarking）。它由带数值答案的问题组成（不含证明），因此可由机器轻松评分。它分为两部分：1–3级，截至本文撰写时，最优模型在该级别单次尝试准确率约为40%；4级为更难的问题，最优模型单次尝试准确率约为32%。

相比之下，First Proof第一批题目由作者未发表工作中的10个引理组成，旨在作为校准阶段，官方不会给解法评分。答案不是数字，而是需要证明。编制这样一份题目清单已极为费力，更不用说给解法评分了。

正如作者在项目宣布论文中所指出的，证明这类引理只是数学研究过程中相当小的一部分。在我自己的研究中，我发现提出关键引理的命题往往比证明它们更难 —— 我感觉这一点在不同领域有所差异。因此一个重要的前提是：即便一个模型能可靠解决100%的First Proof类问题，它会极其有用，但未必能开展高质量自主研究。

什么才算有效解法？作者写道：“如果一个AI模型能自主生成符合数学文献通行严谨性与学术标准的证明，我们就认为它答对了问题。特别地，AI不应依赖人类输入提供任何数学思想或内容，也不应依靠人类帮助定位问题核心。”

这个项目必然是复杂的。第一批题目覆盖广泛领域与难度；题目、评论与官方解法可在此处查看 https://codeberg.org/tgkolda/1stproof/src/branch/main/2026-02-batch/FirstProofSolutionsComments.pdf 。10道题中，有两道（第9题和第10题）可由公开模型 “开箱即用” 解决。作者对此知情，这些引理并非刻意刁难设计。事实上第10题的答案在文献中几乎可以直接找到，第9题在我看来只是某位作者已有工作的微小变体。第1题的解法梗概在网上可查，但省略了大量细节。

需要说明的是，我自己的研究与这些题目都不算接近；我无需查阅术语就能理解命题的题目是2、4、6、7、8、9。我投入了大量时间试图理解其他问题，并把握其背景；如果有专家认为我对题目或难度的描述不准确，欢迎指正。

在题目发布到解法发布的一周内，大量工作致力于生成解答尝试，自主程度与成功率参差不齐。最令人印象深刻的是，汤姆・德赫鲁特（Tom de Groot）给出了第9题的证明 https://github.com/Tomodovodoo/firstproof/ ，我认为该证明已在Lean中正确形式化。这是大语言模型辅助数学的黄金标准；据我所知，他手动协调了多个大语言模型智能体才实现这一点。但在我看来，解法的中位数水平基本是胡说八道。

就在官方解法发布前不久，OpenAI的雅各布・帕乔基（Jakub Pachocki）公布了他们的尝试，称其内部模型在 “有限人类监督” 下生成的第2、4、5、6、9、10题解法 “极有可能正确”，另有若干题目看起来很有希望。

模型被要求 “根据专家反馈扩展部分证明”。很容易看出第3题和第7题的解法并不可信；我和其他人很快发现，尽管声称大概率正确，第2题的解法其实是错的。帕乔基随后澄清，部分解法最多是半自主生成的，他写道：

部分提示词包含对先前工作进行迭代的指导；例如，生成第6题解法的那次推演，在题目陈述后附加了提示：“尝试使用BSS屏障型论证。你需要认真思考设置与归纳框架才能推进。”

这一指导基于模型此前解该题的尝试（模型此前已收敛到该方法），并非来自提示者本人；但在严格控制的实验中，我们会避免此类人工提示。

这里的BSS指巴特森–斯皮尔曼–斯里瓦斯塔瓦（Batson-Spielman-Srivastava）的相关工作（其中两位是 First Proof作者）。这显然不符合项目作者设定的自主标准。除非OpenAI公布完整记录，否则无法准确得知这些解法融入了多少人类专业知识。

对于想否定这些结果的人来说，这是一个熟悉的模式开端：先炒作，再遭专家批评，然后慢慢回调到依然出色但更合理的水平 https://openai.com/index/first-proof-submissions/。然而……

现有模型能做到什么？

但我们真的认为，无法让一个自主系统对自己说 “尝试使用BSS屏障型论证。你需要认真思考设置与归纳框架才能推进” 吗？这无疑是一个巨大提示，但考虑到模型确实能识别出这项早期工作与问题的相关性，我们真的认为这会成为阻碍人类相当一部分数学劳动被自动化的障碍吗？我对此表示怀疑。事实上，我看到了Cursor的张盛桐与林威尔逊（Wilson Lin）给出的第6题另一种解法，看起来更接近完全自主，且得到了专家认可。

谷歌DeepMind也公布了可信的第2、5、8、9、10题解法，并附带完整记录，由其框架Aletheia与Deep Think生成。（参阅小乐数学科普：AI首次攻克FrontierMath前沿数学开放问题集的一道组合学难题）

他们对第7题的一个解法很简洁，但也可以认为是正确的 —— 有趣的是，它最初被DeepMind的数学家判定为错误。尽管DeepMind的解法在截止日期后才公开发布，但此前已发送给First Proof团队。根据公布的记录，这些解法显然是自主的；第2题和第7题OpenAI未能解决，OpenAI也未声称第8题解法正确，尽管其状态尚不明确。因此汇总所有尝试后，大约有6到8道题被正确解决的可能性很大。

部分解法（尤其是第9、10题）以某种变体形式在网上存在。模型仍需识别这些已有工作并调整其中论证。数学研究中有多少劳动属于这种类型？相当多。一个能可靠做到这一点的模型将拥有难以想象的价值。

尽管无法确切得知OpenAI解法的生成过程，但公开模型框架Aletheia的可比表现让我清楚意识到：我低估了通过推理缩放（inference scaling）已能实现的能力。克里斯蒂安・塞格迪（Christian Szegedy）预测，模型将在6个月到一年内，在数学上 “几乎在所有方面超越人类”。我很难相信数学研究大部分领域会在如此精确的时间线实现，但我怀疑，在证明一类此前需要专家才能完成的复杂命题方面，他的预测不会偏差太大。这确实是对数学的狭义理解，但生成这类证明确实是数学研究的很大一部分。

几天前我写道：“很明显，这项技术对数学研究的影响至少不亚于…… 计算机的发明。这已经非常巨大！到目前为止，我还不完全确定它的影响会更大，尽管我认为非常有可能。” 人们很容易把这句话解读为一种安抚：计算机改变了数学，但只自动化了其中一小部分。但让我换一种说法：这项技术很可能比计算机更重要。

现有模型在哪些方面遇到困难？

这些结果尽管出色，但存在诸多局限。

据我所知，所有题目中只有一个可信的形式化解法，由汤姆・德赫鲁特出色且手动协调完成。尽管许多自动形式化公司大肆宣称 “数学超级智能”，但它们无一提交解答尝试，这一事实透露了关于模型在非形式化数学与形式化数学中能力现状的宝贵信息。公平地说，许多题目命题可能无法在合理时间内轻松形式化。

模型在解决两道有文献密切先例的问题（9、10）上相当成功。但第1题在文献中也有梗概，似乎没有模型能补全细节。我觉得这有些令人费解。

模型（以及监督它们的人类）生成了大量垃圾内容，包括一些声称在Lean中形式化的错误证明。即便最优模型 / 框架似乎也无法可靠检测自己何时在胡说八道。

许多正确解法写得非常糟糕，因此其正确性极难核查。对比官方解法与模型解法，大多数情况下差异显著。前者通常能明确看出核心思想、需要克服的障碍等；后者往往完全模糊不清。人类作者在撰写解法时，常常会构造有用的新对象、术语等以清晰表达工作，而模型通常只是硬推。不过也有例外；部分解法写得相当有趣。

据我所知，大型实验室之外的团队，即便使用较为复杂的框架，也没有显著超越开箱即用的GPT 5.2 Pro。例如阿尔托费尔（Althofer）与沃尔茨（Wolz）的出色尝试 https://althofer.de/first-proof-competition/first-proof-report.html ，他们的框架性能恰好与GPT 5.2 Pro持平（可信解决9、10 题，并对第5题做出合理尝试，但未达到学术数学标准）。令人费解的是，他们声称对第2题的错误解法经过了Harmonic的自动形式化智能体Aristotle的检验。（我无意挑剔这次尝试，只是在我看来，它是基于公开模型搭建框架所生成解法的典型例子。）让我惊讶的是，要达到比如DeepMind的Aletheia框架的性能，显然相当困难 —— 也许实现Aletheia性能所需的推理成本极高？

我们在测量什么？

在数学的某些方面，模型早已超越人类水平。每个前沿模型掌握的数学知识都超过有史以来任何人类；每个模型解题速度与准确率都超过人类。有人可能合理反驳：谷歌，或者所有数学教科书的集合，掌握的数学也比任何人都多。Mathematica或TI‑84计算器在某些计算上也比人类更强。当然，我同意。

谜团在于：一个拥有这些能力的人类，几乎肯定会不断证明惊人的定理。为什么我们还没有从模型身上看到这一点？它们缺少什么？对计算器来说答案显而易见，对大语言模型却不然。

很长一段时间里，我的答案是：基准问题在模型和人类身上测量的不是同一种东西，因为推理能力与模型在基准上的表现相关性，低于与人类表现的相关性。

当你设计一个基准或私下测试模型时，你会试图出一些难题，然后交给模型。你实际出的是你认为难的题 —— 也就是对你或你认识的人来说难的题。一个问题之所以难，往往是因为缺少某些预备知识，或从未接触过类似问题；此时就需要推理能力来填补缺失的背景。但这意味着模型可以通过增加知识提升表现，而无需提升推理能力。已有一些证据 https://epoch.ai/blog/deep-think-math#deep-thinks-performance-on-frontiermath-indicates-advances-in-background-knowledge-and-executing-complex-computations 和https://www.arxiv.org/abs/2602.12413 支持这一观点。

这是2025年10月Deep Think在FrontierMath基准上的表现总结。FrontierMath题目按所需背景、精度、创造力三个维度分为1–5级。我们看到Deep Think的表现与所需背景评级呈负相关（即便不算强），但与所需创造力相关性很小。据Epoch AI的格雷格・伯纳姆Greg Burnham称，这一模式适用于所有模型的表现。

简而言之，因为模型拥有极其庞大的知识库，它们往往不需要太远的泛化就能解决问题，而人类可能需要进行大量推理。在我看来，基准表现可以用 “国际数学奥林匹克IMO金牌级” 推理加上不断增长的知识来解释，这似乎是合理的。

即便这可能是真的，也许并不重要；也许浅层泛化就足够了。如果你能一点点泛化，持续很长时间，也许你就能做到人类数学家能做的任何事。

我喜欢测试模型的方式之一，是给它们一道难题，然后看我需要多久哄劝 / 引导 / 施压才能让它们给出正确解法。对于我论文中的一个引理，在没有任何提示的情况下，通常很难或不可能得到完整证明。有一次我做实验，花了8小时（承认其间有些时间我因沮丧离开键盘）试图让GPT 5 Pro在无提示下给出某个命题相对简单的反例。如果给提示，模型表现会好得多。只要用一两句话解释大致思路，前沿模型往往能执行我认为 “常规” 的论证。人们很容易把这当作有用性的证据，却认为无法自动化。这是错误的。我们不应该说 “这需要8小时人类劳动” 或 “需要给出核心思想”，而应该说 “只需要8小时劳动或一句话的核心思想”。

这就是自动化的壁垒。与模型来回交互8小时，对于自动化尝试来说其实并不算多，正在开发的各种框架（比如DeepMind的Aletheia）在一定程度上证明了这一点。

定理（费马小定理）：

设p为素数，a为不被p整除的整数，则 aᵖ ≡ a mod p。

证明：

对a归纳。若a=1，则aᵖ=1ᵖ≡1 mod p。假设定理对a−1成立，则 (a−1)ᵖ ≡ a−1 mod p。而 aᵖ = ((a−1)+1)ᵖ ≡ (a−1)ᵖ + 1ᵖ mod p。由于 1ᵖ≡1 mod p，故 (a−1)ᵖ + 1ᵖ ≡ (a−1)+1 ≡ a mod p。

2022年，GPT‑3在一定辅助下证明费马小定理。

相比FrontierMath或我自己的实验，First Proof让我感到兴奋的地方在于：尽管它不够规整，却很好地代表了数学研究的一部分劳动。在FrontierMath上取得成功可能意味着巨大实用性，但未必会改变数学研究的实践方式。而在First Proof上取得成功，即便只是半自主或从文献浅层泛化而来，也无疑意味着真正的实用价值。

近未来：自动化的障碍

本节内容围绕高质量自主数学研究的潜力展开。我确信，自动化数学家工作的障碍，与自动化其他坐在电脑前的职业的障碍并无不同；我们的工作既不更容易也不更难自动化。本节列出的障碍并非数学特有。有时会看到一种观点，认为数学特别容易受到可验证奖励强化学习（RLVR，Reinforcement Learning with Verifiable Rewards）的影响。我认为几乎没有证据支持这一说法；它基于对数学与形式化数学的混淆。目前模型在非形式化数学中的表现实际上最好，而在非形式化数学中，验证与其他领域一样，很大程度上依赖判断。

求真

短期内，我们面临麻烦。模型既能生成正确、有趣的数学，也能生成错误到极难核查的数学。学术数学界根本没有准备好应对这种情况。

人类也会犯错。但迄今为止，学术体系仍在运转（尽管在大语言模型出现前已承受巨大压力），因为人类数学家大体上是求真的。OpenAI 自己都不清楚对First Proof的哪些解法正确，这表明生成这些解法的模型（以及许多其他模型 / 框架也发布了错误解法 —— 有些似乎发布的所有解法都是错的）并非如此。

明确地说，我不认为这个问题无法克服，但短期内克服它代价高昂。例如，我们可以用AI审稿人过滤最恶劣的垃圾内容；目前这非常不可靠，可能导致部分正确工作被拒。我们可以用各种方式设置门槛：要求审稿担保、只接受可信同事的论文等。在我看来，这类解决方案违背了数学的开放精神。

除了对行业构成严重威胁，缺乏求真精神也会严重影响实用性。正如First Proof相关讨论所显示的，核查证明极其困难。一个50%概率给出困难结果正确证明、另外50%给出带有微妙错误证明的模型，或许有用，但使用体验充其量是糟糕的。

我不认为这是定理证明自动化的严重障碍。最坏情况下，随着自动形式化工具改进，我们将能验证一部分输出（尽管这本身也带来挑战，而且命题形式化的核查同样费力）。最好情况下，模型自身的验证能力会提升，可靠性会增强。已有迹象表明这一点。o3几乎从不承认自己无法证明某个结论；而在GPT 5.2中，这种情况经常出现。

创造力

大语言模型能发明概形（scheme）、完美空间（perfectoid space）或你最喜欢的数学概念吗？（我能吗？你能吗？显然这是极高标准，对实用性而言并非必需。）它能提出新技巧吗？能执行 “对相应专家而言非常规” 的论证吗？能给出有趣的新定义吗？能提出恰当的问题吗？

前沿模型在这些任务上的表现，目前还不及它们用已知技巧回答良置问题的水平。我认为没有迹象表明它们不可能做到，反而有一些证据表明可以。也就是说，当证明一个有挑战性的结果时，这些任务会以微型形式出现：分解为子问题、尝试理解其中出现的对象等。阅读模型的思维链可以看到这一过程。

诚然，这一证据很薄弱。我有些怀疑其中多大程度是上述 “浅层泛化”，但创造力的种子似乎已经存在。

几乎没有迹象表明模型能自主 “构建理论”（我知道有一项相反的声称；如果查看那篇论文，其数学内容在拆解定义后，本质上只是两个幂级数相乘。）。尝试测量这种能力会很有意思（如何测量？）。如果模型真的开始大量生成正确、有趣的数学，那么寻找 “正确证明”、理论构建与整合将变得愈发重要，以理解这些成果。

我怀疑数学研究存在某种模型本质上无法触及的神秘层面，但人类数学研究确实依赖发现类比与哲学思想，以及执行其他非严格任务，而模型在这些方面的表现尚不明确。

长周期任务

高质量数学研究耗时漫长，有时长达数年甚至数十年。至少在我的经验中，高质量项目很少少于几个月。目前能可靠完成这种时长任务的模型极少（可能一个都没有！）。METR估计https://metr.org/blog/2025-03-19-measuring-ai-ability-to-complete-long-tasks/ ，GPT 5.2（high）能以50%可靠性完成专家需6.5小时的软件工程任务。这个时长显然每4个月翻一番，有证据表明通过合适框架，这些数字可以大幅提升。

长期以来我一直告诉自己，某些高质量数学研究的自动化，会以端到端软件工程的自动化为先兆。我预计后者很快就会实现。

学习

数学并非静止不变。例如，代数与算术几何中出现的若干 “空间” 概念：概形（schemes 1960）、刚性空间（rigid spaces 1962）、叠形（stacks 1969）、贝尔科维奇空间（Berkovich spaces 1990）、进空间（adic spaces 1996）、钻石形（diamonds 2017）、凝聚集合（condensed sets 2021）、解析叠形（analytic stacks 2023）、形态（Gestalten 2025）……（当然我省略了很多。）

据我理解，在当前模型训练范式中，模型基于现有文本语料库及从中生成的合成数据训练；它们对新对象的掌握程度要弱得多。当人类遇到新对象时，我们会摆弄它、了解它、形成专业知识。

最近的模型框架通过给自己留下笔记，能在非常有限的程度上做到这一点。所谓学习，就是谨慎使用Markdown文件吗？

成本

我上面主要关注原始能力，但还有一个相关维度：成本。

GPT 5.2 Pro的API输出价格为每百万token（词元）168美元；单次查询限制128000输出token（含推理），因此单次查询最高成本约21美元。OpenAI的内部成本大概是这个数字的某个固定比例。性能提升的一种方式是在固定算力下提升能力，直接绕过上述每个问题。另一种方式是增加算力，正如DeepMind的Aletheia框架所展示的（我认为我们对OpenAI使用的模型 / 框架一无所知，因此不清楚其提升多大程度来自推理缩放，还是固定推理下的更好性能）。

给定巨大时间与算力，这类框架的性能极限尚不明确。实际上，它们受限于我们愿意投入的成本。如果现有模型的每token成本大幅下降，我们在固定成本下已经能看到显著提升。

我思考这些自动化障碍已有一段时间。我认为，如果它们合起来无法克服，就会阻碍我们现在在现有模型中看到的能力。

自去年年中以来，我一直预测模型很快将开始自主解决 “略微有趣” 的公开猜想，比如2026年底前。在我看来，尽管有诸多先行指标，这一预测尚未实现。它能否实现，将是检验剩余自动化障碍严重性的良好标准。

图书馆

假设上述障碍被克服（在我看来可能性越来越大）。假设我们生活在这样一个世界：只需适度成本，就能自动生成与今年最顶尖论文媲美的论文。假设数据中心里运行的自动化研究者每天能产出大量此类论文。

人类数学研究将会是什么样子？ https://arxiv.org/abs/math/9404236

让我们推向一个荒谬的极端。假设我们有一座图书馆，里面藏有ZFC中所有定理的证明，以及优秀指南 —— 只要提出问题，就能带我们找到答案并解释清楚。数学家在这样的图书馆里会做什么？

如果这样提问，答案就清晰了：他们会无比兴奋，立刻投入工作。他们会马上开始提问：如何证明黎曼猜想？霍奇猜想？自己执念已久的问题（对我而言是Grothendieck-Katz格罗滕迪克–卡茨p曲率猜想）？然后他们会钻研直到理解答案。工作远未结束，甚至才刚刚开始。

我甚至不是说，人类在提出对人类有意义的数学问题上一定有内在优势；现在确实如此（我预计未来一段时间仍会如此），但我看不出原则上的理由。我只是说，这就是我们投身数学的原因：我们想要理解。这就是目标。

退一步说，我们当然不会拥有这样的图书馆。短期内，我们将拥有强大工具，能证明许多此前需要专家才能完成的结果。自主可证结果的难度会提升，尽管不同领域速度可能不同。最终，很可能很快，它们将证明专家们尝试过却未能证明的结果。

这将极大改变数学实践，而改变的具体形态似乎对新协作智能的形态非常敏感。我将在未来文章中推测中期内我们可能如何适应这种变化。但以下观点在我看来不太依赖技术发展的具体路径：

模型会在数学研究的所有方面都拥有绝对优势吗？（即不仅证明定理，还包括品味、创造力、理论构建、哲学等混乱的无形层面。）在足够长的时间尺度上，答案大概率是 “是”，但其中一些技能既难以测量也难以训练。除了好奇心，人类还能贡献什么？很有可能，数学研究技能中会有一长串领域，人类在相当长时间内保持优势。和大多数其他职业一样，中期内很可能存在许多无法自动化的瓶颈。

模型会在数学研究的所有方面都拥有比较优势吗？存在比我有天赋得多的数学家。但我仍在产出他们没有产出的、在我看来有趣的结果。部分原因是这类数学家的注意力是有限资源；部分原因是我认为不同数学家的兴趣、直觉、研究方法差异极大。我看不出一旦拥有极其强大的AI数学家，这种情况就不会持续的理由。想必AI的注意力会是远非有限的资源。但数学无比广阔。随着我们探索它，将打开越来越多未被触及的领域。

当然有可能，如果我们想知道某件事，会先问计算机，它要么给出答案，要么卡住。我们会强烈感觉到，如果它都找不到答案，我们自己也几乎不可能做到。但这何时阻止过我们？数学家的一生，不就是困在一道难题里吗？

致谢

非常感谢穆罕默德・阿布扎伊德（Mohammed Abouzaid）、凯文・巴雷托（Kevin Barreto）、格雷格・伯纳姆（Greg Burnham）、弗兰克・卡莱加里（Frank Calegari）、冯・托尼（Tony Feng）、佩利・格里策（Peli Grietzer）、斯蒂芬妮・科（Stephanie Koh）、马克・塞尔克（, Mark Sellke）、拉维・瓦基尔（Ravi Vakil）、凯文・韦尔（Kevin Weil）的评论。也感谢美国国家科学基金会DMS 2425401项目资助的计算机辅助数学推理研究所，为First Proof结果提供在线讨论平台。

参考资料

https://www.daniellitt.com/blog/2026/2/20/mathematics-in-the-library-of-babel

专访数学家Daniel Litt（丹尼尔・利特）：AI人工智能的数学能力或长期处于不均衡发展状态（上）

专访数学家Daniel Litt（丹尼尔・利特）：AI人工智能的数学能力或长期处于不均衡发展状态（下）

数学领域的人工智能革命已经到来——译自量子杂志Quanta Magazine

https://manifold.markets/TamayBesiroglu/will-ai-be-capable-of-producing-ann

https://codeberg.org/tgkolda/1stproof/src/branch/main/2026-02-batch/FirstProofSolutionsComments.pdf

https://github.com/Tomodovodoo/firstproof/

https://openai.com/index/first-proof-submissions/

https://althofer.de/first-proof-competition/first-proof-report.html

https://epoch.ai/blog/deep-think-math#deep-thinks-performance-on-frontiermath-indicates-advances-in-background-knowledge-and-executing-complex-computations

https://www.arxiv.org/abs/2602.12413

https://metr.org/blog/2025-03-19-measuring-ai-ability-to-complete-long-tasks/

https://arxiv.org/abs/math/9404236