种子公式全录（下）：ZFC 九条公理与 Wiedijk 百定理全枚举——数学的 DNA 与考卷

上篇《种子公式全录（上）》收了大众正典层的 22 条。这篇往金字塔底部走，收更硬核的两层——而且这两层之间的”压缩比”被真实测量过：Metamath 项目把”从公理到名定理”的每一步推导都形式化了，结论是：9 条 ZFC 公理，经过 12,151 条中间定理的台阶，撑起 Wiedijk”形式化 100 定理”清单上的名定理（2016 年 6 月统计）。光是从公理构造出复数系——让 $e^{i\theta}$ 里那个 $i$ 合法存在——就要 3,014 条定理。公理是 DNA，不是说明书；本篇把 DNA（ZFC 九条）和考卷（Wiedijk 百条）全部枚举，每条给精确写法。

先立好整个系列的金字塔，本篇覆盖加粗的两层：

压缩档位	数量	收录处
公理层（ZFC）	9 条	本篇第一部分
大众正典层	22 条	上篇
学界基准层（Wiedijk）	100 条	本篇第二部分
支撑骨架层	12,151 条	Metamath 数据库（机器可读，不适合人读）

第一部分：ZFC 九条公理——数学的 DNA

ZFC = Zermelo–Fraenkel 集合论 + Choice（选择公理）。它的语言极端贫瘠：一阶逻辑，外加唯一一个非逻辑符号 $\in$（属于）。自然数、实数、函数、矩阵、$e^{i\pi}+1=0$——全部要用”集合的集合的集合”从这九条搭出来。记号约定：$\forall$（任意）、$\exists$（存在）、$\exists!$（存在唯一）、$\land$（且）、$\lor$（或）、$\Rightarrow$（蕴含）、$\Leftrightarrow$（当且仅当）、$\varnothing$（空集）。以下形式写法与 Wikipedia ZFC 条目一致。

公理 1：外延公理（Extensionality）

$\forall x\,\forall y\,\bigl[\forall z\,(z \in x \Leftrightarrow z \in y) \Rightarrow x = y\bigr]$

人话：元素完全相同的两个集合就是同一个集合。集合没有”包装”——只看内容。

公理 2：正则公理（Regularity / Foundation）

$\forall x\,\bigl(x \neq \varnothing \Rightarrow \exists y\,(y \in x \land y \cap x = \varnothing)\bigr)$

人话：每个非空集合都含有一个与自身不相交的元素。后果：不存在”自己属于自己”的集合（$x \in x$ 被禁止），也不存在无穷下降链 $\cdots \in x_2 \in x_1$。这是对罗素悖论时代疯狂集合的驱逐令。

公理 3：分离公理模式（Specification / Separation）

$\forall z\,\forall w_1 \cdots \forall w_n\,\exists y\,\forall x\,\bigl[x \in y \Leftrightarrow \bigl(x \in z \land \varphi(x, w_1, \ldots, w_n, z)\bigr)\bigr]$

人话：从已有集合 $z$ 中，用任何一条性质 $\varphi$ 筛出子集 $\{x \in z : \varphi(x)\}$。关键限制是必须在已有集合内部筛——不允许凭空定义”所有满足 $\varphi$ 的东西的集合”，罗素悖论（“所有不属于自身的集合的集合”）正是这样被拆除的。

公理 4：配对公理（Pairing）

$\forall x\,\forall y\,\exists z\,\bigl((x \in z) \land (y \in z)\bigr)$

人话：任给两个集合 $x, y$，存在一个同时包含它俩的集合。配合分离公理即可精确裁出 $\{x, y\}$。

公理 5：并集公理（Union）

$\forall \mathcal{F}\,\exists A\,\forall Y\,\forall x\,\bigl[(x \in Y \land Y \in \mathcal{F}) \Rightarrow x \in A\bigr]$

人话：对任何”集合的集合” $\mathcal{F}$，存在一个囊括其所有成员之元素的集合；配合分离公理裁出精确的 $\bigcup \mathcal{F}$。

