在尝试 第一版 后，继续对照 5月9日博文「A tool to verify estimates, II: a flexible proof assistant」 提到的例程，对输出进行中文化。使用的是5月14日的源码内容，修改后的代码库 在此。最后是一些个人感受。

第一例 反证不等式

linarith_solution 输出如下：

开始证明。当前情况：
x: pos_real
y: pos_real
z: pos_real
h1: x < 2*y
h2: y < 3*z + 1
求证：x < 7*z + 2
检验以下不等式可否成立：
1*x > 0
1*z > 0
1*y + -3*z < 1
1*x + -7*z >= 2
1*x + -2*y < 0
1*y > 0
以下式子取和，得证不可能成立：
1*z > 0 两边乘 1/4
1*y + -3*z < 1 两边乘 -1/2
1*x + -7*z >= 2 两边乘 1/4
1*x + -2*y < 0 两边乘 -1/4
证明完毕！

对反证法的使用未直接反映在输出中。取和方法与上一版相同。

当前版描述证明目标是这段：

def linarith_exercise() -> ProofAssistant:
    p = ProofAssistant()
    x, y, z = p.vars("pos_real", "x", "y", "z")
    p.assume(x < 2 * y, "h1")
    p.assume(y < 3 * z + 1, "h2")
    p.begin_proof(x < 7 * z + 2)
    return p

对比前一版里这样写：

def 一次不等式():
    inequalities = set()
    inequalities.add(不等式({'x': 1}, 'gt', 0))
    inequalities.add(不等式({'y': 1}, 'gt', 0))
    inequalities.add(不等式({'z': 1}, 'gt', 0))
    inequalities.add(不等式({'x': 1, 'y': -2}, 'lt', 0))
    inequalities.add(不等式({'y': 1, 'z': -3}, 'lt', 1))
    inequalities.add(不等式({'x': 1, 'z': -7}, 'geq', 2))
    verbose_feasibility(inequalities)

直接写不等式使得可读性增加。是改用了与上一版的Variable-Expression等类似功能的SymPy库（Symbol-Basic等）。

求证目标用的是符号 - ，也许是Lean风格。中文化时改为「求证」。

分情况证不等式

split_solution 输出：

开始证明。当前情况：
x: real
y: real
h1: (x > -1) & (x < 1)
h2: (y > -2) & (y < 2)
求证：(x + y > -3) & (x + y < 3)
分情况 h1: (x > -1) & (x < 1) 为 x > -1, x < 1.
尚余一目标。
分情况 h2: (y > -2) & (y < 2) 为 y > -2, y < 2.
尚余一目标。
拆分目标为：x + y > -3, x + y < 3
尚余 2 目标。
目标由 linear arithmetic 求解！
尚余一目标。
目标由 linear arithmetic 求解！
证明完毕！

仅从这个输出看不清每步达成了哪个目标。

渐进不等式

中文化时将输出化为更接近数学公式的表达，如省去 **1 等：

Theta(x)**1 * Theta(N)**-2 <= Theta(1) raised to power -1
=>
𝚹(x) * 𝚹(N)^-2 <= 𝚹(1) 的 -1 次幂

loglinarith_solution 改为 p.use(LogLinarith(verbose=True)) 输出如下：

开始证明。当前情况：
N: pos_int
x: pos_real
y: pos_real
h1: x <= 2*N**2
h2: y < 3*N
求证：𝚹(x)*𝚹(y) <= 𝚹(N)^4
为反证，化为以下渐进不等式：
['𝚹(N) >= 𝚹(1)']
['𝚹(x) * 𝚹(N)^-2 <= 𝚹(1)']
['𝚹(y) * 𝚹(N)^-1 <= 𝚹(1)']
['𝚹(x) * 𝚹(y) * 𝚹(N)^-4 > 𝚹(1)']
检验以下不等式可否成立：
𝚹(N) >= 𝚹(1)
𝚹(x) * 𝚹(N)^-2 <= 𝚹(1)
𝚹(y) * 𝚹(N)^-1 <= 𝚹(1)
𝚹(x) * 𝚹(y) * 𝚹(N)^-4 > 𝚹(1)
以下之积可得矛盾：
𝚹(N) >= 𝚹(1) 的 1 次幂
𝚹(x) * 𝚹(N)^-2 <= 𝚹(1) 的 -1 次幂
𝚹(y) * 𝚹(N)^-1 <= 𝚹(1) 的 -1 次幂
𝚹(x) * 𝚹(y) * 𝚹(N)^-4 > 𝚹(1) 的 1 次幂
证明完毕！

