计算机数学入门（三）：怎么证明它是对的

上一篇：（二）世界是连续的，机器是离散的——讲一堆东西怎么被压进机器。 这一篇：讲怎么确认压完之后它还是对的。

耗时：读完约 50 分钟，动手约 2 小时。

开头：一个活了 9 年的 bug

2006 年，Google 的 Joshua Bloch 在博客里写了一件事：

JDK 里的二分查找是错的。

不是逻辑写错了。是这一行：

int mid = (low + high) / 2;

看着完全正常。它错在：low + high 会溢出。

int lo = 2000000000, hi = 2100000000;
printf("%d\n", lo + hi);        // -194967296
printf("%d\n", (lo + hi) / 2);  // -97483648

两个正数加起来变成负数，中间位置算出来是 −97,483,648。

而且这个错，在 Java 里活了大约 9 年。

为什么能活这么久？因为这个 bug 只在数组超过 10 亿个元素时才会触发。日常测试、单元测试、代码评审，全都碰不到。逻辑「看起来」完美，测试「全都过了」，线上「从来没出问题」——因为它根本触发不到。

这一篇讲的就是这件事：「我觉得没问题」和「我证明它没问题」，差在哪里。

上一篇结尾说过：离散化砍了三刀，每一刀都有确定的规律，所以每一刀都能提前算。那——「算对了」这件事本身，怎么保证？

一、先看测试能走多远：5 个二分查找，穷举测

二分查找是计算机科学里最被反复研究的算法之一。它的正确写法只有几种，错误写法有无数种。

我写了 6 个版本，穷举所有输入去测：

• 数组：{0..11} 的所有子集，长度 0 到 8（去重、排序）→ 共 3798 个数组
• 查询值：−1 到 12 → 每个数组 14 个
• 总用例：53,158 个

结果：

这里有个特别值得注意的细节

v5（lo = mid 那个）失败的方式很特殊：

53,158 个用例 → 死循环 41,562 次，答错 0 次，答对 11,596 次

它从来没有给出过错误答案。 要么对，要么永远不停。

为什么？因为 lo = mid 在 a[mid] < x 时，如果 mid == lo，区间就再也不缩小了——lo 永远是 lo。它不是在算错答案，它是在原地打转。

这就是为什么这类 bug 最阴险：如果你的测试跑在超时保护里，它表现为"偶尔超时"；如果没有超时保护，它表现为"卡死"。它永远不会给你一个错的数字让你发现。

但测试没告诉你最重要的一件事

现在看这 5 行结果，问一个问题：

v1 和 v2 都「全过」——它们是同一个算法吗？

不是。v1 用闭区间，v2 用半开区间。它们的循环条件不同、更新方式不同、终止状态不同。它们只在"结果"上一致。

测试能告诉你「这两个在 5 万个输入上给出相同输出」。它不能告诉你——

• v1 为什么对？
• v2 为什么对？
• 为什么 v3 只差一点就错了？
• 换一个 10 亿元素的数组，v1 还对吗？（v6 就是这个问题）

这就是「测试」和「证明」的分界线：测试给的是样本，证明给的是全部。

而 v6 那一行更狠——它在我的测试里全过，因为它跑在 Python 上，Python 的整数不溢出。 同一个算法搬进 Java/C，在 10 亿元素时就会崩。

测试的盲区，取决于你用什么环境测。 你在 Python 上测出来的「全过」，不能保证 C 里也对。

二、换一条路：归纳法

先离开代码，看纯数学。三个命题，每个都"验证过很多次"：

命题 A：n² + n + 41 对所有 n ≥ 0 都是素数

验证一下：

n = 0 到 39，连续 40 个值，全是素数。 这个数很有意思，欧拉发现的。

那 n = 40 呢？

40² + 40 + 41 = 1600 + 40 + 41 = 1681 = 41 × 41

是合数。 而且恰好是 41 的平方。

验证了 40 次没错，第 41 次错。 这个命题一测就穿。

命题 B：2ⁿ − 1 对 n = 2, 3, 5, 7 都是素数

验证了 4 次没错，第 5 次错。 而且注意第 6 次（n=13）又对了——所以"错了之后又对了"也会发生，你不能用"最近一次通过"当证据。

命题 C：1 + 2 + … + n = n(n+1)/2

我验了 n = 0 到 100,000：

反例：0 个

但这不是证明。

三个命题的对照，说明一件事