公理 6：替换公理模式（Replacement）

$\forall A\,\forall w_1 \cdots \forall w_n\,\bigl[\forall x\,(x \in A \Rightarrow \exists! y\,\varphi) \Rightarrow \exists B\,\forall x\,\bigl(x \in A \Rightarrow \exists y\,(y \in B \land \varphi)\bigr)\bigr]$

人话：集合 $A$ 在任何”可定义函数”下的像仍是集合。这是搭建超穷层级（很大很大的无穷）的脚手架。

公理 7：无穷公理（Infinity）

$\exists X\,\bigl[\varnothing \in X \land \forall y\,(y \in X \Rightarrow S(y) \in X)\bigr]$

人话：存在一个包含 $\varnothing$ 且对后继运算 $S(y) := y \cup \{y\}$ 封闭的集合——即存在无穷集。自然数就在这里诞生：$0 := \varnothing$，$1 := \{\varnothing\}$，$2 := \{\varnothing, \{\varnothing\}\}$，……上篇第 1 条 $1+1=2$ 的原材料，由这条公理供货。

公理 8：幂集公理（Power Set）

$\forall x\,\exists y\,\forall z\,(z \subseteq x \Rightarrow z \in y)$

人话：任何集合的全部子集也构成一个集合（$z \subseteq x$ 是 $\forall w\,(w \in z \Rightarrow w \in x)$ 的缩写）。它是”越来越大的无穷”的引擎：由康托定理（下文考卷第 63 题），$\mathcal{P}(x)$ 永远严格大于 $x$。

公理 9：选择公理（Choice，以良序定理形式）

$\forall X\,\exists R\,(R \text{ 良序化 } X)$

人话：任何集合都能被排成”每个非空子集都有最小元”的次序；等价的更常见说法：任何一族非空集合，都存在一个”从每个集合里各取一个元素”的选择函数。九条中最有争议的一条——它保证了选择的存在却给不出选择的方法，还会推出分球悖论（一个球拆成五块拼出两个同样大的球）这类怪胎，但现代数学离开它寸步难行。

符号精准的三条注记

1. “九条”其实数不清：第 3、6 条是公理模式（axiom schema）——对每一条一阶公式 $\varphi$ 各有一条实例，所以严格说 ZFC 有可数无穷条公理（且已证明它不能被有限条公理化）。“9”数的是模式。
2. 弱形式：配对、并集、幂集三条按 Wikipedia 的写法都只断言”存在一个包含目标的集合”（注意式中是 $\Rightarrow$ 而非 $\Leftrightarrow$），精确的 $\{x,y\}$、$\bigcup\mathcal{F}$、$\mathcal{P}(x)$ 由分离公理事后裁出。很多教科书直接写强形式，两者等价。
3. 不是极简清单：分离公理模式可由替换公理模式推出，配对公理也可由替换+幂集推出——保留它们是历史与教学习惯。所以”最少要几条”的答案比 9 还小。

第二部分：Wiedijk 百定理——学界公认的考卷

Freek Wiedijk 维护的”Formalizing 100 Theorems”清单是形式化数学界的标准考卷：各大证明系统（Lean、Rocq/Coq、Isabelle、Metamath……）以拿下清单上的定理数为能力标尺。截至目前，100 条中 99 条已在至少一个系统中被计算机逐步验证，唯一悬着的是第 33 题费马大定理——Kevin Buzzard 团队正在 Lean 中形式化它（2024 年起的五年项目）。

以下 100 条，编号与名称照录原清单，陈述为标准精确形式。约定：$\mathbb{N}, \mathbb{Z}, \mathbb{Q}, \mathbb{R}, \mathbb{C}$ 依次为自然数、整数、有理数、实数、复数集；$p$ 无说明时指素数；$\gcd$ 为最大公约数；$a \mid b$ 记”$a$ 整除 $b$“。

第 1–10 题

