主题演讲

压缩即一切：为数学建模

Compression is all you need: Modeling mathematics

主题演讲🎤 Michael Freedman（迈克尔·弗里德曼，菲尔兹奖得主）；合作者 Vitaly Aksenov、Eve Bodnia、Mike Mulligan⏱ 10:55👁 NA

▶ 在 YouTube 观看

用单体（monoid）这一简单玩具模型刻画数学的可压缩性，论证人类数学是形式数学海洋中那个可被层级化压缩的小角落，并据此为自动推理提供指引。

核心要点

人类数学（human math）只是形式数学（formal math，即所有可能推导的全集）中极小的一个子集，其显著特征是层级嵌套带来的可压缩性。
用单体（monoid）作为数学推理的玩具模型：阿贝尔单体（A，类似自然数、顺序无关）增长缓慢呈多项式，自由单体（F，顺序重要）则呈指数级爆炸。
在多项式增长的阿贝尔单体里，稀疏的宏（macro/新符号）就能带来指数级乃至无限的表达力（如位值记号、Waring 定理）；在指数增长的自由单体里，即使稠密的宏也几乎无济于事。
以约 50 万元素的 MathLib 作为人类数学的代理，实测发现其行为出人意料地像稀疏宏 + 多项式增长的阿贝尔单体，而非天真预期的自由单体。
由此推断：人类数学是形式数学中那个可压缩的区域；可借助压缩相关指标（reductive compression、证明长度）配合 PageRank 来指导 premise selection 等自动推理任务。

分章详解

两类数学：人类数学 vs 形式数学

区分人类数学（human math，即 arXiv 上我们熟悉的数学）与形式数学（formal math，所有可能推导构成的更大空间）。
人类数学只是这片广阔海洋中的一个小角落、小子集。
核心问题：如何在这片汪洋中识别出这个小子集？讲者主张其关键特征是层级嵌套（hierarchical nesting）及由此带来的压缩。
这一思想并非新事：几千年前的位值记号（place notation）就体现了通过引入新符号来压缩表达。

记号与单体模型

设定原始字母表为一元记号（unary）G，新引入的符号集称为宏集（macro set）M，二者合成增广字母表。
把数学推导看作从前提到结论的有向无环图（DAG），将其压平为字符串，再用单体（monoid，类似群但无逆元）来建模这些推导串。
考虑两种最简单的单体：阿贝尔单体（abelian monoid A，类似自然数，字符顺序无关、只看重数）与自由单体（free monoid F，非阿贝尔，字符顺序至关重要）。
直觉上数学推导（参数顺序关键）应对应自由单体，但讲者将论证数学的可压缩性反而更像阿贝尔单体。

理论计算：宏集的杠杆效应

度量：给定单体与宏集，新符号能带来多大的表达力提升。两类单体存在强烈二分（dichotomy）。
阿贝尔单体中可表达事物仅呈多项式（缓慢）增长；自由单体中则呈指数级增长，是巨大的推导空间。
在位值记号这一例子中，稀疏的宏集就能在阿贝尔单体里买来指数级表达力；放宽到稍大的宏集，借助 Waring 定理（与拉格朗日四平方和定理相关）甚至可达无限表达力。
反观自由单体：即便宏集非常稠密也几乎换不来什么；要获得超线性增长，几乎得给所有元素都命名，从而失去压缩的意义。

用 MathLib 做实证检验

以 MathLib（带依赖关系的元素集合）作为人类数学的代理，约 50 万个元素；其元素分两类：lean 原语（粗略类比公理）与命名定理（macro set）。
为每个元素关联三个长度尺度：wrapped length（定义该元素的 lean 代码 token 数）、unwrapped length（递归展开到底层原语所需的原语数）、depth（元素到原语的最长链长）。
实测结果：unwrapped length 随 depth 呈指数增长（在 log-y 轴上呈线性）；而 wrapped length 仅随 depth 呈线性增长。
与各玩具模型对比：天真预期相关的自由单体并不能捕捉这些扩张性质；唯一能较好吻合的，恰是位值记号式的阿贝尔单体。
结论：MathLib 的行为像是处在多项式增长单体中、配以稀疏宏集。

