升级版证明助手：用Python和Sympy实现数学命题自动化验证

在最近的一篇博文中，作者讨论了一款概念验证工具，旨在自动验证估计。此后，该工具经过了两次重大升级：首次升级将其转化为能够处理命题逻辑的初级证明助手；第二次则参照 Lean 证明助手的关键设计，使其更加灵活，并借助了 Python 包 sympy 进行符号代数运算。目前，这一工具框架已经稳定，可以进一步扩展以处理更广泛的数学任务。作者最初的目的是自动化或半自动化标量函数渐近估计的证明，但理论上可以通过添加更多策略、新的 sympy 类型和引理来扩展工具功能。 该证明助手的最新版本可以在这里找到。作者在开发过程中大量依赖大型语言模型的帮助，特别是 GitHub Copilot 的补全功能。尽管工具支持完全自动化的证明，但目前主要关注的是在人类用户的指导下进行半自动的交互式证明。用户可以在 Python 交互模式下逐条输入命令使用这一工具（作者提到这与文本冒险游戏的界面类似，不过图形用户界面也在考虑之中）。 通过加载预设练习，用户可以启动证明助手并开始验证各种数学问题。例如，有一个练习要求证明当 x、y 和 z 是正实数，且满足 x < 2y 和 y < 3z + 1 时，是否可以推出 x < 7z + 2。使用 Linarith() 策略，工具可以直接完成证明： ``` from main import * p = linarith_exercise() Starting proof. Current proof state: x: pos_real y: pos_real z: pos_real h1: x < 2y h2: y < 3z + 1 |- x < 7*z + 2 p.use(Linarith()) Goal solved by linear arithmetic! Proof complete! ``` 对于需要更多信息的情况，可以使用带有详细标志的 Linarith 策略查看具体步骤。证明过程会通过列出一系列不等式并检查其不可行性来完成。例如，在分解假设置后，一个更复杂的案例证明如下： ``` 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! ``` 此外，工具还支持渐近估计。作者在 sympy 中实现了上一篇博文中的量级形式化方法，并定义了如 (X \lesssim Y) 这样的渐近估计。通过一种对数形式的线性算术，工具可以自动验证某些渐近估计。例如，给定正值 x 和 y 满足 (x \leq 2N^2) 和 (y < 3N)，目标是证明 ( \Theta(x)\Theta(y) \leq \Theta(N)^4 )： ``` p = loglinarith_exercise() Starting proof. Current proof state: N: pos_int x: pos_real y: pos_real h1: x <= 2N2 h2: y < 3N |- 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! ``` 然而，对数线性规划求解器目前尚无法很好地处理“最大”类型表达式。例如，当需要验证 ( x \leq 2N^2 + 1 ) 和 ( y < 3N + 4 ) 是否能推出 ( \Theta(x)\Theta(y) \leq \Theta(N)^3 ) 时，工具无法一次性解决问题，因为当前的 LogLinarith() 未能正确处理这些非线性关系。为此，作者计划开发一个更强大的 LogLinarith 版本，通过分裂处理此类项，从而能够一次性解决类似问题。 未来，作者还计划开发一些工具，用于估计符号函数的空间范数，如部署霍尔德不等式和索博列夫嵌入不等式的引理。symPy 框架足够灵活，可以创建更多此类对象类。目前，作者仅有一个示例引理来展示这一框架——算术均值-几何均值引理。 业内专家表示，这款工具的初步成果非常令人鼓舞，它展示了在自动化数学证明领域的巨大潜力。虽然目前还有许多不足之处，但这一框架的灵活性和强大的符号运算能力为未来的扩展提供了坚实的基础。作者是一位经验丰富的科学家，擅长数学和编程，曾在多个项目中展现出创新能力和严谨的科研态度。他对这一工具的持续改进持开放态度，并期待来自社区的更多建议和贡献。