撰文｜董彬北京大学 北京国际数学研究中心教授

撰文｜董彬北京大学 北京国际数学研究中心教授‍

做数学研究有一个基本循环，读论文，从中获得启发或找到工具，用它们解决自己的问题，然后把结果写成论文发表，等待别人来读。影响力在这个循环里自然产生。一篇论文如果真的有用，会被后来的研究者读到、引用、依赖。被引次数、h-index、期刊影响因子，这些指标虽然对象不同，但都把被同行引用作为核心信号之一。[1]

这套体系运转了几十年，问题不少（DORA 和莱顿宣言批评了十几年 [1]），但底层逻辑是通的。人读论文，人引论文，人的阅读行为构成影响力的基础数据。

然后 AI 开始介入这个循环的各个环节。

最初是写作端。AI 帮你润色英文、整理参考文

最初是写作端。AI 帮你润色英文、整理参考文献、画图表，省掉一些机械劳动，但核心的智力工作还是人在做。接下来是阅读端。AI 帮你总结一篇长论文、提取关键结论、在几百篇文献中筛选出可能相关的那十几篇。再往后是方法端。AI 开始参与实验设计、代码生成、数据分析。Nature今年的一项大规模研究分析了 4130 万篇论文，识别出一批 AI-augmented researchers，发现他们的论文数量约为 3 倍、引用量约为 5 倍[2]。但同一研究也提到，科学整体的主题覆盖收缩了 4.63%，不同研究间的交叉承接互动下降22%。个人产出在膨胀，集体视野在收缩。产出加速了，但加速本身并不等于进步。

每一步变化发生的时候，感觉都只是效率的提升，科研的本质没有变。所有学科都面临类似的瓶颈：AI 加速了产出，但验证跟不上。实验科学需要重复实验，临床研究需要多中心试验，这些验证成本无法靠算力压缩。

但数学这边有一条独特的出路。AI 同样在加速数学的产出，而纯数学的证明极难审，一篇论文审一两年是常事。陶哲轩最近谈到，当 AI 让提出候选证明、搜索文献和测试思路的成本下降时，可靠验证和结果审查反而变得更加关键[3]。Buzzard近年来也反复强调，现代数学证明的复杂度已经让传统审稿很难逐步核查每个细节[4]。产出端在膨胀，审核端还是那些疲惫的人类专家。

但数学至少在原则上有一条出路：当命题和证明被准确形式化后， 证明是否成立可以由机器来判定 。真正困难的是形式化命题是否忠实表达了人类原本想证明的数学，但一旦这一步完成，逻辑核查就可以交给机器，人类专家转向检查定义、形式化目标和证明策略。形式化目前覆盖的数学还远不到前沿研究的程度，但边界在快速扩展。我们团队开发的LeanSearch（http://leansearch.net）是Mathlib的语义搜索引擎，团队内部监测显示，调用量在三个月内从日均不到 2000 次增长到超过 10 万次/日[5]。单个工具的增长不等于整体趋势，但至少说明形式化社区的活跃度在快速上升。Scholze 早在 2021 年就说过，“原则上可以在 Lean 中形式化任何你想形式化的东西”[6]。DeepMind 的 AlphaProof已经能在 Lean 4 中找到 IMO 级别问题的形式化证明[7]。 这个趋势预示着未来的一个可能性：AI 提出证明，形式化系统验证，人类在关键节点选择问题和判断方向。

如果这个趋势延续下去，数学论文的产出速度会远

如果这个趋势延续下去，数学论文的产出速度会远超任何人的阅读能力。在许多快速增长的方向里，单靠个人阅读已经越来越难追踪领域进展，研究者不得不借助搜索、推荐、形式化库和 AI agent 来筛选信息。

那个“读论文，获得启发，解决问题，发表论文”的基本循环，中间的每一步都开始由 AI 代劳。而当 AI 代劳到一定程度，我们就需要重新思考“影响力”的含义。

