Some content in this article was created with AI assistance. Please verify as needed.

Lean 证明中的表达式、命题、证明项和 tactic 属于不同层次。只看执行效果时，ring、positivity、linarith 都像是在“帮我算一下”。实际上，tactic 负责构造证明，证明仍要经过 kernel 检查。

下面用一个单文件 Python demo 拆开这几层。程序处理如下代数问题：设 $0<p,q,r<1$，并且

$$
(1-p^2)(1-q^2)(1-r^2)=8p^2q^2r^2, \tag{1}
$$

分别证明

$$
1<p+q+r,
\qquad
p+q+r<2.
$$

程序不给 $p,q,r$ 赋浮点数，也不靠抽样验证结论。表达式、命题和证明都保存为数据，再由一个小型 checker 逐步检查：

1
2
3
4
5
6
7
数学写法
   ↓
Expr / Prop 抽象语法树
   ↓
规则或 tactic 构造 Proof 树
   ↓
Kernel 递归检查

下文按源码顺序解读。依次拼接所有 Python 代码块，即可得到完整的 demo 脚本。

表达式

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
# %% [markdown]
# # 用 Python 拆解 Lean：一个单文件证明器 demo
#
# 形式表达式 → 命题 → Proof 对象 → tactic 构造 Proof → Kernel 检查。
# 这只是有序域多项式上的教学模型，不是真正的 Lean 实现。

# %%
"""A one-file Lean-style proof demo for two algebraic inequalities."""

from __future__ import annotations

from dataclasses import dataclass
from fractions import Fraction
from itertools import product
from typing import Any

# %% [markdown]
# ## 1. 形式表达式与命题

# %%


@dataclass(frozen=True, eq=False)
class Expr:
    op: str
    args: tuple[Any, ...]

    @staticmethod
    def var(name: str) -> Expr:
        return Expr("var", (name,))

    @staticmethod
    def const(value: int | Fraction) -> Expr:
        return Expr("const", (Fraction(value),))

    def __add__(self, other):
        return Expr("add", (self, as_expr(other)))

    def __radd__(self, other):
        return as_expr(other) + self

    def __neg__(self):
        return Expr("neg", (self,))

    def __sub__(self, other):
        return self + -as_expr(other)

    def __rsub__(self, other):
        return as_expr(other) - self

    def __mul__(self, other):
        return Expr("mul", (self, as_expr(other)))

    def __rmul__(self, other):
        return as_expr(other) * self

    def __pow__(self, exponent: int):
        if not isinstance(exponent, int) or exponent < 0:
            raise ValueError("only non-negative integer powers are supported")
        return Expr("pow", (self, exponent))

    def __lt__(self, other):
        return Prop("<", self, as_expr(other))

    def __le__(self, other):
        return Prop("≤", self, as_expr(other))

    def __gt__(self, other):
        return Prop("<", as_expr(other), self)

    def __ge__(self, other):
        return Prop("≤", as_expr(other), self)

    def __eq__(self, other):  # type: ignore[override]
        # 形式等式返回 Prop，而不是 Python bool。
        return Prop("=", self, as_expr(other))

    def __hash__(self) -> int:
        raise TypeError("formal expressions are intentionally unhashable")

    def __str__(self):
        return show_expr(self)


def as_expr(value) -> Expr:
    """把 Python 整数提升为 Const；已有 Expr 保持不变。"""
    if isinstance(value, Expr):
        return value
    if isinstance(value, (int, Fraction)):
        return Expr.const(value)
    raise TypeError(f"cannot use {type(value).__name__} as an expression")

Expr 用一棵小型抽象语法树保存表达式。Expr.var("p") 不表示一个等待赋值的普通 Python 变量，而表示形式节点 Var("p")。常数统一保存为 Fraction，后续多项式运算不会引入浮点误差。

加法、乘法和幂的运算符重载也不做数值计算。例如 1 - p**2 内部保存成 Add(Const(1), Neg(Pow(Var("p"), 2)))。as_expr() 负责把 Python 整数提升为形式常数，所以整数可以和 Expr 一起书写。

