可压缩性（Compressibility）is all you need

#algorithms #podcast #ai #compression

在这篇由 Michael Mulligan 演讲的视频中，核心观点是“人类数学（Human Math）”与“形式数学（Formal Math）”的根本区别在于其具备极高的“可压缩性（Compressibility）”。演讲者通过引入群论中的幺半群（Monoids）作为玩具模型，并结合 Lean 语言的数学库（Mathlib）进行实证研究，论证了人类数学是通过层次嵌套的定义和定理被高度压缩的。

以下是视频内容的超详细拆解：

1. 核心概念引入：人类数学 vs 形式数学

形式数学（Formal Math）： 包含了所有逻辑上合法的推导和证明的庞大空间。这个空间是极其巨大的，甚至可以说是呈指数级爆炸增长的。
人类数学（Human Math）： 人类真正发现、理解并记录在论文或库（如 arXiv）中的数学，只是形式数学这一浩瀚汪洋中一个非常小的子集 [00:00:21]。
核心问题： 我们如何在这片汪洋中精准定位并识别出“人类数学”这块小角落？演讲者提出，高层次的嵌套定义（Hierarchical Nesting）和由此带来的“压缩性”，就是人类数学最显著的特征 [00:00:52]。

2. 理论模型：基于“幺半群”的逻辑模拟

为了量化证明这种“压缩”是如何工作的，研究团队利用幺半群（Monoids）建立了一个模拟数学推导的玩具模型（将推导树展平成字符流/字符串）[00:02:16]。他们对比了两种极端的幺半群：

阿贝尔幺半群（Abelian Monoid）：
类似于自然数加法，字符的顺序不重要，只看字符出现的次数（多重集）。
空间增长非常缓慢，属于多项式级增长空间（Polynomial-growth space） [00:02:59]。
自由幺半群（Free Monoid）：
非交换律，字符的排列顺序至关重要（就像真正的逻辑推论一样，步骤顺序不能错）。
空间极其庞大，呈指数级增长空间（Exponential-growth space） [00:03:21]。

“宏（Macros）”的引入与杠杆效应

在模型中，他们引入了“新符号”或“定义”（即宏集 $M$），这类似于人类数学中不断发明新概念（如定义了加法后定义乘法，再定义幂）。

在阿贝尔幺半群中： 引入一个稀疏的宏集（少量的定义），就能带来指数级的表达能力（Expressivity）（即“位值表示法 Place notation”）；如果引入稍微大一点的宏集，甚至能利用“华林问题（Waring's theorem）”获得无限的表达能力 [00:04:51]。
在自由幺半群中： 即使你引入一个非常密集的宏集，也几乎无法获得额外的表达效率。要想表达更多东西，你几乎必须为每一个元素都单独命名，这让“定义新符号”失去了意义 [00:05:35]。

直觉上，数学推导应该更像“自由幺半群”（顺序至关重要），但实验结果却带来了一个惊人的反直觉结论。

3. 实证研究：Lean 数学库（Mathlib）的数据表现

为了验证理论，团队将 Lean 语言的 Mathlib（包含约 50 万个数学元素）作为“人类数学”的代理数据集进行测量 [00:06:01]。他们为库中的每个数学元素（定理/定义）测量了三个核心指标 [00:06:47]：

包裹长度（Wrap Length）： 该元素在 Lean 代码中被定义时的原生 Token 数量（即人类看到的定理简写长度）。
解包长度（Unwrap Length）： 如果把该定理中用到的所有定义、定理递归地拆解还原到最底层的公理/元始概念（Primitives），最终需要的总总 Token 数。
深度（Depth）： 从该定理出发，通过依赖链条倒推回底层公理所需的最长路径。

令人震惊的测量结果：

解包长度（Unwrap Length） vs 深度： 随着深度增加，定理完全解包后的长度呈现明显的指数级爆炸增长 [00:07:29]。
包裹长度（Wrap Length） vs 深度： 尽管解包后是个天文数字，但人类代码中的包裹长度却基本保持线性增长（极其平缓） [00:08:04]。

这意味着，人类数学在不断向深处推进时，通过层层套娃式的“新定义”，成功把一个逻辑上呈指数级爆炸的复杂结构，压缩成了人类大脑和代码能够处理的线性复杂度。

4. 模型对比与最终结论

当把 Mathlib 的真实数据与前面的幺半群玩具模型进行匹配时，结果如下 [00:08:13]：

绝大多数模拟自由幺半群（非交换、重视顺序）的模型全部宣告失败，无法解释这种高压缩比。
奇特的是，唯一能和真实数据良好匹配的，正是那个看似简单的阿贝尔幺半群（位值表示法） [00:08:41]。

最终推论： 人类数学在形式数学的无边海洋中，表现得就像是一个“在多项式增长空间中拥有稀疏宏集的特例”。人类数学的本质就是寻找可压缩的逻辑结构 [00:08:51]。

5. 未来展望：指引 AI 自动推理（Automated Reasoning）

既然“压缩性”是人类数学的灯塔，那我们能不能用它来指导 AI 证明智能体（Agents）呢？演讲者提出了一个具体构想 [00:09:02]：

建立压缩指标： 设计“还原压缩比（Reductive compression）”等指标，评估一个定义在压缩复杂性上的贡献；或者评估一个精简的陈述是否对应一个很深的证明。
结合 PageRank 算法： 在 Mathlib 的依赖图上运行标准 PageRank（网页排名）算法，但将上述“压缩指标”作为权重偏置（Bias）注入进去 [00:09:42]。
应用场景： 通过这个加权后的 PageRank 计算出固定点分数，未来或许能极大地帮助 AI 在进行定理证明时进行“前提选择”（Premise Selection，即让 AI 知道证明当前定理时，哪些已知的定理和概念是最重要、最相关的） [00:10:08]。