以 Allen Institute for AI 的 Asta 系统为例。Asta 在为用户生成文献综述时引用了哪些学术论文，Allen AI 从去年开始追踪这些数据。半年多下来，累计追踪到近 500 万次引用，覆盖了 207 万篇论文[8]。这些引用没有进入 Google Scholar，没有进入 Web of Science，没有出现在任何一个学者的 h-index 里。在现有的学术评价体系中，它们不存在。但一个 AI 系统在替用户解决问题时，确实检索并显式引用了这些论文，把它们作为回答用户问题的知识来源。Asta 的意义不在于它已经给出了新的评价体系，而在于它第一次让我们看见：AI 系统如何在具体问题中实际调用学术知识。

AI 引用同样存在集中度，头部论文占据了大部分引用。但 AI 的筛选逻辑和人类的不同。人类引用受同行互引、学术政治、声望光环等主观因素影响，在 RAG 型科研 agent 中，排序信号更直接地面向当前问题的相关性和可用性。当然，AI 的训练数据本身继承了人类世界的偏见，英语论文覆盖率远高于其他语言，高被引论文在语料中出现频率更高，一个从未上过 arXiv 的关键引理在 AI 检索中可能完全不可见。AI 不一定复制人类引用网络中的所有旧偏见，但它会引入新的系统性盲区。即便如此，这类调用日志也许提供了一个比传统引用更接近即时使用场景的观察窗口。

回到数学。AI agent 在为你解决问题时

回到数学。AI agent 在为你解决问题时检索了哪些定理、调用了哪些引理、使用了哪些工具，这些调用记录本身就构成了一种新的影响力度量。数学品味是否可以量化？恐怕不能完全量化。品味包含对美感的判断、对深度的直觉、对“什么问题重要”的嗅觉，这些东西很难被任何指标捕获。但品味有一些可观测的切面：一条定理在数学知识网络中连接了多少不同的领域，它作为桥梁的结构性价值，可能比它被几篇论文引用更能反映它对数学整体的贡献。当 AI 系统大规模地在这个知识网络中检索和调用时，这种结构性价值第一次变得可观测了。

在数学中，形式化验证使一部分 AI 调用信号更容易被解释：如果 agent 调用了某个已形式化定理，我们至少知道它在一个经过核查的形式系统中被复用过。其他学科没有这种确定性的正确性判定机制，信号更弱更模糊，但趋势方向一致。当越来越多的研究者通过 AI agent 获取知识，agent 在这个过程中调用了谁的工作，谁就获得了更多关注。不是因为 agent 在主动赋予声望，而是因为在特定任务、语料库和检索策略下，它把某些工作判定为更相关、更可调用；人类看到的，正是这层筛选后的结果。当足够多人的 agent 都检索到了同一篇工作，这篇工作在人类世界的注意力也会自然上升。

由此可以再推一步。借用一个略带科幻色彩的说法， 一个学者在碳基圈（人类世界）的影响力，可能越来越受到其工作在硅基系统中可检索、可调用、可复用程度的影响。 人类获取知识越来越多地通过 AI 过滤，你所看到的成果是你的 agent 在为你解决问题时检索到的，而 agent 检索到的是在硅基世界中被证明有用的东西。碳基圈的声望，反过来由硅基圈的使用频率所塑造。

当 AI 降低了常规问题求解的成本，真正稀缺的不再是"做出来"，而是"值得被用"。对年轻研究者来说，这未必是坏消息。在这套逻辑下，一项工作的能见度越来越取决于它在硅基系统中是否被证明有用，而非作者在碳基圈的资历与位置。陶哲轩最近的判断也指向类似的方向：当 AI 承担了更多常规求解，研究者的核心价值转向选择正确的问题、设计合理的工作流程以及仔细检查结果[9]。"做"的门槛在降低，"被选中"的权重在上升，不管是被人选中，还是被 AI 选中。当然，"被证明有用"本身不容易，但至少游戏规则正在变得更可验证。

这个框架如果成立，还意味着影响力不再只通过正

