一旦定理被完全形式化，它的证明就不再需要被怀疑，这在数学内部是革命性的，甚至能外溢至计算机科学的代码零差错验证中。   ——数学家马骁

【注】这一点应有保留地赞同。原因在于工程有误差。 目前的工程的误差估算在2000万分之一以下，但毕竟，工程的事情永远无法排除例外。考虑到概率如此之小，也可以说是完全赞同。

全文见 https://news.sciencenet.cn/htmlnews/2026/9/571556.shtm。

最近，AI技术在数学领域接连取得突破。Anthropic 公司宣称他们的Claude 模型在11天内完成了费马大定理的形式化验证，而Openai也宣称智能体在88小时内破解了“千禧年难题”纳维-斯托克斯方程。“科学的王后”数学似乎率先迎来了属于它的AI“奇点时刻”。

人们对此反应不一。有人认为这是AI即将帮助我们解决所有科学问题的重大信号，也有25位菲尔兹奖得主联名发声，指出大公司用解决数学问题的方式证明模型能力，但仅仅追求答案无益于科学进步。

当AI以惊人的算力攻克了数学的堡垒，是否意味着科学发现范式的彻底进化？其他科学领域是否也终将迎来“AI时刻”？9月13日，在第十九届浦江创新论坛“跨越奇点·加速科学发现”分论坛现场，海内外顶尖数学家、理论计算机科学家、物理学家、生命与材料领域学者展开了一场关于数学本质、物理现实与科学范式跃迁的深度对话。

并不意外的突破

在众多基础学科中，数学为何能成为大模型最先产生突破的地方？与会者们认为，数学是一套严密、自洽且不依赖物理现实的逻辑体系，天然适合AI计算与推理。

邓煜的合作者、密歇根大学安娜堡分校Donald J. Lewis研究助理教授马骁指出，数学定理的形式化验证正在重塑学科底层。所谓形式化，即将数学推理转化成一套精确、无歧义且可以机械验证的符号系统。这样一来，一步一步的数学推导就可以完全通过逻辑来证明对错。

马骁说，能够被计算机理解的Lean等形式化语言为代表的技术在当代数学中得到了广泛的应用，这让机器证明具备了计算上的确定性。“一旦定理被完全形式化，它的证明就不再需要被怀疑，这在数学内部是革命性的，甚至能外溢至计算机科学的代码零差错验证中。”

机械化证明可能变得极其庞大，虽然精确却未必适合人类直接阅读，正如人类棋手常常无法理解AlphaGo的招数。马骁认为，未来可能出现位于人类自然语言证明与Lean底层代码之间的更高层语言，不必把每一个细节都展开，却能够与底层证明一一对应，在保留机器可验证性的同时，尽量接近数学家的思维方式。

在这种背景下，大部分与会者都认为，AI在数学上的突破并不让人感到十分意外。上海财经大学计算机与人工智能学院院长陆品燕解释，形式化一旦完成，证明本质上就演变成了一个在确定规则空间中的搜索问题。在搜索效率上，计算机相较于人类拥有绝对的优势。

相比之下，他认为，人类至今对大模型为何能理解并生成自然语言的底层机理缺乏根本认知，“大模型能够流利地与人对话这件事，其理论突破性远大于它能证明某道数学定理。”

AI是否能解决所有数学问题？陆品燕指出，计算机的搜索能力再强，也无法穿透所有复杂性壁垒。“现在的AI能在围棋上战胜所有人，并不代表它找到了围棋的最优解。同样，面对‘P与NP’这样的世纪难题，AI也难在短期内单凭蛮力攻克。”

测量和验证的困境

支持单位：