Lean 原理：数学记号先被解析为语法，再由 elaborator 转换成带类型的 term。Kernel 检查的是 elaboration 后的 term，而不是用户输入的表面文本。这里的 Expr 只模拟了最前面的表达式构造。

命题及其结构比较

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
@dataclass(frozen=True, eq=False)
class Prop:
    kind: str
    # A tagged-union payload: binary propositions contain Expr values, while
    # ``not`` contains another Prop.  The kernel validates the tag before use.
    left: Any = None
    right: Any = None

    def __bool__(self):
        raise TypeError("a formal proposition is not a Python bool")

    def __str__(self):
        if self.kind == "not":
            return f"¬({self.left})"
        if self.kind == "false":
            return "False"
        return f"{self.left} {self.kind} {self.right}"


def Not(proposition: Prop) -> Prop:
    return Prop("not", proposition)


FALSE = Prop("false")
ZERO = Expr.const(0)


# Expr.__eq__ 用于构造命题，因此另用结构 key 比较 AST。
def expr_key(expr: Expr):
    if expr.op in {"var", "const"}:
        return (expr.op, expr.args[0])
    if expr.op == "pow":
        return ("pow", expr_key(expr.args[0]), expr.args[1])
    return (expr.op, *(expr_key(arg) for arg in expr.args))


def prop_key(prop: Prop):
    if prop.kind in {"=", "<", "≤"}:
        return prop.kind, expr_key(prop.left), expr_key(prop.right)
    if prop.kind == "not":
        return "not", prop_key(prop.left)
    return (prop.kind,)


def show_expr(expr: Expr, outer=0) -> str:
    """按运算优先级打印表达式；只影响展示，不参与证明正确性。"""
    if expr.op == "var":
        return expr.args[0]
    if expr.op == "const":
        value = expr.args[0]
        return str(value.numerator) if value.denominator == 1 else f"({value})"
    precedence = {"add": 1, "mul": 2, "neg": 3, "pow": 3}[expr.op]
    if expr.op == "add":
        left, right = expr.args
        text = (
            f"{show_expr(left, 1)} - {show_expr(right.args[0], 2)}"
            if right.op == "neg"
            else f"{show_expr(left, 1)} + {show_expr(right, 1)}"
        )
    elif expr.op == "mul":
        text = f"{show_expr(expr.args[0], 2)} * {show_expr(expr.args[1], 2)}"
    elif expr.op == "neg":
        text = f"-{show_expr(expr.args[0], 3)}"
    else:
        text = f"{show_expr(expr.args[0], 3)}^{expr.args[1]}"
    return f"({text})" if precedence < outer else text

比较运算构造 Prop。表达式 0 < p 的类型是 Prop，不是 bool；直接调用 bool(0 < p) 会抛出异常。此时应区分：

1
2
3
p       是 Expr
0 < p   是 Prop
hp0     稍后才会成为 Proof

Expr.__eq__ 已用来构造数学等式，不能再承担 Python 结构比较。expr_key() 和 prop_key() 把 AST 转为只含 tuple、字符串和有理数的 key，Kernel 后面用这些 key 核对命题。

Lean 原理：Lean 遵循 Curry–Howard 对应，命题是类型，证明是该类型的 term。Bool 是用于计算的数据类型。一个命题可以具有可判定性，但命题本身并不因此变成布尔值。

Proof object

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
# %% [markdown]
# ## 2. Proof object

# %%


@dataclass(frozen=True)
class Proof:
    proposition: Prop
    rule: str
    premises: tuple[Proof, ...] = ()
    certificate: tuple[Fraction, ...] | None = None
    name: str | None = None

    def tree(self, indent="") -> str:
        """把 proof tree 展开为缩进文本，便于观察 tactic 实际生成了什么。"""
        label = f" [{self.name}]" if self.name else ""
        lines = [f"{indent}{self.rule}{label}: {self.proposition}"]
        lines += [premise.tree(indent + "  ") for premise in self.premises]
        return "\n".join(lines)