#	名称	精确陈述
1	$\sqrt{2}$ 无理	$\sqrt{2} \notin \mathbb{Q}$：不存在整数 $p,q$ 使 $(p/q)^2 = 2$
2	代数基本定理	每个次数 $\geq 1$ 的复系数多项式在 $\mathbb{C}$ 中至少有一个根
3	有理数可数	存在双射 $\mathbb{N} \leftrightarrow \mathbb{Q}$，即 $\lvert\mathbb{Q}\rvert = \aleph_0$
4	勾股定理	直角三角形：$a^2 + b^2 = c^2$（$c$ 为斜边）
5	素数定理	$\pi(x) \sim \dfrac{x}{\ln x}$，即 $\lim_{x\to\infty} \dfrac{\pi(x)\ln x}{x} = 1$（$\pi(x)$ 为不超过 $x$ 的素数个数）
6	哥德尔不完备定理	任何一致、可递归公理化、包含初等算术的理论 $T$，存在语句 $G$：$T \nvdash G$ 且 $T \nvdash \neg G$
7	二次互反律	奇素数 $p \neq q$：$\left(\dfrac{p}{q}\right)\left(\dfrac{q}{p}\right) = (-1)^{\frac{p-1}{2}\cdot\frac{q-1}{2}}$（Legendre 符号）
8	三等分角与倍立方不可能	尺规可作数的次数必为 $2$ 的幂；而 $[\mathbb{Q}(\sqrt[3]{2}):\mathbb{Q}] = 3$、$\cos 20°$ 的次数为 $3$，故二者尺规不可作
9	圆面积	$A = \pi r^2$
10	欧拉–费马定理	$\gcd(a,n)=1 \Rightarrow a^{\varphi(n)} \equiv 1 \pmod{n}$（$\varphi$ 为欧拉函数）

第 11–20 题

#	名称	精确陈述
11	素数无穷多	素数集合无限（欧几里得：任给有限素数表，$p_1\cdots p_n + 1$ 的素因子不在表中）
12	平行公设独立	存在满足欧氏其余公理但平行公设不成立的模型（双曲几何），故平行公设不可由其余公理证明
13	多面体公式	凸多面体：$V - E + F = 2$
14	巴塞尔问题	$\displaystyle\sum_{n=1}^{\infty} \frac{1}{n^2} = \frac{\pi^2}{6}$
15	微积分基本定理	$f$ 连续时 $\dfrac{d}{dx}\displaystyle\int_a^x f(t)\,dt = f(x)$；且 $\displaystyle\int_a^b f = F(b) - F(a)$（$F' = f$）
16	高次方程不可根式解	次数 $\geq 5$ 的一般多项式方程不存在根式求根公式（Abel–Ruffini）
17	棣莫弗定理	$(\cos\theta + i\sin\theta)^n = \cos n\theta + i\sin n\theta$（$n \in \mathbb{Z}$）
18	刘维尔定理与超越数构造	代数数不可被有理数”过好”地逼近；由此 $\displaystyle\sum_{k=1}^{\infty} 10^{-k!}$ 是超越数（第一个被证明超越的数）
19	四平方和定理	每个自然数都是四个整数的平方和：$n = a^2+b^2+c^2+d^2$（Lagrange）
20	费马二平方定理	奇素数 $p$ 可写成两平方和 $\Leftrightarrow p \equiv 1 \pmod 4$

第 21–30 题