这个框架如果成立，还意味着影响力不再只通过正式论文这一种载体显现。一段写在 GitHub 上的代码、一条写入形式化数学库的引理、一个可被 AI agent 调用的工具，从未以论文形式发表，但在 AI 系统中的影响力可能远超某些发在顶刊上的论文。Matplotlib 的论文被引用了两万多次，但依赖它的软件包数量曾被统计到接近三十万个量级，实际使用的广度远超引用数字所能反映的[10]。被依赖和被引用之间的巨大鸿沟，软件引用运动推了十年也没能弥合[11]。但在 AI 时代，这个问题也许会以一种意想不到的方式被绕过，至少在 RAG 和工具调用这类场景中，AI 系统对知识的显式调用在工程上更容易被记录，不完全依赖人类作者事后自觉地补上一行引用。

如果被 AI 引用成为一种影响力指标，Goodhart 定律几乎必然会发生，研究者开始优化自己的工作以提高 AI 可见性，而不是追求真正的知识贡献。任何指标一旦成为评估标准就会被博弈，AI 调用量大概也不例外。它最多应被视为一种辅助观察信号，而不应直接变成新的考核指标。

陶哲轩和 Michael Harris 对 AI 在数学中的角色有不同的侧重[12]，陶哲轩看到的是 AI 扩大了数学的产出能力，Harris 担忧的是 AI 可能破坏数学的理解功能。证明了多少定理是一回事，创造了多少数学理解是另一回事。硅基影响力能衡量前者，一条定理被调用了多少次、连接了多少领域，但它能衡量后者吗？一个深刻但难以形式化的洞察，一个改变了一代人思维方式的概念框架，这些东西在 AI 的调用日志里可能完全不可见。但这两件事也许不像表面上那样对立。Scholze 做形式化的初衷是确认正确性，结果却获得了更深的理解。形式化本身可以是通向理解的路径，不一定是理解的对立面。真正的风险不在于工具，而在于用工具的人是否还追问“为什么成立”，还是只满足于“确认成立”。

这些推演是否兑现，取决于接下来五到十年技术和制度的共同演化，没有人有确定答案。

但不管评价体系怎么变，驱动好的研究的东西没变

但不管评价体系怎么变，驱动好的研究的东西没变过，好奇心，对问题本身的兴趣，以及生命中那些属于人的部分。Scholze 当初发起 Liquid Tensor Experiment的形式化，是因为他自己也不确定是否有人真正读懂了那个证明，他想用机器来确认[6]。完成后他说，形式化过程让他“理解了证明实际上为何成立”。这不是为了什么硅基影响力，就是一个数学家对自己证明的诚实。这些东西不在任何 agent 的调用日志里，但它们可能是唯一真正重要的。

注：本文也发布在知乎。