def assume(prop: Prop, name: str) -> Proof:
    """构造假设叶子；它只有出现在 theorem assumptions 中才会被 Kernel 接受。"""
    return Proof(prop, "assumption", name=name)

Proof 保存结论、规则、子证明和可选证书。假设是 Proof 树的叶子；assume(0 < p, "hp0") 只是构造一个标记为 assumption 的节点，它最终仍要由 Kernel 确认属于定理的允许假设。

Lean 原理：证明成立的含义是“存在一个 term，其类型正是该命题”。正确性因此归结为类型检查，而不是给命题附加一个 True 标记。Proof 把命题和构造过程显式存入记录，只是对 proof term 的简化模拟。

多项式正规形

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
# %% [markdown]
# ## 3. 多项式正规形

# %%


def poly(expr: Expr):
    """Normalize to {monomial: coefficient}; a monomial is ((name, power), ...)."""
    if expr.op == "const":
        return {} if expr.args[0] == 0 else {(): expr.args[0]}
    if expr.op == "var":
        return {((expr.args[0], 1),): Fraction(1)}
    if expr.op == "neg":
        return scale(poly(expr.args[0]), -1)
    if expr.op == "add":
        return add_poly(poly(expr.args[0]), poly(expr.args[1]))
    if expr.op == "mul":
        return mul_poly(poly(expr.args[0]), poly(expr.args[1]))
    result = {(): Fraction(1)}
    for _ in range(expr.args[1]):
        result = mul_poly(result, poly(expr.args[0]))
    return result


def add_poly(left, right):
    result = dict(left)
    for monomial, value in right.items():
        result[monomial] = result.get(monomial, 0) + value
        if result[monomial] == 0:
            del result[monomial]
    return result


def scale(value, coefficient):
    coefficient = Fraction(coefficient)
    return {} if coefficient == 0 else {m: coefficient * c for m, c in value.items()}


def mul_poly(left, right):
    result = {}
    for lm, lc in left.items():
        for rm, rc in right.items():
            powers = {}
            for name, exponent in lm + rm:
                powers[name] = powers.get(name, 0) + exponent
            monomial = tuple(sorted(powers.items()))
            result[monomial] = result.get(monomial, 0) + lc * rc
    return {m: c for m, c in result.items() if c}


def difference(prop: Prop):
    """把 a < b 或 a ≤ b 统一表示成右减左，即多项式 b-a。"""
    return add_poly(poly(prop.right), scale(poly(prop.left), -1))

poly() 把多项式展开为字典 {单项式: 系数}。例如 $8p^2q$ 的表示为：

1
{(("p", 2), ("q", 1)): Fraction(8)}

mul_poly() 合并同名变量的次数，add_poly() 合并相同单项式的系数。因此 (1-p)*(1+p) 和 1-p**2 虽然 AST 不同，却有相同的正规形。

对 $a<b$ 或 $a\le b$，difference() 统一计算右边减左边，即 $b-a$。这样线性推理只需处理“某个多项式为正或非负”。

Lean 原理：证明自动化可以使用反射，先把表达式转成便于计算的内部表示，再比较正规形，并把计算结果转回可检查的证明。可信性不来自“算法运行成功”，而来自算法最终产生的证明能通过 Kernel。

Kernel

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
# %% [markdown]
# ## 4. Kernel

# %%


class KernelError(ValueError):
    pass


