陶哲轩的开源项目 - 菲尔兹奖得主陶哲轩在五一假期发布了一个开源项目，该项目用于验证涉及任意正参数的给定估计是否成立，工具名为「estimates」[1] - 该项目是一个用于自动或半自动证明分析中估计值的框架，主要处理X≲Y或X≪Y形式的不等式[1] 项目背景与动机 - 当前符号数学软件包在代数、微积分等领域已非常发达，但缺乏复杂工具来验证渐近估计，尤其是涉及未知函数或序列的情况[2] - 陶哲轩与Bjoern Bringmann讨论后，决定开发一个工具来解决这一空白，重点处理有限数量正实数的简单渐近估计[2] - 陶哲轩曾希望有一个工具能自动判断估计是否成立并提供证明或反例，现在通过该项目实现了这一目标[3] 技术实现与AI辅助 - 陶哲轩使用ChatGPT作为主要AI工具，经过约4小时编程完成概念验证工具的开发[7] - 项目开发过程中，陶哲轩与ChatGPT进行了多轮对话，涉及Python类操作、符号表达式实现等基础功能[9][13][14] - 陶哲轩举例说明工具的应用场景，如验证弱算术平均-几何平均不等式，并指出此类任务适合自动化处理[5][6] AI在数学研究中的潜力 - 陶哲轩是较早发现AI大模型数学价值的数学家之一，曾预测到2026年AI将成为数学研究等领域值得信赖的合著者[17] - 陶哲轩此前已多次借助AI工具，如用GPT-4解决数学证明题（8种方法中1种成功）并发现论文中的隐藏bug[17] - 陶哲轩建议数学家与专业程序员协作开发此类软件，以实现优势互补[18] 项目意义与启示 - 陶哲轩强调工具的重点在于自动化而非优雅性，证明过程可能不完美但实现了目标[19] - 该项目展示了大模型在数学研究中的潜在功能，更多应用场景有待探索[19]