把《计算机科学中的数学》系统性地“断言代码化”一遍，是最近这段时间我觉得最值的一次阅读实验。所谓断言代码化，说白了就是不再满足于在纸面上看懂每条定理，而是把书里的定义、引理、定理全部改写成可执行代码里的 assert 语句，让计算机帮我做大量随机验证。这个做法听起来挺硬核，其实门槛极低，而且它给我带来的东西远超预期：不仅逼着我逐字抠清了证明的每个前提，还让我意外发现了几个自己原本理解偏了的细节。如果你也收藏过不少数学书却总是“一读就会、一合就忘”，这篇经验可能正是你需要的。
1. 断言代码化到底在化什么：从“看懂证明”到“让证明跑起来”
1.1 数学书阅读里的“完成幻觉”
我很长一段时间读数学书都用同一种方式：跟着证明走一遍，把关键步骤画线，感觉“逻辑是通的”，然后翻到下一节。问题在于，这个“通了”的感觉非常不可靠。书上的证明省略了大量边界条件，比如某个变量默认是正整数、某个集合默认非空、某个运算默认无符号溢出。作者不会恶意挖坑，但读者会下意识地用自己的直觉把漏洞填平，而这种填补往往和教材的真实要求并不一致。
断言代码化就是用来击碎这种“完成幻觉”的。它的核心动作极其简单：把书里每一句“若满足条件A，则结论B成立”翻译成代码，让程序在大量随机输入上检查“A为真时B是否为真”。一旦断言失败，就说明要么我翻译错了，要么我对前提的理解少了某一条。两者都是非常有价值的发现。相比之下，传统阅读方式下这些歧义会一直被隐藏到做题或考试时，而大部分读者并不会自觉去补做那么多习题。
1.2 assert 是最好用的形式化工具
很多人一听“形式化”就想到大型证明助手，觉得成本很高。但断言代码化的关键是只用 assert 这一个轻量原语。assert 在工程上本来就是表达“这里必须为真”的运行时检查，用在阅读场景里，它恰好构成了一种“可执行的三段论”：
- 大前提：某个数学命题 P 成立；
- 小前提：当前这组随机输入 x 满足 P 的所有前件；
- 结论：执行 assert，确认后件也成立。
拿生活类比，这就像你请了一位极其较真的校对员。他不看你的文字解释，只看你给的条件，然后机械地检查结果。这位校对员不会给你人情分，也不会因为你自认为懂了就放你一马。只要有一条边界条件没写清楚，他立刻翻脸。
纸面证明和断言代码之间最大的差异，我列成了一张表，每次给别人介绍这个方法时都会拿出来：
| 对比维度 | 纸面证明阅读 | 断言代码验证 |
|---|---|---|
| 反馈速度 | 靠读者自己脑内判断 | 程序运行即出结果 |
| 前提遗漏 | 容易被跳过 | 断言条件会明确写出 |
| 多次输入 | 通常只看一个典型例子 | 随机/穷举大量样本 |
| 对错判定 | 主观“感觉通了” | 客观通过或失败 |
| 学习成本 | 只需数学基础 | 十几行 Python 就能开始 |
这张表想说明的是，断言代码化不是为了替代严谨的数学证明，而是给阅读过程增加一层低成本、高密度的反馈。它不会给你“证出来了”的绿色通行证，但能非常高效地告诉你“你理解成的那个定理，大概率不是书上那个”。
2. 阅读工具链搭建：一个十几行的验证骨架
2.1 为什么用 Python 而不是更正式的工具
我身边有朋友第一反应是：要验证数学定理，为什么不上手专业证明器？我的回答是，目的不同。专业证明器追求的是把整个证明树形式化，让机器完全确认推导合法性，这对我来说学习成本和阅读投入都太高了，适合严谨验证某个重要结论，不适合快速扫完一本教材并形成整体直觉。
Python 在阅读场景里有三个不可替代的优点。首先是可读性，数学表达式转写过来几乎不需要额外解释。其次是生态，random、itertools、math 这三个标准库就能覆盖大部分随机验证需求。第三是心理负担小，你不会有“必须写出完整证明”的压力，而敢频繁去验证那些看起来显然成立的小命题，这种高频小验证恰恰是形成直觉的关键。
2.2 验证骨架长什么样
我在实践里没有引入复杂的测试框架，而是写了一个极简的检查工具集合，核心思路是“随机生成输入，检查断言，失败则打印反例”。整个骨架大概十几行，我把它贴在下面：
import random def trial(runner, n=10000): """随机跑 n 次验证，遇到反例立即终止并打印。""" for i in range(n): sample = runner() try: assert sample.valid, f"反例 #{i}: {sample}" except AssertionError as e: print(e) return print(f"通过 {n} 次随机验证") def check_if(label, cond_factory, n=10000): print(f"[验证] {label}") trial(cond_factory, n)这个骨架里，runner返回一个带有valid属性的小对象，或者返回(value, expected)的元组。我用一个更朴素的版本时会让 runner 返回布尔值，但后来发现布尔值太粗糙，反例出现时你根本看不出输入是什么，于是改成返回带样本信息的对象。实际中我常写一个小数据类：
from dataclasses import dataclass @dataclass class Case: n: int a: int b: int valid: bool这只是为了让反例输出更友好。核心思想始终是：验证函数本身只是一个布尔表达式的求值器，最重要的事情是随机样本的质量。
2.3 按书的章节组织验证脚本
刷整本书不能一把梭，我按章节建立了独立文件，约定章号体现在文件名里，比如ch04_number_theory.py、ch06_graph.py。每个文件里再用字典或者一系列check_if调用组织成“验证清单”。这样做的好处有两个：一是跑起来有节奏感，一章一章地推进，像在完成一个长期任务；二是每章验证代码本身就是我的笔记，将来回看时能快速知道当年我把哪条定理理解成了什么样子。
我还给自己定了一条规则：每个验证目标必须有一行注释，写清楚它对应书里的哪段命题，比如“Lecture 4 Theorem 7”这类。这个习惯在后期回查时帮了大忙，因为代码写多了之后，单看函数名根本想不起来当初想验证什么。
关键操作逻辑是：先写定义，再写命题，最后跑随机验证。如果你发现某个断言怎么都过不去，先别怀疑书，把你自己写的条件逐字念一遍，八成是少了一个“互素”或者“非空”的前件。
3. 数论部分的实证：同余、辗转相除与素数幂余数定理
3.1 同余运算的传递性验证
数论章节是断言代码化的最佳试验场，因为几乎所有命题都有清晰的前件后件。我做的第一个验证是同余的传递性：若 a ≡ b (mod m)，且 b ≡ c (mod m)，则 a ≡ c (mod m)。初看这几乎是废话，但用代码写出来就会发现，你必须在随机生成 a、b、c、m 时保证前件真的成立，而不是仅仅取模后相等。
我的生成方式很直接：随机选 m 和 b，然后把 a、c 分别写成 b 加上任意整数倍的 m。这样前件天然满足。然后断言a % m == c % m。这个实验本身不会失败，但它教会了我一件事：构造满足前件的随机样本比验证后件更重要。很多断言失败的根本原因是前件构造得不对，而不是定理有错。
3.2 辗转相除法与贝祖等式的组合断言
接着我写了 gcd 的递归实现，并验证它的递推不变式：gcd(a, b) == gcd(b % a, a)。这个比同余传递性有意思，因为它涉及一个真实算法。我不光验证结果，还验证了所谓的贝祖等式：存在整数 x、y 使得gcd(a, b) == a*x + b*y。
这里有一个代码层面的坑：直接随机暴力搜索 x、y 是不现实的，所以我实现了一个扩展辗转相除法，返回(g, x, y)。随后验证的重点变成：算出来的 g 确实等于a*x + b*y，并且 g 确实整除 a 和 b。真正跑起来后，我第一次意识到“最大公因数”不是靠试除得到的，而是可以从线性组合里长出来的。这个体验比看十遍证明都深刻。
def extended_gcd(a, b): if b == 0: return a, 1, 0 g, x1, y1 = extended_gcd(b, a % b) x = y1 y = x1 - (a // b) * y1 return g, x, y def check_bézout(): def runner(): a = random.randint(1, 1000) b = random.randint(1, 1000) g, x, y = extended_gcd(a, b) case = Case(a, b, g, g == a*x + b*y and g % a == 0 and g % b == 0) return case check_if("贝祖等式", runner, n=20000)这个例子后来被我反复用来说明断言代码化的价值：如果不把 x、y 的线性组合结果写进断言，只看 gcd 的数值对不对，等于只验证了最表层的一半结论。贝祖等式的证明在纸面上只有几行，但亲手让它跑起来，你才真正理解“最大公因数”和“整数线性组合”之间的等价关系是多么反直觉的结论。
3.3 素数幂余数定理：从固定小样本到随机互素样本
数论里另一个经典结论是：对于素数 p 和任意整数 a，若 a 不是 p 的倍数，则 a 的 p-1 次方模 p 等于 1。我验证的方式是随机选择素数 p，再随机选一个与 p 互素的 a，断言pow(a, p-1, p) == 1。Python 的pow天然支持模幂运算，效率很高，所以跑几十万次也没有压力。
真正让我觉得警示的是，如果我忘了“a 不是 p 的倍数”这个前件会怎样。我把代码改成随机任意 a，立刻就会见到大量反例。比如 p=7 时取 a=14，模 7 等于 0，结果显然不是 1。那一刻我顿悟：书上写的“a 与 p 互素”不是可选项，而是定理成立的生命线。这种“通过主动破坏前件来观察反例”的玩法，是纸面阅读很难获得的经验。
为了再进一步，我还扩展验证了更一般的 φ(n) 形式：对任意正整数 n，取与 n 互素的随机 a，断言pow(a, phi(n), n) == 1，其中phi是数论里的欧拉函数。验证它比素数情形难，因为你需要正确实现 φ(n) 的定义。等我把 φ(n) 的实现和定理断言一起跑通时，整段数论章节基本就没有模糊地带了。
4. 图论章节的难点：先造对象，再谈验证
4.1 为什么图论验证比数论麻烦得多
数论里的对象是整数，随机生成非常容易。图论的验证麻烦在于，你需要随机生成“合法的图”，并且很多定义之间是强耦合的。比如你想验证“连通无环图一定满足边数等于顶点数减一”，就必须先能生成连通无环图；你想验证欧拉回路判定条件，就必须先能生成各种度分布不同的图。生成器一旦写错，后面的断言全部白跑。
我的做法是把图的生成器分成三层：第一层生成随机图，第二层生成随机连通图，第三层生成随机树。最底层用邻接表表示，每层都在生成后做基础断言，确保生成器本身可信。这一步很枯燥，但它是图论验证能否进行的地基。
def random_tree(n): if n <= 1: return {i: [] for i in range(n)} adj = {i: [] for i in range(n)} for i in range(1, n): parent = random.randrange(i) adj[i].append(parent) adj[parent].append(i) return adj def is_connected(adj): n = len(adj) seen = {0} stack = [0] while stack: v = stack.pop() for u in adj[v]: if u not in seen: seen.add(u) stack.append(u) return len(seen) == n def is_acyclic(adj): n = len(adj) visited = set() for start in range(n): if start in visited: continue stack = [(start, -1)] while stack: v, p = stack.pop() if v in visited: return False visited.add(v) for u in adj[v]: if u != p: stack.append((u, v)) return True写完这三个函数，我顺手补了一个断言：随机生成的树必须同时满足连通、无环、边数为 n-1 这三个性质。如果这里没过，后面的所有实验都没有意义。
4.2 树的三条等价定义，一次跑通
教材里会提到树的多种等价描述，比如“连通且无环”“连通且边数等于 n-1”“无环且边数等于 n-1”，这三者通常被证明为等价。我在代码里真正验证时，发现一个容易忽略的点：从“连通且边数等于 n-1”推“无环”时，必须小心孤立点。一个只有两个连通分量、边数恰好为 n-2 的图，加上一条连接这两个分量的边后，边数变成 n-1 且连通，但它一定无环吗？如果你把“环”定义成简单环，这个结论没问题；但如果你忘了限制图必须简单，那平行边就会制造长度为 2 的“环”，一下子破坏等价性。
通过这样的验证实验，我深刻体会了数学教材里“图”是指简单无向图这个默认假设有多重要。纸面上一个“图”字带过，代码里可是会出人命的。我把树的三条性质循环验证了上万次，每次生成新的随机树，再分别计算三个布尔属性，然后断言三者真值相等。运行通过的那一刻，这个区域在我脑子里才算真正焊死。
4.3 奇偶度路径判定：用构造算法验证充要条件
图论章节里更有挑战性的是欧拉回路和欧拉路径的判定：所有非零度顶点连通 + 奇度顶点数为 2，则存在一笔画路径；奇度顶点数为 0，则存在一笔画回路。我决定不只验证判定条件，还顺手实现了 Hierholzer 算法来构造路径，然后用断言检查构造出的路径确实覆盖每条边一次。
这个步骤是断言语义化的高阶玩法：断言本身很难直接“证明”存在性，但如果你能构造出一个候选答案，则“存在”立刻变成了“可验证”。我的验证流程是：随机生成图 → 统计奇度顶点数和连通性 → 如果满足路径条件，就调用构造算法得到路径 → 断言路径长度等于边数，并且每条边在路径中恰好出现一次。
代码里最麻烦的是维护边的使用状态。我踩过一个坑：用邻接表返回路径时，如果只用端点判断边是否重复，平行边会导致误判。正确做法是给每条边编号，在路径里记录边的 ID。这个坑让我多花了一个晚上，但收获是理解了“存在性证明”和“构造性证明”之间的区别。书上说存在一条路径时，读者往往意识不到这里其实藏着一个算法问题。
5. 从断言失败中反推教材前提：计数、概率章节给我上的课
5.1 鸽巢原理的边界条件竟然也有学问
鸽巢原理应该是计数章节最直观的命题：把 n+1 个物体放进 n 个盒子，至少有一个盒子装了至少两个物体。我一开始觉得这有什么好验证的，直接随机随机放鸽子就行。结果我的第一版断言写得太大意：我只断言“至少存在一个盒子非空”。这当然永远成立，但根本没有抓住原意。
修正后，我的断言改成“至少存在一个盒子，其容量大于 floor(n/m)”，其中 m 是盒子数。这个看似显然的事实，一旦你遇到分布极为平均、余数正好等于 1 的边界情况，代码就会给你好看。我还尝试断言强的形式：最大盒子里的物体数至少是 ceil(n/m)。随机验证轻松通过，但真正让我警醒的是，如果我把物体数改成 n-1 而不是 n，这个断言偶尔会在随机验证里失败——因为可能出现每个盒子恰好一个的情况。
这段经历让我养成了一个习惯：任何断言都要先写清楚前提，测试条件里不允许出现“差不多、显然、很容易看到”这种模糊词汇。
5.2 生日问题概率公式的容差设定
概率章节的验证比计数更微妙，因为随机实验的结果是频率而不是真值。第一次我尝试断言理论概率公式和模拟频率严格相等，结果当然一次次失败。后来我才意识到自己犯了一个概念错误：有限次采样得到的频率本身就服从一个分布，断言它等于理论值是荒谬的。
正确的做法是给频率一个置信区间。我选了 50000 次模拟，断言模拟频率落在理论值 ±0.01 的范围内。这个容差不能设得太松，否则断言失去意义；也不能太紧，否则运行时间不够时偶尔会有小幅越界。我最终通过多次运行，确认了 0.01 的容差在 50000 次模拟下相当稳定。
这段经历让我对“定理成立”和“实验吻合”的关系有了更深理解。断言代码化在这个场景里的角色，不是证明理论公式，而是证明我对公式的实现没有理解错。如果实现错了，偏差会明显超过容差；如果实现对了，即使有小幅波动，也会大致贴着理论值走。
5.3 期望线性性质的验证让我理解了“独立”的真实地位
概率论里有一个特别反直觉的结论：对任意两个随机变量 X 和 Y，无论是否独立，都有期望的可加性。这个结论我每次看书都觉得懂了，每次合上书又觉得哪里不对劲。借着断言代码化，我干脆写了两个不独立的随机变量做测试。
具体做法很简单：先随机掷一个骰子得到 X，然后让 Y 的取值依赖于 X，比如 Y = 2X。这种情况下两者明显不独立，但我可以轻松验证E[X+Y] == E[X] + E[Y]。随机模拟的均值当然稍有偏差，所以我用同样的区间容差方法，断言两个均值之差的绝对值不超过某个阈值。
等代码跑完，我忽然真正接受了“期望可加性不要求独立”这件事。纸上的证明推导我也看过，但人脑对“不独立则相关”的本能警惕会导致理解扭曲。有了运行结果作为外部反馈，这个心结才算解开。某种意义上，断言代码化最擅长处理的正是这种“道理都知道，直觉却拧巴”的概念。
6. 有限验证的边界：断言通过不等于定理成立
6.1 随机验证的反例价值高于正例价值
随着验证的章节变多，我越来越清楚地意识到一个边界：随机测试通过只能说明“我没找到反例”，并不能证明“反例不存在”。这就像你在池塘里捞了一圈没捞到鱼，不能说池塘里绝对没有鱼。尤其当对象空间足够稀疏时，随机采样很可能错过那些精心构造才能触达的边界情况。
但反过来，随机验证找到反例的价值是决定性的。只要出现一个反例，就足以推翻“我的理解版本”。在我实践过程中，绝大多数有价值的发现都来自反例，而不是通过验证。因为通过只能让你安心，反例则会直接告诉你哪个条件漏了、哪个定义歪了、哪个推导里的“显然”其实并不显然。
所以我在组织验证脚本时，刻意保留了每个测试的反例输出格式。一旦assert失败，程序会打印完整的输入样本。这个习惯让我后来排查问题时节省了大量时间，而不是看着一个古老的“False”发呆。
6.2 断言失败通常是“我写错了”，而不是“书错了”
这是我在整个阅读过程中最深刻的体会：上百次断言失败里，没有一次能真的证明教材有错。失败几乎都源自我的实现或我对前提的转述有误。最常见的是三种情况：一是生成器没有正确模拟前件，比如我压根没保证输入连通；二是实现某个函数时边界条件出错；三是我把一个定理的充分条件错记成了充要条件，导致验证时用了一个过强的断言。
理解了这一点后，我的心态从“跑验证找书的问题”转变为“跑验证找自己的问题”。这个转变很关键，它让断言代码化从一种检验工具变成了一种学习方法。每失败一次，我反而离正确理解更近一步。回到数学阅读的语境里，这种“失败引导发现”的节奏，和做题、对照答案、订正错题的过程异曲同工，只是电脑把订正环节提前到了阅读阶段。
6.3 哪些章节适合断言化，哪些不适合
在实际操作后，我总结出适合断言语义化的章节特征：命题的前件后件清晰、对象可以方便地随机生成、定义可以用代码结构精确表示。数论、图论、计数、离散概率这些章节高度适合。相反，如果某个章节涉及连续统、极限或者抽象代数中的无限结构，单纯用有限随机验证就会显得特别尴尬。
比如书里如果有关于实数序列收敛的讨论，直接暴力采样意义不大，因为你根本无法在有限步骤里模拟“无穷多个后续项”。对于这类内容，我会退回到传统证明阅读，只用断言代码验证一些离散的有限特例。这是取舍，而不是缺陷。断言代码化本质上是给“有限数学对象”准备的高亮笔，用它去读连续数学，战斗力会打折。
6.4 给打算照做的朋友的三条建议
如果读者也想把一本数学教材扫一遍，我的建议很具体。第一，不要追求一次把所有命题都验证完，从一章里挑五六个最核心的定理开始，跑通后建立信心，再逐步扩展。第二，生成器的质量永远排在验证脚本的前面，先写几个“生成器自检断言”，确认生成的对象合法，再开始验证定理。第三，务必养成保存反例的习惯，但不要急着改断言去“修掉”反例——先回去翻书，看是不是遗漏了前提条件，这个回溯过程才是成长发生的地方。
我在整个实验中真正获得的，不是“这本书我已经验证过”的虚荣感，而是一种更谦卑的学习节奏：每一个断言都在逼我承认自己以为懂了的那些部分其实还值得推敲。现在回头再看那些画满线的纸页，我反而会觉得，真正的笔记不在纸上，而在那几十个能跑的验证文件里。