def check(candidate: Proof, assumptions=()) -> bool:
    """递归检查 proof tree；这里只接收声明过的定理假设。"""
    allowed = tuple(prop_key(prop) for prop in assumptions)

    def visit(node: Proof, local=allowed):
        prop, rule, ps = node.proposition, node.rule, node.premises

        if rule == "assumption":
            if prop_key(prop) not in local:
                raise KernelError(f"unavailable assumption: {prop}")
            return
        if rule == "by_contra":
            require(
                len(ps) == 1 and prop.kind == "<" and ps[0].proposition.kind == "false",
                rule,
            )
            # 只在反证子树中开放 ¬goal。
            visit(ps[0], local + (prop_key(Not(prop)),))
            return

        for premise in ps:
            visit(premise, local)

        if rule == "positive_const":
            require(
                not ps
                and prop.kind == "<"
                and expr_key(prop.left) == expr_key(ZERO)
                and prop.right.op == "const"
                and prop.right.args[0] > 0,
                rule,
            )
        elif rule == "mul_pos":
            require(len(ps) == 2 and positive(ps[0]) and positive(ps[1]), rule)
            expect(prop, ZERO < ps[0].proposition.right * ps[1].proposition.right)
        elif rule == "sub_pos":
            require(len(ps) == 1 and ps[0].proposition.kind == "<", rule)
            expect(prop, ZERO < ps[0].proposition.right - ps[0].proposition.left)
        elif rule == "lt_trans":
            require(len(ps) == 2 and all(p.proposition.kind == "<" for p in ps), rule)
            require(
                expr_key(ps[0].proposition.right) == expr_key(ps[1].proposition.left),
                rule,
            )
            expect(prop, ps[0].proposition.left < ps[1].proposition.right)
        elif rule in {"mul_lt_right", "mul_lt_left"}:
            require(
                len(ps) == 2 and ps[0].proposition.kind == "<" and positive(ps[1]), rule
            )
            relation, term = ps[0].proposition, ps[1].proposition.right
            expected = (
                (relation.left * term < relation.right * term)
                if rule.endswith("right")
                else (term * relation.left < term * relation.right)
            )
            expect(prop, expected)
        elif rule == "ring":
            require(
                not ps and prop.kind == "=" and poly(prop.left) == poly(prop.right),
                rule,
            )
        elif rule == "linear":
            certificate = node.certificate
            require(prop.kind in {"<", "≤"} and certificate is not None, rule)
            if certificate is None:
                raise KernelError("linear proof has no certificate")
            require(len(certificate) == len(ps), rule)
            total, strict = {}, False
            for weight, premise in zip(certificate, ps):
                relation = premise.proposition
                require(relation.kind in {"=", "<", "≤"}, rule)
                require(relation.kind == "=" or weight >= 0, rule)
                total = add_poly(total, scale(difference(relation), weight))
                strict |= relation.kind == "<" and weight > 0
            require(total == difference(prop) and (prop.kind == "≤" or strict), rule)
        elif rule in {"eq_then_lt", "lt_then_eq"}:
            require(len(ps) == 2, rule)
            eq, lt = (
                (ps[0].proposition, ps[1].proposition)
                if rule == "eq_then_lt"
                else (ps[1].proposition, ps[0].proposition)
            )
            require(eq.kind == "=" and lt.kind == "<", rule)
            if rule == "eq_then_lt":
                require(expr_key(eq.right) == expr_key(lt.left), rule)
                expect(prop, eq.left < lt.right)
            else:
                require(expr_key(lt.right) == expr_key(eq.left), rule)
                expect(prop, lt.left < eq.right)
        elif rule == "le_of_not_gt":
            require(
                len(ps) == 1
                and ps[0].proposition.kind == "not"
                and ps[0].proposition.left.kind == "<",
                rule,
            )
            negated = ps[0].proposition.left
            expect(prop, negated.right <= negated.left)
        elif rule == "eq_lt_false":
            require(len(ps) == 2 and prop.kind == "false", rule)
            eq, lt = ps[0].proposition, ps[1].proposition
            require(eq.kind == "=" and lt.kind == "<", rule)
            endpoints = {expr_key(eq.left), expr_key(eq.right)}
            require(endpoints == {expr_key(lt.left), expr_key(lt.right)}, rule)
        else:
            raise KernelError(f"unknown rule: {rule}")

    visit(candidate)
    return True


def require(condition, rule):
    if not condition:
        raise KernelError(f"invalid use of {rule}")


def expect(actual, expected):
    require(prop_key(actual) == prop_key(expected), "wrong conclusion")


def positive(proof):
    return proof.proposition.kind == "<" and expr_key(
        proof.proposition.left
    ) == expr_key(ZERO)