第三行是最关键的：即使命题是真的，你测 10 万次也不能证明它。

「没测出错误」只能推出「没测出错误」。它推不出「正确」。

那怎么办？数学的答案只有一条：找到那个"为什么对所有 n 都成立"的结构。

归纳法：两步，不是一万步

要证明「对所有 n 成立」，只需要两步：

1. 基础步：证明 n = 0（或 1）时成立
2. 归纳步：假设 n = k 时成立，证明 n = k+1 时也成立

然后你就可以说：对所有 n 成立。

为什么？因为 0 成立 → 1 成立 → 2 成立 → ……这个链条是无底的，所以覆盖了全部自然数。

对命题 C（求和公式）做一遍：

基础步：n=0 时，左边 = 0，右边 = 0×1/2 = 0。✅

归纳步：假设 1+2+…+k = k(k+1)/2 成立。那么

1 + 2 + … + k + (k+1) = k(k+1)/2 + (k+1)
                       = (k+1)(k/2 + 1)
                       = (k+1)(k+2)/2

这正是 n = k+1 时的公式。

两步。比分 10 万次还短，而且它覆盖了 n = 10⁹、n = 10¹⁰⁰、你根本跑不到的所有 n。

归纳法的价值不在"省事"，在于它是唯一能覆盖"无限多个情况"的方法。 测试永远只能覆盖有限个。

三、进到程序里：循环不变量

归纳法讲的是自然数。程序里的循环，本质上是同一个东西：

循环每转一圈，就相当于归纳法里的"从 k 走到 k+1"。

把这个想法形式化，就是循环不变量（loop invariant）。

定义

循环不变量是一个关于程序变量的断言，要求在三个时刻都成立：

1. 初始化（进入循环前）：成立
2. 保持（每轮循环体执行后）：如果这轮开始时成立，这轮结束时仍然成立
3. 终止（循环结束后）：加上终止条件，能推出你要的结论

第 2 条就是归纳步。整个结构跟归纳法一模一样，只是"n"换成了"循环轮数"。

用它证明二分查找

先固定一个版本（v1，闭区间）：

int binary_search(int a[], int n, int x) {
    int lo = 0, hi = n - 1;
    while (lo <= hi) {
        int mid = lo + (hi - lo) / 2;     // 注意这里，稍后讲
        if (a[mid] == x) return mid;
        else if (a[mid] < x) lo = mid + 1;
        else hi = mid - 1;
    }
    return -1;
}

不变量（注意它说的是条件句，不是"x 在数组里"）：

I：如果 x 出现在 a 中，那么它的下标一定落在 [lo, hi] 内。

这个条件句很关键——x 可能根本不在数组里，那时前提为假，整个命题在形式上成立（这一点第五节细讲）。

现在验证三个时刻：

1. 初始化：lo=0, hi=n−1，覆盖整个数组。如果 x 在里面，它的下标当然在 [0, n−1] 内。✅

2. 保持：假设进入这轮时 I 成立。看三个分支：

• a[mid] == x：直接返回 mid，循环不再继续，保持条件不需要验证（这也是一种正确：返回值是对的）
• a[mid] < x：因为数组有序，x 不可能在 mid 及其左边 → x 若存在，下标在 [mid+1, hi]。代码正好设 lo = mid+1。✅
• a[mid] > x：同理，x 若存在，下标在 [lo, mid−1]。代码设 hi = mid−1。✅

注意第二步里，“有序"这个前提被用到了。 数组不是有序的，整个证明就垮了。这就是为什么证明了正确性的代码，换个前提就不对。

3. 终止：循环结束时 lo > hi，即区间 [lo, hi] 是空的。而 I 说"x 若存在则下标在 [lo,hi] 内”——空区间里没有任何下标。

所以 x 不存在。 返回 −1 是对的。✅

证完了。

现在用它去"审"那 5 个变体

有了不变量，你不用跑 5 万个用例，直接看代码就知道哪错：

看到区别了吗：

• 测试告诉你：v3 错 7216 次，v4 错 11674 次，v5 死循环。
• 不变量告诉你：v3 错在终止条件，v4 错在区间不缩小，v5 错在根本不终止。

前者是"哪里坏了"，后者是"为什么坏"。 后者才能让你下次不犯。

这就是"彻底掌握"和"能用"的分界线。 能用 = 我知道这个写法能跑。 掌握 = 我知道为什么这个写法能跑，所以换一个场景也能判断。

