用于验证估计的工具，II：一个灵活的 Proof Assistant

在最近的一篇文章中，我谈到了一个自动验证估计的 proof of concept tool。自那篇文章之后，我对该工具进行了两次重大改进：首先将其转变为一个可以处理部分命题逻辑的简易 Proof Assistant；其次将其改造成一个更加灵活的 Proof Assistant (刻意模仿了 Lean Proof Assistant 的几个关键方面)，并且由广泛使用的 Python 包 sympy 提供支持，用于符号代数运算，这些都来自于之前评论者的反馈。我认为现在这是一个稳定的框架，可以进一步扩展该工具；我最初的目标只是自动化（或半自动化）涉及标量函数的渐近估计证明，但原则上，我们可以不断地向工具中添加策略 (tactics)、新的 sympy 类型和引理，从而处理非常广泛的其他数学任务。

当前版本的 Proof Assistant 可以在这里找到。（与我之前的编码工作一样，我最终严重依赖大型语言模型来理解 Python 和 sympy 的一些更精细的点，其中 GitHub Copilot 的自动补全功能特别有用。）虽然该工具可以支持完全自动化的证明，但我目前决定更多地关注半自动化的交互式证明，即人类用户提供高级的 "tactics"，然后 Proof Assistant 执行必要的计算，直到证明完成。

通过示例来解释 Proof Assistant 的工作原理是最容易的。目前，我已经实现了在 Python 的 交互模式 中使用该助手，在这种模式下，用户一次输入一个 Python 命令。（我这一代的读者可能熟悉文本冒险游戏，它们具有大致相似的界面。）我对开发该工具的图形用户界面很感兴趣，但对于原型设计目的而言，Python 交互式版本就足够了。（当然，也可以在 Python 脚本中运行 Proof Assistant。）

下载相关文件后，可以通过输入 from main import * 并在 Python 中加载预先制作的练习来启动 Proof Assistant。这是一个这样的练习：

>>> from main import *
>>> p = linarith_exercise()
Starting proof. Current proof state:
x: pos_real
y: pos_real
z: pos_real
h1: x < 2*y
h2: y < 3*z + 1
|- x < 7*z + 2

这是 Proof Assistant 对以下问题的形式化：如果 x,y,z 是正实数，并且 x < 2y 并且 y < 3z+1，证明 x < 7z+2。

Proof Assistant 的工作方式是，引导助手使用各种 "tactics" 来简化问题，直到问题得到解决。在这种情况下，该问题可以通过线性算术来解决，如 Linarith() tactic 所形式化的那样：

>>> p.use(Linarith())
Goal solved by linear arithmetic!
Proof complete!

如果想要了解更多关于线性算术如何工作的细节，可以运行带有 verbose 标志的 tactic：

>>> p.use(Linarith(verbose=true))
Checking feasibility of the following inequalities:
1*z > 0
1*x + -7*z >= 2
1*y + -3*z < 1
1*y > 0
1*x > 0
1*x + -2*y < 0
Infeasible by summing the following:
1*z > 0 multiplied by 1/4
1*x + -7*z >= 2 multiplied by 1/4
1*y + -3*z < 1 multiplied by -1/2
1*x + -2*y < 0 multiplied by -1/4
Goal solved by linear arithmetic!
Proof complete!

有时，证明涉及情况拆分 (case splitting)，那么最终的证明具有树的结构。这是一个例子，其中任务是证明假设 (x>-1) \wedge (x<1) 和 (y>-2) \wedge (y<2) 蕴含 (x+y>-3) \wedge (x+y<3)：

>>> from main import *
>>> p = split_exercise()
Starting proof. Current proof state:
x: real
y: real
h1: (x > -1) & (x < 1)
h2: (y > -2) & (y < 2)
|- (x + y > -3) & (x + y < 3)
>>> p.use(SplitHyp("h1"))
Decomposing h1: (x > -1) & (x < 1) into components x > -1, x < 1.
1 goal remaining.
>>> p.use(SplitHyp("h2"))
Decomposing h2: (y > -2) & (y < 2) into components y > -2, y < 2.
1 goal remaining.
>>> p.use(SplitGoal())
Split into conjunctions: x + y > -3, x + y < 3
2 goals remaining.
>>> p.use(Linarith())
Goal solved by linear arithmetic!
1 goal remaining.
>>> p.use(Linarith())
Goal solved by linear arithmetic!
Proof complete!
>>> print(p.proof())
example (x: real) (y: real) (h1: (x > -1) & (x < 1)) (h2: (y > -2) & (y < 2)): (x + y > -3) & (x + y < 3) := by
 split_hyp h1
 split_hyp h2
 split_goal
 . linarith
 linarith

在这里的最后，我们给出了一个 "伪-Lean" 描述，证明中使用了三个 tactics：一个 cases h1 tactic 来对假设 h1 进行情况拆分，然后是两次应用 simp_all tactic，以简化每种情况。

该工具支持渐近估计。我找到了一种方法来实现前一篇文章中的数量级形式主义。事实证明，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)，其属性是如果 n 是一个标准数字，则 Theta(n)=Theta(1)，并使用这个概念来定义渐近估计，例如 X \lesssim Y (实现为 lesssim(X,Y))。然后可以应用对数形式的线性算术来自动验证一些渐近估计。这是一个简单的例子，其中给定一个正整数 N 和正实数 x,y，使得 x \leq 2N^2 并且 y < 3N，任务是得出结论 xy \lesssim N^4：

>>> p = loglinarith_exercise()
Starting proof. Current proof state:
N: pos_int
x: pos_real
y: pos_real
h1: x <= 2*N**2
h2: y < 3*N
|- Theta(x)*Theta(y) <= Theta(N)**4
>>> p.use(LogLinarith(verbose=True))
Checking feasibility of the following inequalities:
Theta(N)**1 >= Theta(1)
Theta(x)**1 * Theta(N)**-2 <= Theta(1)
Theta(y)**1 * Theta(N)**-1 <= Theta(1)
Theta(x)**1 * Theta(y)**1 * Theta(N)**-4 > Theta(1)
Infeasible by multiplying the following:
Theta(N)**1 >= Theta(1) raised to power 1
Theta(x)**1 * Theta(N)**-2 <= Theta(1) raised to power -1
Theta(y)**1 * Theta(N)**-1 <= Theta(1) raised to power -1
Theta(x)**1 * Theta(y)**1 * Theta(N)**-4 > Theta(1) raised to power 1
Proof complete!

对数线性规划求解器还可以通过一种相当暴力的分支方法来处理低阶项：

>>> p = loglinarith_hard_exercise()
Starting proof. Current proof state:
N: pos_int
x: pos_real
y: pos_real
h1: x <= 2*N**2 + 1
h2: y < 3*N + 4
|- Theta(x)*Theta(y) <= Theta(N)**3
>>> p.use(LogLinarith())
Goal solved by log-linear arithmetic!
Proof complete!

我计划开始开发用于估计符号函数函数空间范数的工具，例如创建 tactics 来部署引理，例如 Hölder 不等式和 Sobolev 嵌入不等式。看起来 sympy 框架足够灵活，可以创建用于这些对象的其他对象类。（现在，我只有一个 概念验证引理来说明该框架，即算术平均-几何平均引理。）

我对这个 Proof Assistant 的基本框架感到满意，我很乐意接受关于新功能的进一步建议或贡献，例如通过引入新的数据类型、引理和 tactics，或者通过贡献应该可以通过这样的助手轻松解决，但目前由于缺乏适当的 tactics 和引理而超出其能力的示例问题。