check() 不搜索证明，只递归检查 Proof 树。假设节点必须出现在 allowed 中；把任意命题包装成 Proof(prop, "assumption") 不能凭空获得结论。

每个规则分支都重新构造期望结论。例如 mul_pos 检查两个前提确实具有 $0<a$、$0<b$ 的形式，再要求当前节点的结论恰好是 $0<ab$。mul_lt_left 和 mul_lt_right 还会检查乘数为正，因为负数会改变不等号方向。

ring 分支重新计算等式两边的正规形。linear 分支读取 tactic 给出的系数证书，检查

$$
\sum_i c_i(\text{right}_i-\text{left}_i)
=\text{goal.right}-\text{goal.left}.
$$

不等式的系数必须非负；严格结论还必须使用至少一个严格不等式。

检查 by_contra 时，Kernel 会在“推出 False”的子树中临时把 Not(goal) 加入局部假设。离开这棵子树以后，该假设不再可用。

Lean 原理：Lean 把可信基础压缩在较小的 Kernel 中。Kernel 依据类型论规则检查 term，并执行必要的归约；搜索策略和大部分数学自动化位于可信边界之外。本 demo 使用粒度较粗的直接规则，但同样把证明搜索排除在可信检查器之外。

基础规则构造器

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
# %% [markdown]
# ## 5. Rule constructor 与 tactic

# %%


def positive_const(n):
    return Proof(ZERO < n, "positive_const")


def mul_pos(a, b):
    return Proof(ZERO < a.proposition.right * b.proposition.right, "mul_pos", (a, b))


def sub_pos(h):
    return Proof(ZERO < h.proposition.right - h.proposition.left, "sub_pos", (h,))


def lt_trans(a, b):
    return Proof(a.proposition.left < b.proposition.right, "lt_trans", (a, b))


def mul_lt_right(h, hp):
    return Proof(
        h.proposition.left * hp.proposition.right
        < h.proposition.right * hp.proposition.right,
        "mul_lt_right",
        (h, hp),
    )


def mul_lt_left(h, hp):
    return Proof(
        hp.proposition.right * h.proposition.left
        < hp.proposition.right * h.proposition.right,
        "mul_lt_left",
        (h, hp),
    )


def eq_then_lt(eq, lt):
    return Proof(eq.proposition.left < lt.proposition.right, "eq_then_lt", (eq, lt))


def lt_then_eq(lt, eq):
    return Proof(lt.proposition.left < eq.proposition.right, "lt_then_eq", (lt, eq))


def le_of_not_gt(h):
    negated = h.proposition.left
    return Proof(negated.right <= negated.left, "le_of_not_gt", (h,))


def contradiction(eq, lt):
    return Proof(FALSE, "eq_lt_false", (eq, lt))


def by_contra(goal, false_proof):
    return Proof(goal, "by_contra", (false_proof,))

这些函数是显式规则构造器，只组装 Proof 节点。它们不搜索证明，也不会自行调用 Kernel。例如 mul_lt_right() 根据两个前提拼出一个新结论，但该节点是否符合规则仍由 check() 判断。

Lean 原理：定理和引理可以看成函数，输入若干前提的证明，输出结论的证明。组合证明就是应用这些函数并形成更大的 term，而不是在运行时把命题“算成真”。这里的规则构造器将这种组合直接显示为树节点。

三个简单 tactic

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
def ring(left, right):
    """寻找一个 ring proof；Kernel 稍后会再次正规化，不信任这里的判断。"""
    if poly(left) != poly(right):
        raise ValueError("ring failed")
    return Proof(left == right, "ring")


def positivity(expr, known):
    """递归拆解乘法，在已知假设中寻找每个因子的正性证明。"""
    for proof in known:
        if prop_key(proof.proposition) == prop_key(ZERO < expr):
            return proof
    if expr.op == "const" and expr.args[0] > 0:
        return positive_const(expr.args[0])
    if expr.op == "mul":
        return mul_pos(positivity(expr.args[0], known), positivity(expr.args[1], known))
    raise ValueError(f"positivity cannot prove 0 < {expr}")