此部分功能与第一版的类似。

继续逼近

目标是在上一例基础上作修改。这里想到，也许可基于这个自动工具的例程生成一些猜想。

loglinarith_hard_solution2 穷举法，输出90行。

比较 loglinarith_hard_solution 输出：

开始证明。当前情况：
N: pos_int
x: pos_real
y: pos_real
h1: x <= 2*N**2 + 1
h2: y < 3*N + 4
求证：𝚹(x)*𝚹(y) <= 𝚹(N)^3
将 h1: x <= 2*N**2 + 1 转化为渐进形式 h1_theta: 𝚹(x) <= Max(𝚹(1), 𝚹(N)^2).
尚余一目标。
将 h2: y < 3*N + 4 转化为渐进形式 h2_theta: 𝚹(y) <= Max(𝚹(1), 𝚹(N)).
尚余一目标。
可断言 𝚹(1) <= 𝚹(N).
尚余 2 目标。
由 log-linear arithmetic 达成目标！
尚余一目标。
可断言 𝚹(1) <= 𝚹(N)^2.
尚余 2 目标。
由 log-linear arithmetic 达成目标！
尚余一目标。
简化 𝚹(x) <= Max(𝚹(1), 𝚹(N)^2) 为 𝚹(x) <= 𝚹(N)^2，由于 𝚹(1) <= 𝚹(N)^2.
简化 𝚹(y) <= Max(𝚹(1), 𝚹(N)) 为 𝚹(y) <= 𝚹(N)，由于 𝚹(1) <= 𝚹(N).
尚余一目标。
由 log-linear arithmetic 达成目标！
证明完毕！

可见在人工指导下的证明过程要简短的多，同时输出可读性仍有很大改进空间。

使用定理

amgm_solution 输出：

开始证明。当前情况：
x: nonneg_real
y: nonneg_real
求证：2*x*y <= x**2 + y**2
用定理 算术-几何均值不等式(x**2, y**2) 推导 this: x*y <= x**2/2 + y**2/2.
尚余一目标。
检验以下不等式可否成立：
-1*x**2 + -1*y**2 + 2*x*y > 0
-1/2*x**2 + -1/2*y**2 + 1*x*y <= 0
1*y >= 0
1*x >= 0
以下式子取和，得证不可能成立：
-1*x**2 + -1*y**2 + 2*x*y > 0 两边乘 1
-1/2*x**2 + -1/2*y**2 + 1*x*y <= 0 两边乘 -2
证明完毕！

要是能查看定理内容就更好了。

如果把使用定理这两行去掉：

    x, y = p.get_vars("x", "y")
    p.use_lemma(Amgm(x**2, y**2))

输出如下：

开始证明。当前情况：
x: nonneg_real
y: nonneg_real
求证：2*x*y <= x**2 + y**2
Checking feasibility of the following inequalities:
1*x >= 0
-1*x**2 + -1*y**2 + 2*x*y > 0
1*y >= 0
Feasible with the following values:
x*y = 0
y = 0
x = 0
y**2 = -1/2
x**2 = 0

看起来有问题。y 和 y**2 的值没有关联起来。回头看看有没有更简短的例子复现。

初感

在数学和编程结合方面，是一次非常珍贵的尝试。尤其是选取的内容与编程如算法复杂度很有关联，并且使用了接近初等数学公式的输入和输出格式，让更多人尤其是国内广大程序员群体对自动证明有了更直观的亲身体验。希望看到开枝散叶。

在中文化过程中，有些输出内容在不同文件中有重复，比如 Checking feasibility of the following inequalities: 在 linarith, linprog, log_linarith 中都有，也许是历史版本的冗余代码。

当前版用 SymPy 省去了自行定义各种基本类型，另一方面是对表达式符号的使用限制，比如 p.use_lemma(Amgm(x^2, y**2)) 就会报错：TypeError: unsupported operand type(s) for ^: 'Symbol' and 'int'

main.py 还有很多其他例子未尝试。在继续开发之前，如果重构代码并编写批量自动测试集，相信会对后续参与开发者降低门槛，也利于长远发展。