参考文献： [1] DORA (San Francisco Declaration on Research Assessment), 2013. https://sfdora.org ; Hicks, D., Wouters, P., et al. “Bibliometrics: The Leiden Manifesto for research metrics.” Nature, 520, 429–431, 2015. https://www.nature.com/articles/520429a [2] Hao, Q., Xu, F., Li, Y., & Evans, J. “Artificial intelligence tools expand scientists’ impact but contract science’s focus.” Nature, 649, 1237–1243, January 14, 2026. https://doi.org/10.1038/s41586-025-09922-y [3] Tao, T. “AI is ready for primetime in math and theoretical physics.” IPAM 会议暨 OpenAI Academy 博客, March 6, 2026. https://academy.openai.com/public/blogs/terence-tao-ai-is-ready-for-primetime-in-math-and-theoretical-physics-2026-03-06 [4] Buzzard, K. 关于 referees 与形式化验证的观点，参见 Science News, “Math, disrupted: AI can now verify proofs,” 2026. https://www.sciencenews.org/article/math-disrupted-by-ai-verify-proofs ; 及其在 ITP 2019、http://plus.maths.org 等场合的多次公开发言。 [5] LeanSearch 调用量统计（实时前端渲染数据，具体数值以访问时页面或后台日志为准）. https://leansearch.net/stats.html [6] Scholze, P. “Half a year of the Liquid Tensor Experiment: Amazing developments.” Xena Project, June 5, 2021. https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ ; 另见 Hartnett, K. Quanta Magazine, July 28, 2021. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ [7] Hubert, T. et al. “Olympiad-level formal mathematical reasoning with reinforcement learning.” Nature 651, 607–613 (2026). Published online Nov. 12, 2025. https://doi.org/10.1038/s41586-025-09833-y [8] Atmakuri, S., Singh, A., & Downey, D. “Making AI citations count with Asta.” Allen AI Blog, October 8, 2025. https://allenai.org/blog/asta-citations [9] Tao, T. 引述自 Castelvecchi, D. “The job description is changing.” Nature, 653, 16–17, April 27, 2026. https://www.nature.com/articles/d41586-026-01246-9 [10] Hunter, J.D. “Matplotlib: A 2D Graphics Environment.” Computing in Science & Engineering, 9(3), 90–95, 2007. Semantic Scholar 等数据库中引用数会随时间变化，此处只取量级。软件包依赖数据参见 Katz, D.S. & Murray, H. “Citing Software in Scholarly Publishing.” Scholarly Kitchen, January 21, 2021. https://scholarlykitchen.sspnet.org/2021/01/21/guest-post-citing-software-in-scholarly-publishing-to-improve-reproducibility-reuse-and-credit/ [11] Smith, A.M., Katz, D.S., Niemeyer, K.E., et al. “Software Citation Principles.” PeerJ Computer Science, 2:e86, 2016. https://doi.org/10.7717/peerj-cs.86 [12] Harris, M. “Silicon Reckoner” (Substack). https://siliconreckoner.substack.com ; Ithaka S+R. “A Third Transformation? Generative AI and Scholarly Publishing.” 2024.https://sr.ithaka.org/publicati

Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.

撰文｜董彬北京大学 北京国际数学研究中心教授

撰文｜董彬北京大学 北京国际数学研究中心教授‍

做数学研究有一个基本循环，读论文，从中获得启发或找到工具，用它们解决自己的问题，然后把结果写成论文发表，等待别人来读。影响力在这个循环里自然产生。一篇论文如果真的有用，会被后来的研究者读到、引用、依赖。被引次数、h-index、期刊影响因子，这些指标虽然对象不同，但都把被同行引用作为核心信号之一。[1]

这套体系运转了几十年，问题不少（DORA 和莱顿宣言批评了十几年 [1]），但底层逻辑是通的。人读论文，人引论文，人的阅读行为构成影响力的基础数据。

然后 AI 开始介入这个循环的各个环节。

最初是写作端。AI 帮你润色英文、整理参考文

最初是写作端。AI 帮你润色英文、整理参考文献、画图表，省掉一些机械劳动，但核心的智力工作还是人在做。接下来是阅读端。AI 帮你总结一篇长论文、提取关键结论、在几百篇文献中筛选出可能相关的那十几篇。再往后是方法端。AI 开始参与实验设计、代码生成、数据分析。Nature今年的一项大规模研究分析了 4130 万篇论文，识别出一批 AI-augmented researchers，发现他们的论文数量约为 3 倍、引用量约为 5 倍[2]。但同一研究也提到，科学整体的主题覆盖收缩了 4.63%，不同研究间的交叉承接互动下降22%。个人产出在膨胀，集体视野在收缩。产出加速了，但加速本身并不等于进步。

每一步变化发生的时候，感觉都只是效率的提升，科研的本质没有变。所有学科都面临类似的瓶颈：AI 加速了产出，但验证跟不上。实验科学需要重复实验，临床研究需要多中心试验，这些验证成本无法靠算力压缩。