def linarith(goal, premises):
    """枚举系数 0、1、2，寻找一个足以推出 goal 的加法证书。

    这远不是真正的 Lean ``linarith``，更不是 ``nlinarith``。刻意保持它很小，
    才能直观看到 tactic 产出的 certificate 如何被 Kernel 重新检查。
    """
    for weights in product((0, 1, 2), repeat=len(premises)):
        total, strict = {}, False
        for weight, premise in zip(weights, premises):
            total = add_poly(total, scale(difference(premise.proposition), weight))
            strict |= premise.proposition.kind == "<" and weight > 0
        if total == difference(goal) and (goal.kind == "≤" or strict):
            return Proof(goal, "linear", tuple(premises), tuple(map(Fraction, weights)))
    raise ValueError(f"tiny linarith found no certificate for {goal}")

ring、positivity 和 linarith 会做搜索或计算，可以视为 tactic；它们的返回值仍然只是待检查的 Proof。

positivity(2*p*r, hs) 沿乘法 AST 递归，在 hs 中找到 $0<p$、$0<r$，并为常数 2 构造 positive_const。结果是一棵由 assumption、positive_const 和 mul_pos 组成的树，没有向 Kernel 添加新规则。

极小版 linarith 只枚举系数 $0,1,2$。例如 $q(1-r)>0$ 和 $r(1-q)>0$ 的 difference 相加为

$$
(q-qr)+(r-qr)=q+r-2qr>0,
$$

即 $2qr<q+r$。tactic 把 (1, 1) 存入 certificate，Kernel 再做一次同样的线性组合检查。

Lean 原理：Tactic 位于元编程层，可以读取目标和局部上下文，执行搜索、归一化或决策过程，但产物仍是 proof term。若生成的 term 不满足目标，Kernel 会拒绝它；tactic 本身不在可信基础内。

公共假设与小引理

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
# %% [markdown]
# ## 6. 公共假设与小引理

# %%


def hypotheses(p, q, r):
    props = (
        0 < p,
        p < 1,
        0 < q,
        q < 1,
        0 < r,
        r < 1,
        (1 - p**2) * (1 - q**2) * (1 - r**2) == 8 * p**2 * q**2 * r**2,
    )
    names = ("hp0", "hp1", "hq0", "hq1", "hr0", "hr1", "hprod")
    return tuple(assume(prop, name) for prop, name in zip(props, names))


def square_positive(x, hx0, hx1):
    # 0 < 1-x，0 < 1+x，所以 0 < (1-x)(1+x)；再用 ring 改写为 1-x²。
    factors = mul_pos(sub_pos(hx1), linarith(0 < 1 + x, (positive_const(1), hx0)))
    return lt_then_eq(factors, ring((1 - x) * (1 + x), 1 - x**2))


def sum_pair(x, y, hx0, hx1, hy0, hy1):
    # x(1-y)>0 与 y(1-x)>0 相加，得到 2xy < x+y。
    a = mul_pos(hx0, sub_pos(hy1))
    b = mul_pos(hy0, sub_pos(hx1))
    return linarith(2 * x * y < x + y, (a, b))


def product_pair(x, y, hx1, hy1):
    # (1-x)(1-y)>0 展开后正是 x+y-1 < xy。
    return linarith(x + y - 1 < x * y, (mul_pos(sub_pos(hx1), sub_pos(hy1)),))

hypotheses() 创建六个范围假设和等式 (1)。square_positive() 将 $1-x^2$ 写成 $(1-x)(1+x)$，再由 $0<x<1$ 证明两个因子为正。sum_pair() 从 $x(1-y)>0$、$y(1-x)>0$ 得 $2xy<x+y$；product_pair() 从 $(1-x)(1-y)>0$ 得 $x+y-1<xy$。

Lean 原理：证明状态包含目标和局部上下文。上下文中的每一项都是带类型的局部声明；中间结论会扩展这个上下文，后续 term 可以引用它们。最终证明依赖哪些假设，也由这些引用明确记录。

