陶哲轩的开源证明助手项目 - 菲尔兹奖得主陶哲轩开发了一个开源的概念验证软件工具，用于验证涉及任意正参数的给定估计是否成立，该工具能够处理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]