四、那个溢出 bug：不变量写在纸上是假的

回到开头那个活了 9 年的 bug。

int mid = (lo + hi) / 2;

我在 C 里实测（lo = 2000000000, hi = 2100000000，查 2050000000）：

(lo + hi) = -194967296      ← 超过 INT32_MAX(2147483647) 1952516353
(lo + hi) / 2 = -97483648   ← 中间位置算成了负数

buggy 版第 1 轮: lo=2000000000 hi=2100000000 mid=-97483648
        第 2 轮: lo=-97483647   hi=2100000000 mid=1001258176
        第 3 轮: lo=1001258177  hi=2100000000 mid=-596854559
        第 4 轮: lo=-596854558  hi=2100000000 mid=751572721
        第 5 轮: lo=751572722   hi=2100000000 mid=-721697287
        → 永远不收敛，死循环

正确版 mid = lo + (hi - lo) / 2 → 2050000000，一次命中

看到那个 mid 序列了吗：负数、正数、负数、正数……它在来回跳，永远落不到目标上。

这件事的教训比 bug 本身重要

我在纸上证的那三条，全都依赖一个隐含前提：

mid 落在 [lo, hi] 里面。

(lo+hi)/2 在数学上确实落在区间里。但在 32 位整数上不是。 我的证明里，mid 是一个"数字"；代码里，mid 是一个 32 位整数。

数学证明的是"理想对象"的性质。程序和理想对象之间，隔着一层"表示"。 第一层（数值表示）和这一层（证明）在这里对撞了。

这正是上一篇讲的"格点"在逻辑上的版本：你以为你在证明一个连续的东西，其实你在证明一个离散的东西；而你的证明脚本站错了地方。

还有一层：我的测试环境也是盲区

这个 bug 在 Python 里永远不会出现：

>>> lo, hi = 2000000000, 2100000000
>>> (lo + hi) // 2
2050000000          # 完全正常，Python 整数无限精度

所以如果我拿 Python 写测试、拿 C 写生产代码，测试 100% 通过，生产 100% 崩。

测试能给的东西，上限是"我这个环境下没出问题"。 这不是没用——但它不是"正确"。

五、命题逻辑：为什么"条件写反了"是数学错误

到这儿，逻辑还只用在"推断"上。但现在要正式一点：条件和判断本身，也是可以研究、可以证明的对象。

三个基本运算，一张真值表

A → B（蕴含）那一列是最反直觉的：前提 A 为假时，整个蕴含恒为真。

这不是数学家的怪癖，它有道理：「如果明天下雨，我就带伞」——明天没下雨，你带不带伞都不算食言。 你只在"下雨了却没带伞"时才食言。

最后两行（A 为假）整个蕴含都为真，这叫空真（vacuous truth）。

这个奇怪的东西，在代码里天天出现。

空真在代码里的样子

>>> all(x > 0 for x in [])     # 空数组上，"所有元素都 > 0" 
True
>>> any(x > 0 for x in [])     # 空数组上，"存在元素 > 0"
False

空数组上 all() 返回 True。

很多人第一次见会觉得是 bug。它是对的：全称命题「对每个 x，若 x 在数组里则 x>0」——数组里没有 x，前提不成立，整个命题为真。

它的实际后果要记住：

空数组上的 all() 返回 True，这一条会导致真实的逻辑漏洞：

if all(check(p) for p in 用户权限列表):      # 权限列表为空 → 通过！
    允许访问()

用户一个权限都没有，反而全通过了。 这不是假设，这是真实系统里反复出现的漏洞形态。

德摩根律：为什么"改成 ||“是错的

¬(A ∧ B)  ==  (¬A) ∨ (¬B)
¬(A ∨ B)  ==  (¬A) ∧ (¬B)

穷举验证 4 种组合：违反 0 次。 恒等式，不是巧合。

所以下面这个改法必错：

// 原意：不满足（甲 且 乙）就报错
if (!(age >= 18 && has_license)) error();

// 有人"简化"成：
if (age < 18 || !has_license) error();     // ✅ 这个改对了（德摩根）
if (age < 18 && has_license) error();      // ❌ 改错了，变成"未成年且有驾照才报错"

德摩根律告诉你：&& 取反变成 ||，不是保持 &&。 这不是编码风格，这是恒等式——它只有一种正确写法，其余全错。

为什么这类 bug 特别难查：它在 75% 的输入上表现正常。只有当左边那条和右边那条一真一假时，才暴露。而测试往往只走"常见路径”。