把压缩用于指导自动推理

若压缩是人类数学的固有属性，便可用它来指导 AI 智能体（agent）。
提出两个基于压缩的指标：T0（reductive compression，衡量定义的压缩能力）；以及某个项/陈述是否拥有长证明（可能与陈述深度相关）。
上述是单个元素的局部属性，无法体现定理之间的重要性差异；修正办法是在 MathLib 依赖图上做标准 PageRank，并用这些压缩指标加以偏置。
推测：从该 PageRank 不动点得到的分数或可用于 premise selection（前提选择），留待未来验证。

总结：人类数学是形式数学的可压缩区域

稀疏宏集在多项式增长单体中威力强大，在指数增长单体中则乏力。
MathLib 数据显示：unwrapped length 相对 depth/wrapped length 呈指数增长，而 wrapped length 相对 depth 则平坦或弱线性。
据此推断：人类数学是形式数学中那个可被压缩的区域。

关键引述

“人类数学是这片广阔海洋（形式数学）中的一个小角落、小子集；我会论证它的一个特征正是层级嵌套及其带来的压缩。”— Michael Freedman

“你天真地会以为数学应该属于后者（自由单体，参数顺序至关重要），但出人意料的是，我会展示数学具有这种可压缩性，反而更像顺序无关紧要的阿贝尔单体。”— Michael Freedman

“唯一能较好吻合的一行，竟是阿贝尔单体里那个简单的位值记号例子。”— Michael Freedman

“由此我们推断：人类数学是形式数学中那个可压缩的区域。”— Michael Freedman

术语 / 人物

Michael Freedman（迈克尔·弗里德曼） — 菲尔兹奖（1986）得主，因证明四维庞加莱猜想而闻名；现为数学-AI 创业公司 Logical Intelligence 的首席科学官。

形式数学（formal math） — 所有可能的形式推导构成的全集，是一个极其庞大的空间；人类数学只是其中的小子集。

单体（monoid） — 类似群但没有逆元的代数结构；可视为一个字母表加上组合字符成词的规则，用作数学推导的玩具模型。

阿贝尔单体 / 自由单体（abelian / free monoid） — 阿贝尔单体中字符顺序无关（类似自然数），表达力多项式增长；自由单体中顺序重要，表达力指数增长。

宏集（macro set, M） — 在原始字母表之上引入的新符号集合（对应数学中的定义/命名定理），用来压缩表达式、扩展表达力。

MathLib — 基于 Lean 的大型数学形式化库（约 50 万元素、带依赖关系），讲者用作人类数学的实证代理。

wrapped / unwrapped length 与 depth — MathLib 元素的三个度量：定义代码的 token 数、递归展开到底层原语的原语数、到原语的最长依赖链长。

premise selection（前提选择） — 自动定理证明中为目标命题挑选相关前提/引理的任务，讲者设想用压缩指标加权的 PageRank 分数来辅助。

背景补充

主讲人 Michael Freedman 是 1986 年菲尔兹奖得主（证明四维庞加莱猜想），曾长期在微软 Station Q 从事拓扑量子计算研究，现为数学-AI 创业公司 Logical Intelligence 的首席科学官，该公司 CEO 为本演讲合作者 Eve Bodnia。本演讲基于其与 Vitaly Aksenov、Eve Bodnia、Mike Mulligan 合作的论文《Compression is all you need: Modeling Mathematics》（arXiv 2603.20396，2026），并在哈佛 CMSA 等场合宣讲。论文以物理学家式的玩具模型（有限生成单体）刻画数学的可压缩性，并用 Lean 的 MathLib 库做实证对照。

适合谁看

适合关注自动定理证明、形式化数学（Lean/MathLib）、数学基础与 AI for Math 的研究者与工程师，以及对用简单代数模型理解数学结构感兴趣的数学物理爱好者。