本周二，我们报道了菲尔兹奖得主陶哲轩的一个开源项目 —— 在大模型的协助下编写了一个概念验证软件工具，来验证涉及任意正参数的给定估计是否成立（在常数因子范围内）。
在项目中，他开发了一个用于自动（或半自动）证明分析中估计值的框架。估计值是 X≲Y（在渐近记法中表示 X=O (Y)）或 X≪Y（在渐近符号中表示 X=o (Y)）形式的不等式。
这才几天的时间，这个估计验证工具的 2.0 版本就来了！
陶哲轩对该工具进行了两次全面改进。
首先，他将其改造成一个基础的证明助手（proof assistant），同时能够处理一些命题逻辑；接着，他根据评论者的反馈，将其改造成一个更加灵活的证明助手（在几个关键方面特意模仿了 Lean 证明助手），它也由功能强大的 Python 符号代数包 sympy 提供支持。
陶哲轩认为现在得到了一个稳定的框架，并可以进一步扩展该工具。他最初的目标只是自动化（或半自动化）标量函数渐近估计的证明，但原则上可以继续向该工具添加策略、新的 sympy 类型和引理，以处理范围广泛的其他数学任务。
该证明助手的 2.0 版本已经上传到了 GitHub。同样地，与自己以前的编码一样，陶哲轩最终「严重」依赖大语言模型的帮助来理解 Python 和 sympy 的一些细节，其中 Github Copilot 的自动补全功能尤其有用。
虽然该工具支持全自动证明，但陶哲轩决定现在更多地关注半自动交互式证明，其中人类用户提供高级「策略」，然后证明助手执行必要的计算，直到证明完成。
GitHub 地址：https://github.com/teorth/estimates
根据项目简介，这是一个利用 Python 开发的轻量级证明助手，其功能远逊于 Lean、Isabelle 或 Rocq 等完整证明助手，但希望它能够轻松用于证明一些简短而繁琐的任务，例如验证一个不等式或估计是否由其他不等式或估计推导出来。该助手的一个具体目标是为渐近估计（asymptotic estimates）提供支持。
具体实现过程
下载相关文件后，即可在 Python 中启动证明助手，只需输入「from main import *」并加载一个预先制作的练习即可。以下是其中一个练习：
这是证明助手对以下问题的形式化描述：如果 x, y, z 是正实数，且 x<2y 且 y<3z+1，则证明 x<7z+2。
证明助手的工作方式是：用户指示助手使用各种「策略」来简化问题，直到问题得到解决。在本例中，该问题可以通过线性算法求解，具体形式化为「Linarith ()」策略：
如果有人想更详细地了解线性算法的工作原理，可以使用「verbose」标志（flag）来运行此策略。
有时，证明过程会涉及情况拆分，最终的证明会呈现出树状结构。这里有个例子：其务是证明假设 (x>-1)∧(x<1) 且 (y>-2)∧(y<2) 蕴涵 (x+y>-3)∧(x+y<3)：
这里，根据使用的三种策略对证明进行「伪精益」描述：策略「cases h」 1 对假设「 h1」进行情况拆分，然后在两种情况下分别应用「simp_all」策略来简化。
该工具支持渐近估计。陶哲轩找到了一种在 Sympy 中实现量级形式化的方法。事实证明，Sympy 在某种意义上已经可以原生实现非标准分析：它的符号变量有一个「is_number」标志，基本上对应于非标准分析中「标准」数的概念。
举例而言，数字 3 的「sympy」版本「S (3)」有「S (3).is_number == True」，因此是标准的；而整数变量「n = Symbol (\”n\”, integer=true)」有「n.is_number == False 」，因此是非标准的。
在「sympy」中，他能够构建各种（正）表达式「X」的数量级「Theta (X)」，其属性「 Theta (n)=Theta (1)」如下：如果「n」是标准数，然后使用这个概念来定义渐近估计，例如