#	名称	精确陈述
21	格林定理	$\displaystyle\oint_{\partial D} (L\,dx + M\,dy) = \iint_D \Bigl(\frac{\partial M}{\partial x} - \frac{\partial L}{\partial y}\Bigr)\,dA$
22	连续统不可数	$\lvert\mathbb{R}\rvert > \aleph_0$：实数不能与自然数一一对应（康托对角线法）
23	勾股数公式	本原勾股三元组恰为 $(m^2-n^2,\ 2mn,\ m^2+n^2)$，其中 $m>n\geq 1$，$\gcd(m,n)=1$，$m,n$ 一奇一偶
24	连续统假设不可判定	CH（$\aleph_0$ 与 $2^{\aleph_0}$ 之间无中间基数）在 ZFC 中既不可证（Cohen 1963）也不可否证（Gödel 1940）
25	Schröder–Bernstein 定理	若存在单射 $A \to B$ 与单射 $B \to A$，则存在双射 $A \leftrightarrow B$
26	莱布尼茨 π 级数	$1 - \dfrac{1}{3} + \dfrac{1}{5} - \dfrac{1}{7} + \cdots = \dfrac{\pi}{4}$
27	三角形内角和	欧氏平面中 $\alpha + \beta + \gamma = 180°$
28	帕斯卡六边形定理	内接于圆锥曲线的六边形，三组对边（所在直线）的交点共线
29	费尔巴哈定理	三角形的九点圆与内切圆内切，与三个旁切圆均外切
30	选票问题	甲得 $p$ 票、乙得 $q$ 票（$p>q$），计票全程甲严格领先的概率为 $\dfrac{p-q}{p+q}$

第 31–40 题

#	名称	精确陈述
31	拉姆齐定理	$\forall r,s\ \exists N$：$N$ 个顶点完全图任意红蓝染色，必含红色 $K_r$ 或蓝色 $K_s$
32	四色定理	任何平面地图可用 4 种颜色染色使相邻区域异色（1976 计算机辅助证明，2005 年在 Coq 中全形式化）
33	费马大定理	$n \geq 3$ 时 $x^n + y^n = z^n$ 无正整数解（Wiles 1995；本清单唯一未形式化的一条）
34	调和级数发散	$\displaystyle\sum_{n=1}^{\infty} \frac{1}{n} = \infty$
35	泰勒定理	$f(x) = \displaystyle\sum_{k=0}^{n} \frac{f^{(k)}(a)}{k!}(x-a)^k + R_n$，余项 $R_n = \dfrac{f^{(n+1)}(\xi)}{(n+1)!}(x-a)^{n+1}$（某 $\xi$ 介于 $a,x$ 之间）
36	布劳威尔不动点定理	连续映射 $f: B^n \to B^n$（$n$ 维闭球）必有不动点 $f(x) = x$
37	三次方程解	$x^3 + px + q = 0$ 的根 $x = \sqrt[3]{-\frac{q}{2} + \sqrt{\frac{q^2}{4} + \frac{p^3}{27}}} + \sqrt[3]{-\frac{q}{2} - \sqrt{\frac{q^2}{4} + \frac{p^3}{27}}}$（Cardano）
38	均值不等式	$x_i \geq 0$：$\dfrac{x_1 + \cdots + x_n}{n} \geq \sqrt[n]{x_1 \cdots x_n}$，等号当且仅当全相等
39	佩尔方程	$D$ 为非平方正整数时，$x^2 - Dy^2 = 1$ 有无穷多组正整数解
40	闵可夫斯基定理	$\mathbb{R}^n$ 中关于原点对称的凸体体积 $> 2^n$，则必含非零整点

第 41–50 题

#	名称	精确陈述
41	皮瑟定理	代数方程 $f(x,y)=0$ 的解支可展为 $x$ 的分数幂级数（Puiseux 级数）
42	三角形数倒数和	$\displaystyle\sum_{n=1}^{\infty} \frac{2}{n(n+1)} = 2$
43	等周定理	平面闭曲线周长 $L$、围面积 $A$：$L^2 \geq 4\pi A$，等号当且仅当圆
44	二项式定理	$(x+y)^n = \displaystyle\sum_{k=0}^{n} \binom{n}{k} x^k y^{n-k}$
45	欧拉分拆定理	把 $n$ 分拆成奇数部分的方案数 = 分拆成两两不同部分的方案数
46	四次方程解	一般四次方程存在根式解（Ferrari：化归三次预解式）
47	中心极限定理	$X_i$ 独立同分布，均值 $\mu$、方差 $\sigma^2 < \infty$：$\dfrac{\sqrt{n}(\bar{X}_n - \mu)}{\sigma} \xrightarrow{d} N(0,1)$
48	狄利克雷定理	$\gcd(a,d)=1$ 时，等差数列 $a, a+d, a+2d, \ldots$ 含无穷多素数
49	凯莱–哈密顿定理	方阵代入自己的特征多项式得零矩阵：$\chi_A(A) = O$
50	正多面体恰五种	正四、六、八、十二、二十面体，再无其他（可由第 13 题欧拉公式推出）