第一个目标

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
# %% [markdown]
# ## 7. 第一个目标：`1 < p+q+r`


# %%
def prove_goal1(p, q, r, hs):
    hp0, hp1, hq0, hq1, hr0, hr1, hprod = hs
    hp_sq, hq_sq = square_positive(p, hp0, hp1), square_positive(q, hq0, hq1)
    h2pr = positivity(2 * p * r, hs)
    h2pq = positivity(2 * p * q, hs)
    goal = 1 < p + q + r
    hnot = assume(Not(goal), "h")
    hsum = le_of_not_gt(hnot)

    hqr = sum_pair(q, r, hq0, hq1, hr0, hr1)
    hpr = sum_pair(p, r, hp0, hp1, hr0, hr1)
    hpq = sum_pair(p, q, hp0, hp1, hq0, hq1)
    hp1a = linarith(2 * q * r < 1 - p, (hqr, hsum))
    hq1a = linarith(2 * p * r < 1 - q, (hpr, hsum))
    hr1a = linarith(2 * p * q < 1 - r, (hpq, hsum))
    hp = linarith(2 * q * r < 1 - p**2, (hp1a, mul_pos(hp0, sub_pos(hp1))))
    hq = linarith(2 * p * r < 1 - q**2, (hq1a, mul_pos(hq0, sub_pos(hq1))))
    hr = linarith(2 * p * q < 1 - r**2, (hr1a, mul_pos(hr0, sub_pos(hr1))))

    first = lt_trans(mul_lt_right(hp, h2pr), mul_lt_left(hq, hp_sq))
    triple = lt_trans(mul_lt_right(first, h2pq), mul_lt_left(hr, mul_pos(hp_sq, hq_sq)))
    expanded = (2 * q * r) * (2 * p * r) * (2 * p * q)
    strict = eq_then_lt(ring(8 * p**2 * q**2 * r**2, expanded), triple)
    return by_contra(goal, contradiction(hprod, strict))

第一个目标使用反证法。hnot 表示 $\neg(1<p+q+r)$，le_of_not_gt() 得到 $p+q+r\le1$。三次调用 sum_pair() 后，通过线性组合得到

$$
2qr<1-p,
\quad 2pr<1-q,
\quad 2pq<1-r.
$$

因为 $p(1-p)>0$，有 $(1-p)+p(1-p)=1-p^2>1-p$，另外两组同理。于是代码中的 hp、hq、hr 分别证明

$$
2qr<1-p^2,
\quad 2pr<1-q^2,
\quad 2pq<1-r^2.
$$

三个不等式分两次相乘。每次调用 mul_lt_left 或 mul_lt_right 都显式提供正性证明，
不能无条件把两个严格不等式相乘。ring 将左侧整理为 $8p^2q^2r^2$，所得严格不等式与 hprod 冲突，by_contra 返回目标 Proof。

Lean 原理：反证法会在一个局部作用域中假设目标的否定，再从该假设推出矛盾。完成后的 proof term 会解除这个临时假设；它不能泄漏到作用域之外。这里通过 Kernel 检查时临时扩展 local，模拟假设的引入与解除。

第二个目标

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
# %% [markdown]
# ## 8. 第二个目标：`p+q+r < 2`


# %%
def square_lt(x, pair, canonical, hprime, hx0, hx1, pair_pos):
    """由 1-x<pair 和 1+x<2 显式相乘，得到 1-x²<2*pair。"""
    first = mul_lt_right(hprime, linarith(0 < 1 + x, (positive_const(1), hx0)))
    second = mul_lt_left(linarith(1 + x < 2, (hx1,)), pair_pos)
    chain = lt_trans(first, second)
    chain = eq_then_lt(ring(1 - x**2, (1 - x) * (1 + x)), chain)
    return lt_then_eq(chain, ring(pair * 2, canonical))