但数学这边有一条独特的出路。AI 同样在加速数学的产出，而纯数学的证明极难审，一篇论文审一两年是常事。陶哲轩最近谈到，当 AI 让提出候选证明、搜索文献和测试思路的成本下降时，可靠验证和结果审查反而变得更加关键[3]。Buzzard近年来也反复强调，现代数学证明的复杂度已经让传统审稿很难逐步核查每个细节[4]。产出端在膨胀，审核端还是那些疲惫的人类专家。

但数学至少在原则上有一条出路：当命题和证明被准确形式化后， 证明是否成立可以由机器来判定 。真正困难的是形式化命题是否忠实表达了人类原本想证明的数学，但一旦这一步完成，逻辑核查就可以交给机器，人类专家转向检查定义、形式化目标和证明策略。形式化目前覆盖的数学还远不到前沿研究的程度，但边界在快速扩展。我们团队开发的LeanSearch（http://leansearch.net）是Mathlib的语义搜索引擎，团队内部监测显示，调用量在三个月内从日均不到 2000 次增长到超过 10 万次/日[5]。单个工具的增长不等于整体趋势，但至少说明形式化社区的活跃度在快速上升。Scholze 早在 2021 年就说过，“原则上可以在 Lean 中形式化任何你想形式化的东西”[6]。DeepMind 的 AlphaProof已经能在 Lean 4 中找到 IMO 级别问题的形式化证明[7]。 这个趋势预示着未来的一个可能性：AI 提出证明，形式化系统验证，人类在关键节点选择问题和判断方向。

如果这个趋势延续下去，数学论文的产出速度会远

如果这个趋势延续下去，数学论文的产出速度会远超任何人的阅读能力。在许多快速增长的方向里，单靠个人阅读已经越来越难追踪领域进展，研究者不得不借助搜索、推荐、形式化库和 AI agent 来筛选信息。

那个“读论文，获得启发，解决问题，发表论文”的基本循环，中间的每一步都开始由 AI 代劳。而当 AI 代劳到一定程度，我们就需要重新思考“影响力”的含义。

以 Allen Institute for AI 的 Asta 系统为例。Asta 在为用户生成文献综述时引用了哪些学术论文，Allen AI 从去年开始追踪这些数据。半年多下来，累计追踪到近 500 万次引用，覆盖了 207 万篇论文[8]。这些引用没有进入 Google Scholar，没有进入 Web of Science，没有出现在任何一个学者的 h-index 里。在现有的学术评价体系中，它们不存在。但一个 AI 系统在替用户解决问题时，确实检索并显式引用了这些论文，把它们作为回答用户问题的知识来源。Asta 的意义不在于它已经给出了新的评价体系，而在于它第一次让我们看见：AI 系统如何在具体问题中实际调用学术知识。

AI 引用同样存在集中度，头部论文占据了大部分引用。但 AI 的筛选逻辑和人类的不同。人类引用受同行互引、学术政治、声望光环等主观因素影响，在 RAG 型科研 agent 中，排序信号更直接地面向当前问题的相关性和可用性。当然，AI 的训练数据本身继承了人类世界的偏见，英语论文覆盖率远高于其他语言，高被引论文在语料中出现频率更高，一个从未上过 arXiv 的关键引理在 AI 检索中可能完全不可见。AI 不一定复制人类引用网络中的所有旧偏见，但它会引入新的系统性盲区。即便如此，这类调用日志也许提供了一个比传统引用更接近即时使用场景的观察窗口。

回到数学。AI agent 在为你解决问题时

回到数学。AI agent 在为你解决问题时检索了哪些定理、调用了哪些引理、使用了哪些工具，这些调用记录本身就构成了一种新的影响力度量。数学品味是否可以量化？恐怕不能完全量化。品味包含对美感的判断、对深度的直觉、对“什么问题重要”的嗅觉，这些东西很难被任何指标捕获。但品味有一些可观测的切面：一条定理在数学知识网络中连接了多少不同的领域，它作为桥梁的结构性价值，可能比它被几篇论文引用更能反映它对数学整体的贡献。当 AI 系统大规模地在这个知识网络中检索和调用时，这种结构性价值第一次变得可观测了。