第 51–60 题

#	名称	精确陈述
51	威尔逊定理	$n \geq 2$：$n$ 为素数 $\Leftrightarrow (n-1)! \equiv -1 \pmod{n}$
52	子集个数	$\lvert\mathcal{P}(S)\rvert = 2^{\lvert S\rvert}$：$n$ 元集恰有 $2^n$ 个子集
53	π 超越	$\pi$ 不是任何整系数多项式的根（Lindemann 1882；推论：化圆为方不可能）
54	柯尼斯堡七桥	连通图存在欧拉回路 $\Leftrightarrow$ 每个顶点度数为偶；七桥图四个顶点全为奇度，故无解
55	弦段乘积定理	圆内两弦交于 $P$：$PA \cdot PB = PC \cdot PD$
56	Hermite–Lindemann 定理	$\alpha$ 为非零代数数 $\Rightarrow e^{\alpha}$ 超越
57	海伦公式	$s = \frac{a+b+c}{2}$：三角形面积 $A = \sqrt{s(s-a)(s-b)(s-c)}$
58	组合数公式	$\dbinom{n}{k} = \dfrac{n!}{k!\,(n-k)!}$
59	大数定律	$X_i$ 独立同分布、$E\lvert X_1\rvert < \infty$：$\bar{X}_n \to \mu$（弱：依概率；强：几乎必然）
60	裴蜀定理	$\exists x, y \in \mathbb{Z}$：$ax + by = \gcd(a,b)$

第 61–70 题

#	名称	精确陈述
61	塞瓦定理	$D,E,F$ 在三边上：$AD, BE, CF$ 共点 $\Leftrightarrow \dfrac{BD}{DC} \cdot \dfrac{CE}{EA} \cdot \dfrac{AF}{FB} = 1$
62	公平赌局定理	鞅（公平赌局）中任何有界停时策略的期望收益等于本金——不存在必胜的离场时机（可选停时定理）
63	康托定理	任何集合严格小于其幂集：$\lvert S\rvert < \lvert\mathcal{P}(S)\rvert$——无穷有无穷多个等级
64	洛必达法则	$f,g \to 0$（或 $\to\infty$）且 $\lim \frac{f'}{g'}$ 存在 $\Rightarrow \lim \dfrac{f}{g} = \lim \dfrac{f'}{g'}$
65	等腰三角形定理	两边相等的三角形，两底角相等
66	几何级数和	$\lvert r\rvert < 1$：$\displaystyle\sum_{n=0}^{\infty} ar^n = \frac{a}{1-r}$
67	e 超越	$e$ 不是任何整系数多项式的根（Hermite 1873）
68	等差级数和	$a_1 + a_2 + \cdots + a_n = \dfrac{n(a_1 + a_n)}{2}$
69	辗转相除法	$\gcd(a, b) = \gcd(b,\ a \bmod b)$，迭代至余数为 $0$（欧几里得算法，可证其正确性与终止性）
70	完全数定理	偶数 $N$ 为完全数（等于自身真因子之和）$\Leftrightarrow N = 2^{p-1}(2^p - 1)$ 且 $2^p - 1$ 为素数（Euclid–Euler）

第 71–80 题

