陶哲轩：感谢ChatGPT，4小时独立完成了一个开源项目

主要观点总结

菲尔兹奖得主陶哲轩发布了一项开源项目，该项目是一个概念验证软件工具，用于验证涉及任意正参数的给定估计是否成立。该工具旨在解决在代数、微积分和数值分析等领域中，缺乏验证渐近估计的复杂工具的问题。陶哲轩通过与 Bjoern Bringmann 的讨论，以及使用大模型的协助，成功开发了这个工具。该工具可以处理不等式形式，如弱算术平均 - 几何平均不等式。在整个开发过程中，陶哲轩使用了 AI 工具 ChatGPT 来协助编程。他认为，如果能够适当使用，AI 将在数学研究和许多其他领域发挥重要作用，并建议数学家与专业程序员协作开发此类软件。

关键观点总结

关键观点1: 陶哲轩发布开源项目，用于验证涉及任意正参数的估计。

该项目是一个概念验证软件工具，旨在解决缺乏验证渐近估计的复杂工具的问题。

关键观点2: 该工具可处理不等式形式，如弱算术平均 - 几何平均不等式。

它能够帮助验证在损失不变的情况下，对于任意大的参数都应该成立的不等式。

关键观点3: 陶哲轩使用大模型和ChatGPT的协助进行开发。

他在开发过程中不断提出需求，ChatGPT 给予回答并协助完成编程。

关键观点4: 陶哲轩认为 AI 在数学研究和许多其他领域具有重要作用。

他建议数学家与专业程序员协作开发此类软件，并强调自动化工具的重要性。

正文

请到「今天看啥」查看全文

「我过去曾希望能有一个工具能够自动判断此类估计是否成立（如果成立，则提供证明；如果不成立，则提供渐近反例）。」

现在，这个心愿实现了。

我们都知道，陶哲轩非常爱好使用大模型来辅助解决数学问题。过去的大多数情况是完成比较简单的编码任务，例如计算然后绘制一些稍微复杂的数学函数，或者对某些数据集进行一些基本的数据分析。

这次，他决定给自己一个更具挑战性的任务：编写一个可以处理上述形式不等式的验证器。

举个例子，一个典型的不等式可能是弱算术平均 - 几何平均不等式。

其中 abc 是任意正实数，这里的 表示我们愿意在估计中丢失一个未指定的（乘性）常数。

原则上，这类形式的简单不等式可以通过强力的案例拆分自动解决。单个这类的不等式都不太难手工求解，但有些应用需要检验大量这样的不等式，或者将其拆分成大量案例。这项任务似乎非常适合自动化，尤其是在现代技术的帮助下。

请到「今天看啥」查看全文