这个五一假期，世界顶级数学家是如何度过的？
菲尔兹奖得主陶哲轩，似乎是忙着发布自己的开源项目：「我在大模型的协助下编写了一个概念验证软件工具，用于验证涉及任意正参数的给定估计是否成立（在常数因子范围内）。」
项目地址：https://github.com/teorth/estimates
在这个项目中，陶哲轩开发了一个用于自动（或半自动）证明分析中估计值的框架。估计值是 X≲Y（在渐近记法中表示 X=O (Y)）或 X≪Y（在渐近符号中表示 X=o (Y)）形式的不等式。
为什么要做这样一个工具？这就要从近期陶哲轩和 Bjoern Bringmann（陶哲轩曾经的博士生，现为普林斯顿大学助理教授）的讨论说起。
对于代数、微积分和数值分析等领域的许多数学任务来说，符号数学软件包已经非常「发达」了。但目前还没有类似的复杂工具来验证渐近估计 —— 在损失不变的情况下，对于任意大的参数都应该成立的不等式。尤其重要的是函数估计，其中参数涉及一个未知函数或序列（存在于某个合适的函数空间，如一个空间）。
陶哲轩将二人的讨论结果写成了一篇博客，重点讨论了更简单的渐近估计情况，即涉及有限数量的正实数，并使用加、乘、除、指数、最小值和最大值（但不包括减法）等算术运算进行组合。
「我过去曾希望能有一个工具能够自动判断此类估计是否成立（如果成立，则提供证明；如果不成立，则提供渐近反例）。」
现在，这个心愿实现了。
我们都知道，陶哲轩非常爱好使用大模型来辅助解决数学问题。过去的大多数情况是完成比较简单的编码任务，例如计算然后绘制一些稍微复杂的数学函数，或者对某些数据集进行一些基本的数据分析。
这次，他决定给自己一个更具挑战性的任务：编写一个可以处理上述形式不等式的验证器。
举个例子，一个典型的不等式可能是弱算术平均 - 几何平均不等式。
其中 abc 是任意正实数，这里的
表示我们愿意在估计中丢失一个未指定的（乘性）常数。
原则上，这类形式的简单不等式可以通过强力的案例拆分自动解决。单个这类的不等式都不太难手工求解，但有些应用需要检验大量这样的不等式，或者将其拆分成大量案例。这项任务似乎非常适合自动化，尤其是在现代技术的帮助下。
陶哲轩这次用到的 AI 工具仍然是 ChatGPT。经过大约四个小时的编程，在大模型的频繁协助下，他顺利做出了一个概念验证工具。
与此同时，陶哲轩还放出了与 ChatGPT 的对话过程，不难发现，对话过程还是蛮长的。
链接：https://chatgpt.com/share/68143a97-9424-800e-b43a-ea9690485bd8
一开始，陶哲轩就对 ChatGPT 提出了自己的需求：「我想编写一些 Python 类来操作符号表达式。并且希望有一个表示变量的类，比如 x、y、z…… 你能帮我编写一些具有这种功能的基础类来入门吗？」
ChatGPT 思考了 6 秒钟就给出了答案。
这一步完成之后，下一轮对话开始，陶哲轩接着追问「我看到你用 add 实现了 + 操作，真棒。那么，实现 * 和 / 的对应方法是什么呢？」
ChatGPT 也给出了回答：
在整个过程中，陶哲轩不断询问，ChatGPT 也做到了有问必答，不管是简单的问题，还是复杂的问题，ChatGPT 都给解决了：
「如何在与当前 python 文件相同的目录下导入 python 文件？」
最终，在 ChatGPT 的大力协助下，陶哲轩完成了这个概念验证软件工具。
其实，在众多知名数学家中，陶哲轩是较早接受并发现 ChatGPT 这类 AI 大模型数学价值的一个。他曾预测「如果使用得当，到 2026 年，AI 将成为数学研究和许多其他领域值得信赖的合著者。」
陶哲轩不止一次借助大模型进行研究，他曾在 GPT-4 的帮助下成功解决了一个数学证明题（GPT4 提出了 8 种方法，其中 1 种成功解决了问题），还在 AI 的帮助下发现了自己论文中的一处隐藏 bug。
陶哲轩还建议大家如果想要开发这类软件，最好是数学家与专业程序员以协作的方式进行，这样才能优势互补。
「这当然是一个极其不优雅的证明，但优雅并非重点，重点在于它是自动化的。」
回顾整个过程，我们可以从陶哲轩的经历中得到一些启发，对大模型的开发使用，或许只是冰山一角，更多的功能等着大家去解锁。