#	名称	精确陈述
71	拉格朗日定理（群论）	有限群 $G$ 的子群 $H$：$\lvert H\rvert$ 整除 $\lvert G\rvert$
72	西罗定理	$p^k$ 为整除 $\lvert G\rvert$ 的最大 $p$ 幂：$p^k$ 阶子群存在，全体共轭，个数 $\equiv 1 \pmod p$
73	单调子列定理	长度 $\geq rs+1$ 的互异实数列，必含长 $r+1$ 的递增子列或长 $s+1$ 的递减子列（Erdős–Szekeres）
74	数学归纳法原理	$\bigl[P(0) \land \forall n\,(P(n) \Rightarrow P(n+1))\bigr] \Rightarrow \forall n\, P(n)$
75	中值定理	$f$ 在 $[a,b]$ 连续、$(a,b)$ 可导 $\Rightarrow \exists c \in (a,b)$：$f'(c) = \dfrac{f(b)-f(a)}{b-a}$
76	傅里叶级数	适当条件下周期 $2\pi$ 函数 $f(x) = \dfrac{a_0}{2} + \displaystyle\sum_{n=1}^{\infty} (a_n \cos nx + b_n \sin nx)$，系数 $a_n = \frac{1}{\pi}\int_{-\pi}^{\pi} f\cos nx\,dx$ 等
77	k 次幂求和	$\displaystyle\sum_{i=1}^{n} i^k$ 是 $n$ 的 $k+1$ 次多项式，首项 $\frac{n^{k+1}}{k+1}$，系数由伯努利数给出（Faulhaber）
78	柯西–施瓦茨不等式	$\lvert\langle u, v\rangle\rvert \leq \lVert u\rVert \cdot \lVert v\rVert$，等号当且仅当线性相关
79	介值定理	$f$ 在 $[a,b]$ 连续，$y$ 介于 $f(a)$ 与 $f(b)$ 之间 $\Rightarrow \exists c \in [a,b]$：$f(c) = y$
80	算术基本定理	每个整数 $n \geq 2$ 唯一地（不计次序）分解为素数之积

第 81–90 题

#	名称	精确陈述
81	素数倒数和发散	$\displaystyle\sum_{p \text{ 素数}} \frac{1}{p} = \infty$（比”素数无穷多”强得多）
82	立方体分割定理	不可能把立方体分割为有限个两两大小不同的小立方体（Littlewood 称其证明”优雅”）
83	友谊定理	若任意两人恰有一个共同朋友，则存在认识所有人的人（Erdős–Rényi–Sós）
84	莫雷角三分线定理	任意三角形相邻内角三等分线的三个交点构成等边三角形
85	被 3 整除判别法	$3 \mid n \Leftrightarrow 3 \mid (n$ 的十进制各位数字之和$)$
86	勒贝格测度与积分	存在平移不变、完备的测度 $\lambda$ 使 $\lambda([a,b]) = b-a$；相应积分严格扩张黎曼积分
87	德萨格定理	两三角形对应顶点连线共点（透视于点）$\Leftrightarrow$ 对应边交点共线（透视于线）
88	错排公式	$D_n = n! \displaystyle\sum_{k=0}^{n} \frac{(-1)^k}{k!}$（$n$ 个信封全装错的方案数，$\approx n!/e$）
89	因式与余式定理	多项式 $p(x)$ 除以 $(x-a)$ 的余数为 $p(a)$；$(x-a) \mid p(x) \Leftrightarrow p(a) = 0$
90	斯特林公式	$n! \sim \sqrt{2\pi n}\,\Bigl(\dfrac{n}{e}\Bigr)^n$

第 91–100 题

