数学 2.0：当 AI 从算得快走向一起猜

一句话定义：Math 2.0（数学 2.0）指数学研究进入这样一个阶段——AI 不再只是替人算数和检查，而是开始参与「提出猜想、寻找证明思路」这些原本被认为只属于人类创造力的环节。这个说法来自数学家陶哲轩对当下趋势的判断。

它是怎么发生的

过去几十年，计算机在数学里的角色很明确：人类把问题想清楚、把路线定好，机器负责把计算跑完。符号计算软件、数值模拟，乃至四色定理那种机器辅助证明，都属于这一类——机器很听话，但它不会替你想「该证什么」。

大语言模型（LLM, Large Language Model）改变了这个分工。它读过的数学文本远超任何个人，于是可以给出一个可能的方向、一个反例、一个跨领域的类比，甚至生成一段看起来完整的证明草稿。

打个比方：以前的数学软件像计算器，你按公式它出数；现在的 AI 像一个反应极快、读得极多、但会一本正经胡说八道的合作者。它递给你一张写满思路的草稿纸，上面既有真金，也有废纸，挑拣的活儿还是你的。数学家的角色，从「亲自搬砖的人」变成「工头加质检员」。

和相邻概念的区别

最容易被混淆的是证明助手（proof assistant），比如 Lean、Coq 这类形式化工具。它只做一件事：你把完整的证明写成它能读的形式，它逐行检查对不对——它不会自己提出定理。而 Math 2.0 里的 AI 会往前多走一步，去「猜」。猜完必须有人验，而验证这一步往往还是要靠形式化工具兜底，因为自然语言里的「看起来对」，在数学上不算数。

对从业者和普通人意味着什么

对数学工作者，写代码、用证明助手、把一个大猜想拆成机器可验证的小块，会逐渐从加分项变成基本功；除了「我会证」，还要「我会和 AI 一起证」。对普通人，最该记住的是可信度问题：AI 抛出的数学结论必须经得起可复查的验证，否则只是听起来很有道理的文字。所以看到「AI 证明了某某猜想」的说法，第一反应应该是问一句：过了形式化验证吗？