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

AIGC动态3周前发布 almosthuman2014

272 0 0

文章摘要

菲尔兹奖得主陶哲轩在五一假期期间发布了一个开源项目，该项目旨在通过大模型的协助，开发一个用于验证涉及任意正参数的估计是否成立的概念验证软件工具。这个工具的核心功能是自动或半自动地证明分析中的估计值，特别是那些涉及渐近估计的不等式，如X≲Y或X≪Y。陶哲轩的这一项目源于他与前博士生Bjoern Bringmann的讨论，他们注意到尽管符号数学软件包在代数、微积分和数值分析等领域已经非常成熟，但在验证渐近估计方面仍缺乏类似的复杂工具。

陶哲轩在博客中详细讨论了更简单的渐近估计情况，即涉及有限数量的正实数，并使用加、乘、除、指数、最小值和最大值等算术运算进行组合。他过去曾希望有一个工具能够自动判断此类估计是否成立，并提供证明或渐近反例。现在，这一心愿通过他开发的概念验证工具得以实现。陶哲轩使用ChatGPT作为AI辅助工具，经过大约四个小时的编程，成功开发出了这个工具。他还在GitHub上公开了与ChatGPT的对话过程，展示了从提出需求到最终实现的详细步骤。

陶哲轩的这一项目不仅展示了AI在数学研究中的潜力，也为未来的数学工具开发提供了新的思路。他建议数学家与专业程序员以协作的方式进行开发，以实现优势互补。陶哲轩的经历表明，大模型在数学研究和工具开发中的应用前景广阔，更多的功能有待进一步探索和开发。通过这一项目，我们可以看到AI在自动化证明和工具开发中的重要作用，以及其在未来数学研究中的潜在价值。