在数学中，形式化验证使一部分 AI 调用信号更容易被解释：如果 agent 调用了某个已形式化定理，我们至少知道它在一个经过核查的形式系统中被复用过。其他学科没有这种确定性的正确性判定机制，信号更弱更模糊，但趋势方向一致。当越来越多的研究者通过 AI agent 获取知识，agent 在这个过程中调用了谁的工作，谁就获得了更多关注。不是因为 agent 在主动赋予声望，而是因为在特定任务、语料库和检索策略下，它把某些工作判定为更相关、更可调用；人类看到的，正是这层筛选后的结果。当足够多人的 agent 都检索到了同一篇工作，这篇工作在人类世界的注意力也会自然上升。

由此可以再推一步。借用一个略带科幻色彩的说法， 一个学者在碳基圈（人类世界）的影响力，可能越来越受到其工作在硅基系统中可检索、可调用、可复用程度的影响。 人类获取知识越来越多地通过 AI 过滤，你所看到的成果是你的 agent 在为你解决问题时检索到的，而 agent 检索到的是在硅基世界中被证明有用的东西。碳基圈的声望，反过来由硅基圈的使用频率所塑造。

当 AI 降低了常规问题求解的成本，真正稀缺的不再是"做出来"，而是"值得被用"。对年轻研究者来说，这未必是坏消息。在这套逻辑下，一项工作的能见度越来越取决于它在硅基系统中是否被证明有用，而非作者在碳基圈的资历与位置。陶哲轩最近的判断也指向类似的方向：当 AI 承担了更多常规求解，研究者的核心价值转向选择正确的问题、设计合理的工作流程以及仔细检查结果[9]。"做"的门槛在降低，"被选中"的权重在上升，不管是被人选中，还是被 AI 选中。当然，"被证明有用"本身不容易，但至少游戏规则正在变得更可验证。

这个框架如果成立，还意味着影响力不再只通过正

这个框架如果成立，还意味着影响力不再只通过正式论文这一种载体显现。一段写在 GitHub 上的代码、一条写入形式化数学库的引理、一个可被 AI agent 调用的工具，从未以论文形式发表，但在 AI 系统中的影响力可能远超某些发在顶刊上的论文。Matplotlib 的论文被引用了两万多次，但依赖它的软件包数量曾被统计到接近三十万个量级，实际使用的广度远超引用数字所能反映的[10]。被依赖和被引用之间的巨大鸿沟，软件引用运动推了十年也没能弥合[11]。但在 AI 时代，这个问题也许会以一种意想不到的方式被绕过，至少在 RAG 和工具调用这类场景中，AI 系统对知识的显式调用在工程上更容易被记录，不完全依赖人类作者事后自觉地补上一行引用。

如果被 AI 引用成为一种影响力指标，Goodhart 定律几乎必然会发生，研究者开始优化自己的工作以提高 AI 可见性，而不是追求真正的知识贡献。任何指标一旦成为评估标准就会被博弈，AI 调用量大概也不例外。它最多应被视为一种辅助观察信号，而不应直接变成新的考核指标。

陶哲轩和 Michael Harris 对 AI 在数学中的角色有不同的侧重[12]，陶哲轩看到的是 AI 扩大了数学的产出能力，Harris 担忧的是 AI 可能破坏数学的理解功能。证明了多少定理是一回事，创造了多少数学理解是另一回事。硅基影响力能衡量前者，一条定理被调用了多少次、连接了多少领域，但它能衡量后者吗？一个深刻但难以形式化的洞察，一个改变了一代人思维方式的概念框架，这些东西在 AI 的调用日志里可能完全不可见。但这两件事也许不像表面上那样对立。Scholze 做形式化的初衷是确认正确性，结果却获得了更深的理解。形式化本身可以是通向理解的路径，不一定是理解的对立面。真正的风险不在于工具，而在于用工具的人是否还追问“为什么成立”，还是只满足于“确认成立”。