短路求值：逻辑的副作用

calls = []
def side(n):
    calls.append(n); return n > 0

_ = False and side(1)
print(calls)        # []   ← side 根本没被调用

_ = True or side(2)
print(calls)        # []   ← 也没调用

and 左边为假，右边根本不执行；or 左边为真，右边也不执行。

这不是优化，这是语言定义的语义。而有副作用时，它改变程序的行为：

# 想每次调用都记日志，但写成了
if 用户已登录 and 记录日志():
    ...
# → 用户没登录时，日志根本不会记

逻辑运算不只是"算真假"，它还控制"算不算"。 这一条是从布尔代数进入程序的第一道门，也是最容易被"看起来等价"骗到的地方。

六、量词：off-by-one 是一个数学错误

两个量词

它们的否定关系容易记反：

¬(∀x. P(x))  ==  ∃x. ¬P(x)
¬(∃x. P(x))  ==  ∀x. ¬P(x)

为什么这条重要：它解释了「测试通过了」到底证明了什么。

测试通过 = 在测过的样本上，∀(样本). P 成立。 程序正确 = ∀(所有可能输入). P 成立。

你没测过的那些输入，不在"测试通过"这句话的覆盖范围里。

空集上的量词：真值表的后果

∀x ∈ ∅. P(x)  = True     （空集上的全称恒真）
∃x ∈ ∅. P(x)  = False    （空集上的存在恒假）

这不是定义，这是真值表的必然结果。 因为 ∀ 等价于「不存在反例」，而空集里当然没有反例。

所以这段代码是"正确"的：

def 检查全部合法(列表):
    return all(合法(x) for x in 列表)      # 空列表 → True

# 但业务上，你可能想要：空列表 → 拒绝
if 检查全部合法(用户提交的名单):
    批准()      # 空名单被批准了

这是"数学上正确、业务上错误"的典型。 要区分这两件事：∀ 在空集上的行为是数学定义的，不是 bug；你需要额外加一条 len(列表)>0 才是业务正确。

边界：开区间和闭区间

到这一节，“off-by-one"终于是可计算的了。

目标：判断 x 是否落在 [0, 10]（两端都含）。

def 错(x): return 0 < x < 10        # 写成开区间了
def 对(x): return 0 <= x <= 10

实测 x 从 −2 到 13：

两种写法差 2 个，正好是边界的那两个。

off-by-one 不是"手滑多打了一个符号”。它是一个量词范围写错了。 [0,10] 有 11 个整数，(0,10) 有 9 个。差的这 2 个是数学事实，不是运气。

所以正确的做法不是"检查一下有没有 <=/< 写错"，而是"每次写边界，先用具体的数点一遍"。 拿 0、10、11 三个值代进去，看结果对不对——两秒钟的事，能挡掉绝大多数 off-by-one。

七、把这一篇放回体系

上一篇给了八层目录，这一篇是第三层：怎么保证对。

这一篇真正讲的三件事

1. 测试和证明不是程度差别，是种类差别

测试是有限个样本，证明是无限个情况。测试多跑一百万次，也不会变成证明。

最后一行不是抬杠。 证明可以是对的，而你还是不懂——那是抄来的证明。

2. 循环不变量是"把归纳法装进代码"的标准做法

三段式：初始化成立 → 每轮保持 → 加上终止条件推出结论。

有了它，你不用跑 5 万个用例，看代码就知道哪错、为什么错。这一条我实测过：5 个二分变体，不变量能精确定位到"错在终止条件"还是"错在区间不缩小"还是"根本不终止"。

3. 「条件写反」是数学错误，不是手滑

• 德摩根律是恒等式——&& 取反只能变 ||，没有第二种对法
• ∀ 在空集上恒真——这是真值表的后果，不是实现选择
• off-by-one 是量词范围的错——[0,10] 就是 11 个整数

把这三条当成"数学事实"而不是"编码规范"，你的代码质量会变一个层次。 因为你会开始问"这个条件覆盖了哪些情况"，而不是"这个 if 看起来对不对"。

八、动手：六个实验

实验 1：穷举 5 个二分变体，看谁过

import itertools

def v1(a, x):                       # 闭区间（标准）
    lo, hi = 0, len(a)-1
    while lo <= hi:
        mid = (lo+hi)//2
        if a[mid] == x: return mid
        elif a[mid] < x: lo = mid+1
        else: hi = mid-1
    return -1