def prove_goal2(p, q, r, hs):
    hp0, hp1, hq0, hq1, hr0, hr1, hprod = hs
    hq_sq = square_positive(q, hq0, hq1)
    hr_sq = square_positive(r, hr0, hr1)
    h2qr, h2pr = positivity(2 * q * r, hs), positivity(2 * p * r, hs)
    goal = p + q + r < 2
    hnot = assume(Not(goal), "h")
    hsum = le_of_not_gt(hnot)
    hp1a = linarith(1 - p < q * r, (hsum, product_pair(q, r, hq1, hr1)))
    hq1a = linarith(1 - q < p * r, (hsum, product_pair(p, r, hp1, hr1)))
    hr1a = linarith(1 - r < p * q, (hsum, product_pair(p, q, hp1, hq1)))
    hp = square_lt(p, q * r, 2 * q * r, hp1a, hp0, hp1, positivity(q * r, hs))
    hq = square_lt(q, p * r, 2 * p * r, hq1a, hq0, hq1, positivity(p * r, hs))
    hr = square_lt(r, p * q, 2 * p * q, hr1a, hr0, hr1, positivity(p * q, hs))

    first = lt_trans(mul_lt_right(hp, hq_sq), mul_lt_left(hq, h2qr))
    triple = lt_trans(mul_lt_right(first, hr_sq), mul_lt_left(hr, mul_pos(h2qr, h2pr)))
    expanded = (2 * q * r) * (2 * p * r) * (2 * p * q)
    strict = lt_then_eq(triple, ring(expanded, 8 * p**2 * q**2 * r**2))
    return by_contra(goal, contradiction(hprod, strict))

第二个目标的反设是 $2\le p+q+r$。由 $(1-q)(1-r)>0$ 得 $q+r-1<qr$，结合反设可得 $1-p<qr$。square_lt() 再把 $1-p<qr$ 和 $1+p<2$ 同乘正数，得到 $1-p^2<2qr$。循环处理三组变量后，分两次相乘得到

$$
(1-p^2)(1-q^2)(1-r^2)<8p^2q^2r^2,
$$

这同样与 hprod 矛盾。

Lean 原理：形式化定理的类型会编码适用条件。不等式同乘需要正性，除法需要分母非零，开平方常需要非负性。自动化可以帮助寻找这些条件的证明，但最终 term 必须把所需参数完整地提供出来。

运行最终检查

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
# %% [markdown]
# ## 9. 运行检查


# %%
def main():
    p, q, r = (Expr.var(name) for name in "pqr")
    hs = hypotheses(p, q, r)
    assumptions = tuple(h.proposition for h in hs)
    goal1_proof = prove_goal1(p, q, r, hs)
    goal2_proof = prove_goal2(p, q, r, hs)
    check(goal1_proof, assumptions)
    check(goal2_proof, assumptions)
    print(f"✓ first goal checked:  {goal1_proof.proposition}")
    print(f"✓ second goal checked: {goal2_proof.proposition}")
    print("\nThe result is a Proof tree, not True:")
    print(f"  proof type = {type(goal1_proof).__name__}")
    print(f"  root rule  = {goal1_proof.rule}")
    return goal1_proof, goal2_proof


if __name__ == "__main__":
    goal1_proof, goal2_proof = main()

main() 先构造两个 Proof，最后才调用 check()。运行输出为：

1
2
3
4
5
6
✓ first goal checked:  1 < p + q + r
✓ second goal checked: p + q + r < 2

The result is a Proof tree, not True:
  proof type = Proof
  root rule  = by_contra

Lean 原理：前端负责解析语法，elaborator 负责补全并生成带类型的 term，tactic 负责构造缺失的证明，最后由 Kernel 检查。通常这条流水线自动运行。显式调用 check() 是为了把最后一步和前面的证明搜索区分开。

这份 demo 的范围很窄：linarith 只搜索三个整数系数，ring 只处理当前 AST 中的多项式，反证规则也只面向严格不等式。真实 Lean 还要处理函数、量词、归纳类型、隐式参数和 universe。这个简化版本集中说明 tactic 与 Kernel 的分工：前者寻找 Proof，后者检查 Proof。