#	名称	精确陈述
91	三角不等式	$\lvert x + y\rvert \leq \lvert x\rvert + \lvert y\rvert$（度量空间版：$d(a,c) \leq d(a,b) + d(b,c)$）
92	皮克定理	顶点在格点上的简单多边形：面积 $A = I + \dfrac{B}{2} - 1$（$I$ 内部格点数，$B$ 边界格点数）
93	生日问题	23 人中存在两人同生日的概率 $\approx 0.507 > \dfrac{1}{2}$（365 天等可能）
94	余弦定理	$c^2 = a^2 + b^2 - 2ab\cos C$（$C=90°$ 时退化为勾股定理）
95	托勒密定理	圆内接四边形 $ABCD$：$AC \cdot BD = AB \cdot CD + BC \cdot AD$
96	容斥原理	$\Bigl\lvert\bigcup_{i=1}^{n} A_i\Bigr\rvert = \displaystyle\sum_i \lvert A_i\rvert - \sum_{i<j} \lvert A_i \cap A_j\rvert + \cdots + (-1)^{n+1}\lvert A_1 \cap \cdots \cap A_n\rvert$
97	克拉默法则	$\det A \neq 0$ 时 $Ax = b$ 的唯一解为 $x_i = \dfrac{\det A_i}{\det A}$（$A_i$：以 $b$ 替换第 $i$ 列）
98	伯特兰假设	$\forall n \geq 1\ \exists$ 素数 $p$：$n < p \leq 2n$（Chebyshev 证明）
99	蒲丰投针	针长 $\ell \leq$ 平行线距 $d$：针与线相交的概率 $P = \dfrac{2\ell}{\pi d}$（由此可用投针估算 $\pi$）
100	笛卡尔符号法则	实系数多项式的正根个数（计重数）不超过系数符号变化数，且两者之差为偶数

读这张考卷的四个角度

1. 它与上篇的接缝。 第 4 题勾股、第 13 题多面体公式直接就是上篇的 #2 与 #6；第 17 题棣莫弗定理 $(\cos\theta + i\sin\theta)^n = \cos n\theta + i\sin n\theta$ 则是欧拉公式的整数次影子——“转 θ 转 n 次 = 转 nθ”，比欧拉公式早半个世纪就被写下。三层金字塔不是三个世界，是同一批种子在不同分辨率下的照片。

2. 它是一张真的在被批改的考卷。 各系统得分（不同时间点的统计）：Lean 84 条、Rocq/Coq 80 条、Metamath 74 条、Isabelle 等紧随其后；合计 99/100。第 33 题费马大定理是唯一空格——人类 1995 年就证完了，机器还要再等几年。这个空格本身就是知识点：“已被人类接受”与”已被机器逐步核验”之间，隔着一个数量级的严格性。

3. 它暴露了”简单”与”深刻”互相独立。 第 65 题（等腰三角形底角相等）小学生能懂，第 24 题（连续统假设不可判定）需要整个现代集合论——它们并排坐在同一张清单上。而且第 24 题是清单里最特殊的一条：它不是”证明了什么”，而是”证明了不能证明”——ZFC 这套 DNA 里压根不含 CH 的答案，公理层的边界被它精确标出。

4. 数一数你已经拥有几条。 中国高中数学大致覆盖：#4、9、11、27、38、44、55、58、61、65、66、68、74、79、89、91、94；本科数学再加二三十条。换句话说，这张人类文明的考卷，你可能已经握着三分之一——种子公式从来不是远方的圣物，它们大多早就在你手里，只是没人告诉你它们在这张清单上。

参考来源

清单与形式化进度

• Formalizing 100 Theorems — Freek Wiedijk（百定理原始清单）
• Formal Proof — Getting Started（AMS Notices, 2008）（Wiedijk 对清单的说明）
• Missing theorems — Lean community、100 theorems in Lean（Lean 进度：84 条，仅费马大定理未竟）
• Formalizing Fermat’s Last Theorem in Lean（Buzzard 五年项目）
• Formalizing 100 theorems in Rocq（Rocq/Coq 进度：80 条）
• Metamath 100（Metamath 进度 74 条；12,151 条支撑定理与复数构造 3,014 条的统计出处）

公理层

• Zermelo–Fraenkel set theory — Wikipedia（九条公理的形式写法）
• Metamath Proof Explorer（从 ZFC 公理机器可验证地推出全部数学的实践）

本站姊妹篇

• 《种子公式全录（上）：大众正典 22 条》
• 《欧拉公式：不是一个数，是”旋转”的名字》