def v3(a, x):                       # 混搭：lo<hi 配 hi=mid-1
    lo, hi = 0, len(a)-1
    while lo < hi:
        mid = (lo+hi)//2
        if a[mid] < x: lo = mid+1
        else: hi = mid-1
    return lo if lo < len(a) and a[lo] == x else -1

def v5(a, x):                       # lo = mid（漏 +1）→ 死循环
    lo, hi = 0, len(a); n = 0
    while lo < hi:
        mid = (lo+hi)//2
        if a[mid] < x: lo = mid
        else: hi = mid
        n += 1
        if n > 100: return 'DEADLOOP'
    return lo if lo < len(a) and a[lo] == x else -1

for name, f in [('v1', v1), ('v3', v3), ('v5', v5)]:
    bad = dead = tot = 0
    for n in range(0, 9):
        for combo in itertools.combinations(range(12), n):
            a = list(combo)
            for x in range(-1, 13):
                tot += 1
                want = a.index(x) if x in a else -1
                got = f(a, x)
                if got == 'DEADLOOP': dead += 1
                elif got != want: bad += 1
    print(f"{name}: {tot} 例 → 答错 {bad}, 死循环 {dead}")

跑出来会是 v1: 0/0、v3: 7216/0、v5: 0/41562。

注意 v5 那一行的形状：答错 0，死循环 41562。 它从不给你错的答案，它只是不给你答案。

实验 2：让二分真的溢出（需要 C）

#include <stdio.h>
int main() {
    int lo = 2000000000, hi = 2100000000;
    printf("(lo+hi)   = %d\n", lo + hi);         // -194967296
    printf("(lo+hi)/2 = %d\n", (lo + hi) / 2);   // -97483648
    printf("正确 mid  = %d\n", lo + (hi - lo) / 2);  // 2050000000
    return 0;
}

三个数字，一个 bug。

想看得更完整，把上表那 5 轮 mid 序列打印出来——你会看到负数、正数、负数、正数来回跳，永远不收敛。

实验 3：证明"验证 10 万次也不是证明"

def isprime(x):
    if x < 2: return False
    i = 2
    while i*i <= x:
        if x % i == 0: return False
        i += 1
    return True

# A: n^2+n+41 —— 40 次全过，第 41 次错
print("A 首个合数:", next(n for n in range(200) if not isprime(n*n+n+41)))
# → 40，值是 1681 = 41×41

# B: 2^n-1 —— 4 次全过，第 5 次错
for n in [2, 3, 5, 7, 11, 13]:
    print(f"B n={n}: {2**n-1} {'素' if isprime(2**n-1) else '合'}")

