仓库源文，站点原文

https://zhuanlan.zhihu.com/p/1905620859944702830

对应5月1日博文：A proof of concept tool to verify estimates

感谢作者保留了该版本，五百行左右源码，比现在的三千多行少的多，可以更方便了解思路。

对其界面初步中文化后放在此库：不等式证明

运行博文中例程2输出如下：

% python examples.py
基于给定公理，确定 max(a, b, c) 是否 (((a * b) * c) ** 0.3333333333333333) 的上界。
分为以下情况：
[[b ≲ a, c ≲ a], [a ≲ b, c ≲ b], [a ≲ c, b ≲ c]]

检查情况: ([b ≲ a, c ≲ a],)
化为证明 (((a ** 0.6666666666666667) * (b ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1.
渐进界由以下假设相乘得证：
b ≲ a 的 0.33333333 次幂
c ≲ a 的 0.33333333 次幂

检查情况: ([a ≲ b, c ≲ b],)
化为证明 (((b ** 0.6666666666666667) * (a ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1.
渐进界由以下假设相乘得证：
a ≲ b 的 0.33333333 次幂
c ≲ b 的 0.33333333 次幂

检查情况: ([a ≲ c, b ≲ c],)
化为证明 (((c ** 0.6666666666666667) * (a ** -0.3333333333333333)) * (b ** -0.3333333333333333)) >= 1.
渐进界由以下假设相乘得证：
a ≲ c 的 0.33333333 次幂
b ≲ c 的 0.33333333 次幂
所有情况皆得证!

以下为例6输出：

基于给定公理，确定 (max(1, a) ** 2) 是否 a 的上界。
分为以下情况：
[[a ≲ 1], [a ≳ 1]]

检查情况: ([a ≲ 1],)
化为证明 (a ** -1) >= 1.
渐进界由以下假设相乘得证：
a ≲ 1 的 1.0 次幂

检查情况: ([a ≳ 1],)
化为证明 a >= 1.
渐进界由以下假设相乘得证：
1 ≲ a 的 1.0 次幂
所有情况皆得证!

例1输出：

基于给定公理，确定 max(a, b) 是否 min(a, b) 的上界。
分为以下情况：
[[a ≲ b], [b ≲ a]]
[[b ≲ a], [a ≲ b]]

检查情况: ([a ≲ b], [b ≲ a])
化为证明 (b * (a ** -1)) >= 1.
渐进界由以下假设相乘得证：
a ≲ b 的 1.0 次幂

检查情况: ([a ≲ b], [a ≲ b])
化为证明 (b * (a ** -1)) >= 1.
渐进界由以下假设相乘得证：
a ≲ b 的 1.0 次幂

检查情况: ([b ≲ a], [b ≲ a])
化为证明 (a * (b ** -1)) >= 1.
渐进界由以下假设相乘得证：
b ≲ a 的 1.0 次幂

检查情况: ([b ≲ a], [a ≲ b])
化为证明 (b * (a ** -1)) >= 1.
渐进界由以下假设相乘得证：
a ≲ b 的 1.0 次幂
所有情况皆得证!

粗看有以下几步：

• 从目标假设中，穷举出所有的变量和常量的排序可能
• 对每个排序组合：
  • 将这些排序关系存在有向图结构
  • 通过搜索图中两节点间是否有通路来比较节点大小
  • 归一化为 >=1 不等式证明
  • 后面用pulp库化为几个部分的乘积，验证每个部分是否Optimal，待细究
• 如果每个组合都可证，则得证

下面先看看第一版有何变化。