这些推演是否兑现，取决于接下来五到十年技术和制度的共同演化，没有人有确定答案。

但不管评价体系怎么变，驱动好的研究的东西没变

但不管评价体系怎么变，驱动好的研究的东西没变过，好奇心，对问题本身的兴趣，以及生命中那些属于人的部分。Scholze 当初发起 Liquid Tensor Experiment的形式化，是因为他自己也不确定是否有人真正读懂了那个证明，他想用机器来确认[6]。完成后他说，形式化过程让他“理解了证明实际上为何成立”。这不是为了什么硅基影响力，就是一个数学家对自己证明的诚实。这些东西不在任何 agent 的调用日志里，但它们可能是唯一真正重要的。

注：本文也发布在知乎。

参考文献： [1] DORA (San Francisco Declaration on Research Assessment), 2013. https://sfdora.org ; Hicks, D., Wouters, P., et al. “Bibliometrics: The Leiden Manifesto for research metrics.” Nature, 520, 429–431, 2015. https://www.nature.com/articles/520429a [2] Hao, Q., Xu, F., Li, Y., & Evans, J. “Artificial intelligence tools expand scientists’ impact but contract science’s focus.” Nature, 649, 1237–1243, January 14, 2026. https://doi.org/10.1038/s41586-025-09922-y [3] Tao, T. “AI is ready for primetime in math and theoretical physics.” IPAM 会议暨 OpenAI Academy 博客, March 6, 2026. https://academy.openai.com/public/blogs/terence-tao-ai-is-ready-for-primetime-in-math-and-theoretical-physics-2026-03-06 [4] Buzzard, K. 关于 referees 与形式化验证的观点，参见 Science News, “Math, disrupted: AI can now verify proofs,” 2026. https://www.sciencenews.org/article/math-disrupted-by-ai-verify-proofs ; 及其在 ITP 2019、http://plus.maths.org 等场合的多次公开发言。 [5] LeanSearch 调用量统计（实时前端渲染数据，具体数值以访问时页面或后台日志为准）. https://leansearch.net/stats.html [6] Scholze, P. “Half a year of the Liquid Tensor Experiment: Amazing developments.” Xena Project, June 5, 2021. https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ ; 另见 Hartnett, K. Quanta Magazine, July 28, 2021. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ [7] Hubert, T. et al. “Olympiad-level formal mathematical reasoning with reinforcement learning.” Nature 651, 607–613 (2026). Published online Nov. 12, 2025. https://doi.org/10.1038/s41586-025-09833-y [8] Atmakuri, S., Singh, A., & Downey, D. “Making AI citations count with Asta.” Allen AI Blog, October 8, 2025. https://allenai.org/blog/asta-citations [9] Tao, T. 引述自 Castelvecchi, D. “The job description is changing.” Nature, 653, 16–17, April 27, 2026. https://www.nature.com/articles/d41586-026-01246-9 [10] Hunter, J.D. “Matplotlib: A 2D Graphics Environment.” Computing in Science & Engineering, 9(3), 90–95, 2007. Semantic Scholar 等数据库中引用数会随时间变化，此处只取量级。软件包依赖数据参见 Katz, D.S. & Murray, H. “Citing Software in Scholarly Publishing.” Scholarly Kitchen, January 21, 2021. https://scholarlykitchen.sspnet.org/2021/01/21/guest-post-citing-software-in-scholarly-publishing-to-improve-reproducibility-reuse-and-credit/ [11] Smith, A.M., Katz, D.S., Niemeyer, K.E., et al. “Software Citation Principles.” PeerJ Computer Science, 2:e86, 2016. https://doi.org/10.7717/peerj-cs.86 [12] Harris, M. “Silicon Reckoner” (Substack). https://siliconreckoner.substack.com ; Ithaka S+R. “A Third Transformation? Generative AI and Scholarly Publishing.” 2024.https://sr.ithaka.org/publicati

Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.