# C: 求和公式 —— 10 万次全过，是真命题，但仍然不是证明
print("C 反例:", sum(1 for n in range(100001) if sum(range(1, n+1)) != n*(n+1)//2))

实验 4：空真让你的权限检查全通过

def 有权限(用户, 资源):
    return all(资源 in 用户.get('允许', [])
               for _ in [资源])        # 抽象成 all 的形式

空用户 = {'允许': []}
其他用户 = {'允许': ['文档A']}

print("空用户能访问文档A吗:", 有权限(空用户, '文档A'))      # ??? 

# 更直白的版本
print("all([]) =", all(x > 0 for x in []))                  # True
print("any([]) =", any(x > 0 for x in []))                  # False
print("空权限列表 =", all([]))                                # True ← 危险

实验 5：德摩根律 + 区间边界

from itertools import product

# 德摩根：穷举 4 种，看有没有违反
bad = sum(1 for a, b in product([True, False], repeat=2)
          if (not (a and b)) != ((not a) or (not b)))
print("德摩根违反次数:", bad)          # 0

# off-by-one：[0,10] 闭区间，两种写法的覆盖
lo, hi = 0, 10
错 = [x for x in range(-2, 14) if lo < x < hi]
对 = [x for x in range(-2, 14) if lo <= x <= hi]
print(f"开区间写法覆盖 {len(错)} 个: {错}")
print(f"闭区间写法覆盖 {len(对)} 个: {对}")

实验 6：短路求值的副作用

calls = []
def side(n):
    calls.append(n)
    return n > 0

False and side(1)
True or side(2)
print("被调用的:", calls)      # [] —— 两次都没调

# 对照：不是短路的位置
calls.clear()
side(1) and side(2)
print("被调用的:", calls)      # [1, 2]

九、带走的东西

一句话：

测试只能覆盖有限个情况，证明才能覆盖全部——而"全部"这件事，靠的是归纳法那两步（基础 + 归纳），不是靠多跑几次。

三句话：

1. “没测出错误"只能推出"没测出错误” —— 命题 B 前 4 次全过、第 5 次才错，就是活的例子。测试不是证明的"弱化版"，是另一种东西。
2. 循环不变量是把归纳法装进代码的标准做法 —— 三段式：初始化成立、每轮保持、加终止条件推出结论。有了它，你能看出"错在终止条件"还是"错在区间不缩小"，而不只是"错了"。
3. 「条件写反」是数学错误，不是手滑 —— 德摩根是恒等式，∀ 在空集上恒真是真值表的后果，off-by-one 是量词范围错。把这三条当数学事实，你会开始问"这个条件覆盖了哪些情况"。

一句话回答最开始那个问题

为什么那个二分 bug 能活 9 年？

因为：

• 测试覆盖不到（要 10 亿元素）
• 逻辑看起来对（数学上 (a+b)/2 确实在区间中间）
• 不变量在纸上成立、在 32 位整数上不成立

三个防线，全在这个 bug 面前失效了。 第四条防线是证明——但证明必须站在正确的脚下：你要证明的是 32 位整数上的程序，不是整数上的程序。

下一篇

（四）什么能算：机器算不出来的东西

从一个具体的程序开始：写一个程序，判断另一个程序会不会停下来。然后证明这件事做不到。

再往下是可计算性的全貌：为什么有些函数没有任何程序能计算、为什么"通用判定程序"必然不存在、为什么这件事对 AI 也成立。

这一篇会有点反常识——它证明的是"不可能"。但正是因为它，你才知道哪些努力是白费的。

深水区

• 逻辑入门：Rosen 那本离散数学的逻辑章（第 1 章），命题逻辑、量词、证明方法全在里面。
• 程序正确性：Bradley & Manna《The Calculus of Computation》、或 Hoare 1969 年那篇《An Axiomatic Basis for Computer Programming》——循环不变量就是这篇提出来的。
• 那个二分 bug 的原始出处：Joshua Bloch, Extra, Extra — Read All About It: Nearly All Binary Searches and Mergesorts are Broken（2006，Google Research Blog）。很短，值得看原文。
• 算不算"证明"：Dijkstra 的 EWD 系列笔记，尤其《A Discipline of Programming》，讲怎么从"为什么对"倒推出来写代码。

这些书我不做页码引用——不同版本页码不同，写了就是骗你。按书名和章节找。

附：本篇所有数字的来源

全部本机跑出来：Ubuntu / Python 3.8 / gcc 9.4 / x86-64。

二分穷举（数组 = {0..11} 长度 0–8 的全部子集，查询值 −1..12，共 53,158 例）：

• v1 闭区间：0 错 0 死循环
• v2 半开区间下界：0 错 0 死循环
• v3 lo<hi 配 hi=mid-1：答错 7,216（首例 [0,1,2] 查 1 得 −1）
• v4 上取整混搭：答错 11,674（首例 [0] 查 −1 抛 IndexError）
• v5 lo=mid：答错 0，死循环 41,562（78.2%）
• v6 (lo+hi)/2：Python 环境全过（不溢出）

二分迭代次数：n 从 10 到 20 万，1800 次查询平均 10.40 次，最多 18 次；最坏情况实测等于上界 ⌈log₂(n+1)⌉（n=10 万 → 17 次）。

C 溢出实测（lo=2000000000, hi=2100000000）：lo+hi = -194967296，(lo+hi)/2 = -97483648，正确 mid = 2050000000；buggy 版 mid 序列 −97483648 → 1001258176 → −596854559 → 751572721 → −721697287，永不收敛。

命题验证：

• A n²+n+41：n=0..39 全素数，n=40 → 1681 = 41×41
• B 2ⁿ−1：n=2,3,5,7 素；n=11 → 2047 = 23×89；n=13 → 8191 素
• C 求和公式：n=0..100000 反例 0 个

逻辑：德摩根 4 种组合违反 0 次；[0,10] 开区间覆盖 9 个 vs 闭区间 11 个；all([])=True、any([])=False；短路求值 False and side(1) 不调用。

你自己机器上跑出来的数字会略有不同（CPU、语言版本）。差一点不影响结论——结论是结构性的。