菲尔兹奖得主用AI编程助手，4小时实现数学证明自动化
菲尔兹奖得主用AI编程助手，4小时实现数学证明自动化
未知变量菲尔兹奖得主陶哲轩：当顶尖数学家遇上 AI 编程助手
这个五一假期，当许多人享受休闲时光时，世界顶尖数学家、菲尔兹奖得主陶哲轩 (Terence Tao) 却投入到了一个有趣的技术项目中。他在社交媒体上宣布，借助大型语言模型 (LLM) 的力量，他成功编写并开源了一个概念验证 (proof-of-concept) 软件工具。
这个工具的核心目标是：验证那些涉及任意正参数的数学估计（Estimate）是否在常数因子范围内成立。
项目地址：https://github.com/teorth/estimates
简单来说，陶哲轩开发的这个框架，旨在实现分析学中常见“估计”不等式的自动化或半自动化证明。这里的“估计”通常指形如 X≲Y（在渐近记法中等价于 X=O(Y)，表示 X 的增长速度不快于 Y 的某个常数倍）或 X≪Y（等价于 X=o(Y)，表示 X 相对于 Y 是无穷小）的不等式。
为何需要这样一个工具？数学研究中的自动化“痛点”
开发这个工具的想法，源于陶哲轩近期与他曾经指导的博士生、现任普林斯顿大学助理教授 Bjoern Bringmann 的一次深入讨论。
他们注意到，虽然现有的符号数学软件包（如 Mathematica, Maple 等）在处理代数运算、微积分和数值分析等任务上已经相当成熟和强大，但在验证渐近估计 (asymptotic estimates) 方面，却缺乏类似的高效工具。这类估计指的是那些在忽略常数因子差异、参数趋于无穷大时应当成立的不等式。尤其对于涉及未知函数或序列（存在于特定函数空间，如 L^p 空间）的函数估计，验证工作往往更加复杂和繁琐。
陶哲轩将这次讨论的思考整理成了一篇博客文章。他特别聚焦于一种相对简单的情况：只涉及有限数量正实数，并通过加、乘、除、指数、取最小/最大值等运算（值得注意的是，不包括减法）组合而成的渐近估计。
他坦言：“我过去一直希望能有一个工具，可以自动判断这类估计是否成立。如果成立，它能提供一个证明；如果不成立，则给出一个渐近反例。”
如今，借助 AI 的力量，这个愿望初步得以实现。
AI 编程伙伴：ChatGPT 助力四小时快速开发
众所周知，陶哲轩是积极拥抱并探索大型语言模型在数学研究中应用的先驱者之一。此前，他主要利用 AI 处理一些相对基础的任务，比如进行复杂的数学函数计算并绘制图形，或是对特定数据集进行初步的数据分析。
这一次，他决定挑战一个更复杂的任务：亲自编写一个能处理前述特定形式不等式的验证器。
让我们来看一个典型的例子，比如“弱算术平均-几何平均不等式”(Weak AM-GM Inequality)：
这里，a, b, c 是任意正实数，而符号 
表示我们允许在估计中忽略一个未指明的（乘性）常数因子。
理论上，这种形式相对简单的不等式可以通过繁琐的“案例拆分”(case splitting) 方法来自动解决。虽然单个不等式的手工证明通常不难，但在某些研究场景下，可能需要检验大量类似的不等式，或者一个不等式需要拆分成极其复杂的多种情况。这种重复性、逻辑性强的工作，似乎天然就适合交给机器自动化处理，尤其是在现代 AI 技术的加持下。
陶哲轩这次选择的 AI 助手依然是他熟悉的 ChatGPT。令人瞩目的是，仅仅花费了大约四个小时的编程时间，在与大模型进行高频次的互动协助下，他就成功构建出了这个概念验证工具。
为了展示这个过程，陶哲轩还大方地分享了他与 ChatGPT 的完整对话记录，从中可以看出，这是一段相当详尽且富有成效的协作：
对话记录链接： https://chatgpt.com/share/68143a97-9424-800e-b43a-ea9690485bd8
对话伊始，陶哲轩清晰地提出了他的需求：“我想编写一些 Python 类来操作符号表达式……希望能有一个表示变量的类，比如 x、y、z……你能帮我写一些基础类来起步吗？”
ChatGPT 仅思考了 6 秒钟，便给出了初步的代码框架。
随后，陶哲轩基于 AI 生成的代码，继续提出具体的技术问题：“我看到你用 __add__ 实现了 + 操作，很棒。那么，实现 * 和 / 的对应方法是什么呢？”
ChatGPT 迅速给出了相应的实现方式：
在整个开发过程中，陶哲轩不断提出各种层级的问题，从核心的类设计、方法实现，到一些具体的编程细节，例如：
“如何在与当前 python 文件相同的目录下导入 python 文件？”
ChatGPT 几乎做到了有问必答，无论是基础概念还是复杂逻辑，都提供了有效的帮助，极大地加速了开发进程。最终，这个概念验证工具在人机协作下顺利诞生。
陶哲轩的 AI 观：从助手到值得信赖的“合著者”
在众多世界级数学家中，陶哲轩可以说是较早认识到并积极探索 ChatGPT 这类 AI 大模型在数学领域潜力的代表人物。他曾做出一个颇为乐观的预测：“如果使用得当，到 2026 年，AI 将成为数学研究以及许多其他领域值得信赖的合著者。”
这并非空谈。陶哲轩本人已多次将 AI 融入其研究工作流：
- 他曾在 GPT-4 的辅助下，成功形式化并解决了一个具有一定挑战性的数学证明问题（据他描述，GPT-4 提出了 8 种潜在方法，其中一种最终奏效）。
- 他还借助 AI 工具，发现了自己一篇论文中一处先前未察觉的隐藏错误 (bug)。
基于这些实践经验，陶哲轩也给出了他的建议：对于开发此类面向数学研究的复杂软件工具，最佳方式或许是数学家与专业程序员紧密协作，实现领域知识与工程能力的优势互补。
正如他对自己这次开发的工具所评价的：“这当然是一个极其不优雅的证明（指工具自动生成的证明过程），但优雅并非重点，重点在于它是自动化的。”
结语：冰山一角，AI 潜能待发掘
回顾陶哲轩的这次尝试，我们可以清晰地看到，即使是对于像他这样的顶尖智慧头脑，AI 也已经能够扮演一个有价值的“编程助手”和“研究伙伴”角色。这不仅展示了大型语言模型在辅助复杂逻辑任务和代码生成方面的能力，更重要的是，它揭示了 AI 在自动化处理繁琐、重复性智力劳动方面的巨大潜力。
陶哲轩与 ChatGPT 的这次合作，或许只是 AI 赋能科学研究的冰山一角。未来，随着技术的不断进步和应用场景的持续探索，AI 在数学乃至更广泛的科研领域中，还将解锁哪些令人惊叹的功能，值得我们共同期待。
参考链接：
