陶哲轩的开源证明助手项目 - 菲尔兹奖得主陶哲轩开发了一个开源的概念验证软件工具，用于验证涉及任意正参数的给定估计是否成立，该工具能够处理X≲Y或X≪Y形式的不等式[2] - 该工具已升级到2.0版本，改进为一个基础的证明助手，能够处理命题逻辑，并模仿Lean证明助手的功能，由Python符号代数包sympy提供支持[3] - 工具支持全自动证明，但陶哲轩更关注半自动交互式证明，用户提供高级策略，助手执行必要计算直至证明完成[3] 项目技术细节 - 项目使用Python开发，是一个轻量级证明助手，功能逊于Lean等完整证明助手，但适合验证简短而繁琐的任务如不等式或估计推导[5] - 工具支持渐近估计，陶哲轩在Sympy中实现了量级形式化，利用Sympy的「is_number」标志区分标准和非标准数[9] - 工具通过线性算法策略如「Linarith()」简化问题，支持情况拆分和树状证明结构，并能处理低阶项[8][10] 项目应用与扩展 - 陶哲轩计划开发用于估计符号函数的函数空间范数工具，创建策略部署Holder不等式和Sobolev嵌入不等式等引理[11] - 目前工具仅有一个概念验证引理即算术平均-几何平均引理，陶哲轩欢迎贡献新数据类型、引理、策略或示例问题[11] - 工具已上传至GitHub，陶哲轩依赖大语言模型如Github Copilot理解Python和sympy细节[3][5] 数学形式化证明实验 - 陶哲轩尝试利用GitHub Copilot和Lean证明助手半自动形式化一页纸的数学证明，约33分钟完成，依赖工具处理逻辑细节[13][14] - 实验证明AI工具可代劳繁琐推理，让人专注于表达而非合理性，尤其适合结构不强、技术推导为主的证明[16] - 实验暴露了Lean项目协作工具的问题，如blueprint工具不支持多证明版本管理[16]

陶哲轩的开源项目 - 菲尔兹奖得主陶哲轩在五一假期发布了一个开源项目，该项目用于验证涉及任意正参数的给定估计是否成立，工具名为「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]