访谈/播客

Michael Freedman：压缩即一切（数学的本质就是压缩）

Michael Freedman: Compression Is All You Need

访谈/播客🎤 嘉宾：Michael Freedman（迈克尔·弗里德曼，菲尔兹奖得主）；主持人：Peter（彼得）⏱ 31:59👁 NA

菲尔兹奖得主 Michael Freedman 用「压缩」这一概念解释人类数学的本质，并通过分析 Lean 数学库 MathLib、建立幺半群（monoid）模型，论证人类数学是形式数学中可被压缩的那一小块多项式增长子集，进而探讨人类数学家应如何与 AI 协作。

核心要点

压缩是数学三千年来的核心机制：从位值记数法（用「位置」把指数级多的整数压进线性长度）到现代数学十几层叠加的抽象，本质都是压缩。
形式数学（所有可能的逻辑演绎）呈双指数级爆炸增长，而人类真正关心的数学（human mathematics）只是其中可被理解、可被压缩的极小一块。
团队把数学建模为幺半群，核心定理是：多项式增长的幺半群很容易压缩，指数增长的（如自由非交换幺半群）则抗拒压缩；由于 MathLib 显示数学高度可压缩，数学若用幺半群刻画必属于多项式增长类型。
对 MathLib 的统计分析发现：一个仅约 600 token 的「打包（wrapped）」陈述，完全「展开（unwrapped）」到 Lean 基本项后长度可达 10 的 104 次方（比古戈尔还大），体现了惊人的压缩比。
论文提出可量化的实用指标——还原压缩（unwrap/wrap 长度比，衡量抽象程度）和演绎压缩（证明长度/陈述长度比，衡量陈述所凝聚的数学功力），可供 AI 智能体在搜索证明时判断「地形」。
Freedman 认为人类与 AI 智能体处境相同：机器虽快百万倍，但面对古戈尔级别的空间仍无法暴力穷举，双方都需要靠直觉，因此必须协作发展直觉。

分章详解

引子：数学不是冰冷的逻辑，而是「软乎乎」的

主持人介绍 Freedman 的传奇经历：因攻克四维庞加莱猜想获菲尔兹奖，后创立微软 Station Q 开创拓扑量子计算，如今转向 AI 与数学。
新论文《Compression is All You Need》与 Logical Intelligence 的同事 Vitaly Aksyonov、Yev Bodnia、Michael Mulligan 合著，用代数模型回答三个问题：人类如何构建数学知识、人类数学与形式数学有何根本区别、未来数学家应如何与 AI 协作。
核心答案归结为一个词：压缩（compression）。

压缩是数学三千年的核心

压缩「发明于三千年前」，可能是数学的第一个伟大定理——位值记数法：用「1」放在不同位置就能表示 1、10、100，整数符号呈对数增长率，于是能用线性时间表达指数级多的整数。
Freedman 用研究生第一堂课的轶事说明抽象的层层压缩：D.C. Spencer 在黑板上写「设 Ω 为向量丛截面芽层（sheaf of germs of sections of a vector bundle）」，要理解这句话需逐层拆开向量丛、截面、芽、层、它们之间的映射、微分算子、再到符号（symbol）并据此分类双曲/抛物/椭圆方程——约十层抽象。
更底层还跳过了逻辑地基：从皮亚诺算术、自然数，加逆元得整数，取商得有理数，完备化得实数，取积得向量空间，局部黏合得流形（向量丛即其一例）。
结论：数学家「毫不费力地工作在地基之上十几层抽象」，并非因为微分方程不难，而是因为太多基础信息已被压缩。若用 Lean 等形式语言展开，所有底层都得被拆解。

用 MathLib 测量「人类数学」

团队以约 50 万行 Lean 代码的 MathLib 库作为「人类数学」的化身/代理（avatar），做统计分析：定理如何调用引理、定义如何相互嵌套，从而看到层级结构与压缩结构。
区分「打包（wrapped）」高层陈述与「展开（unwrapped）」到 Lean 基本项的形式；发现相当朴素的数学陈述展开后会变成极其庞大的树。
关键数据：一个 600 token 的打包陈述，展开后长度达 10 的 104 次方，大于古戈尔（Google/googol）——既显示形式展开的爆炸，也反衬概念带来的惊人压缩。
Freedman 坦言 MathLib 并非完美样本：数论与代数几何偏多，分析与拓扑偏少；但它远胜于「从公理出发做一切可能演绎」那种通向混乱的做法。
「到底」很容易判断：库本身就是结构化的，沿每个陈述的后代节点向下追溯（树状呈现 / tree presentation），直到终止于 Lean 原始项，按权重累加即得巨大数字。

幺半群玩具模型：多项式 vs 指数增长

借鉴数理物理的「玩具模型（toy model）」思路——像电磁学、量子力学、BCS 超导理论那样用极简模型抓住本质并具预测力，且常含物理上不可直接观测的成分（如电磁势、希尔伯特空间）。
模型选用幺半群（monoid）：类似群但不要求有逆元，最简单的例子就是自然数；在幺半群里加入「宏（macros）」即新概念，如 10 的幂这种带来压缩的宏。
可在模型中度量层级（要走多深进入宏）与压缩（用宏能把元素表示到多大的直径），并研究权衡：宏越多压缩越强，宏越少压缩越弱。
形式数学呈双指数增长：从 n 个原始项两两组合，数量按 n、n²、n⁴、n⁸、n¹⁶……连指数本身都在指数增长。
核心定理：多项式增长的幺半群极易压缩，指数增长的幺半群抗拒压缩（如两个无关生成元的自由幺半群 free monoid，需要极不节俭的巨大宏才能获得一点压缩）。因 MathLib 显示数学高度可压缩，故若用幺半群刻画，它必是多项式增长型。
为何幺半群能建模数学？因为数学就是「把东西拼起来」——搭积木、看是否契合、造出新东西；论文还提到放宽到不要求结合律的 magma，乃至各方向拼接的球状 magma（globular magma）。

宏的例子与压缩的「甜点区」

宏的典型例子是 10 的幂（位值记数法）；另一种是把整数写成完全平方数之和：据拉格朗日定理（及华林定理 Waring），每个整数都是四个平方数之和，于是用更稠密的宏只需四步就能表达任意整数。
这看似违反信息论，实则不然——表达那些平方数本身要耗费大量比特；说明宏集越稠密，每项能表达的越多。
论文制表考察宏集越来越「稀」时表达力如何衰减；10 的幂处于对数密度（约 1/n 密度）的「甜点区」，在节俭（宏别太大）与表达力（能展开很多）之间取得平衡。

人类的「品味」、PageRank 与重要性度量

机器每一步逻辑都引发指数爆炸，人类做数学却「直奔要点」、增长慢得多（多项式速率）；这种慢增长正体现人类的品味——这正是这门「实验科学」要去发现、要「给数学史做精神分析」的目标。
论文建议用 PageRank 式算法（本质是求马尔可夫链的均衡/某向量值 ODE 的吸引不动点）识别数学网络中高中心性的核心定义节点，但它需要全局结构知识。
更简单的局部指标：还原压缩（reductive compression）= 展开长度/打包长度，衡量抽象带来的「性价比」；演绎压缩（deductive compression）= 证明长度/陈述长度，衡量陈述凝聚了多少数学功力——如费马大定理一行可写完，却需约 500 页深奥证明、完全机器展开约 5000 页。
Freedman 指出 MathLib 组织成有向无环图（DAG），每个定理只有唯一证明，这其实是缺陷：数学需要保留同一定理的多个证明（因不知哪个能推广），理想的库应含多证明、含相似陈述及其相似度度量，从而对「哪些方程最重要」给出某种测度。
他们最初想直接测增长率（给定长度 L 有多少陈述）来判断是多项式还是指数，但 MathLib 太小，受「有限尺寸效应」干扰——长陈述数量初升后急降，并非因其稀少，而是触到了库的边缘；故改为间接地通过可压缩性来推断数学的几何。

更大的图景：智能、AI 时代与人机协作

标题即论点，刻意用大胆措辞以便被反驳、激发更好的讨论。
Freedman 谈选择此方向的动机：从文艺复兴、宗教改革、启蒙、科学革命、工业革命、高科技革命到 AI，「历史真的在走向某处」，奇点将至，「外星人来了——是我们自己造的」，他想以参与者而非旁观者身份进入新时代。
区分两类压缩：数学家用的是「局部压缩」（把符号组压成新符号，如 10 的幂）；Kolmogorov 研究的是基于算法的「全局压缩」（Kolmogorov 复杂度），但全局压缩不可计算、代价太大；二者之间或许存在新的思维模式有待开发。
比喻：去探索数学就像去徒步，出发前应带张地图、大致了解地形——你是在阿巴拉契亚山还是内华达山脉？山脉与河谷在哪？论文目标就是给出这种地形的一瞥，而模型给出的答案是「多项式结构」。
结语：人类与 AI 智能体「在同一条船上」，是朋友、有相似局限；机器虽快百万倍，但相对古戈尔级空间仍无法暴力穷举，须像人一样靠好的直觉，因此必须协作发展直觉。
片尾预告：几天内将在 arXiv 发布相关论文《Artificial Intelligence and the Structure of Mathematics》，作者为 Michael Douglas、Freedman、Barkeshli 及 Mike。

关键引述

“压缩，从直觉上说，是数学的核心，三千年来一直如此。（Compression, intuitively, is the core of mathematics and has been for 3,000 years.）”— Michael Freedman

“一个数学家毫不费力地工作在地基之上十几层抽象之处……并不是说思考微分方程很难，而是我们压缩了太多基础信息。（A mathematician effortlessly works at a dozen layers of abstraction above the foundation.）”— Michael Freedman

“多项式增长的幺半群很容易压缩，指数增长的幺半群抗拒压缩——这就是这篇论文的主题。（Polynomial growth monoids compress very easily; exponential growth monoids resist compression. That's the theme of the paper.）”— Michael Freedman

“你可以说外星人已经到了——是我们自己造出了它们。我想以参与者、而不是旁观者的身份进入这个时代。（You could say the aliens have arrived. We built them. I wanted to enter this era as a participant, not an observer.）”— Michael Freedman

“它们是我们的朋友，和我们有相似的局限。它们也许快百万倍，但同样无法靠暴力穷举去探索任何东西——它们得像我们一样拥有良好的直觉。（They're our friends and they have similar limitations to us... they still can't explore anything like by brute force. They have to have good intuition like we have.）”— Michael Freedman

术语 / 人物

Michael Freedman（迈克尔·弗里德曼） — 美国数学家，1986 年因证明四维庞加莱猜想获菲尔兹奖；曾创立微软 Station Q 开创拓扑量子计算，现于 Logical Intelligence 从事 AI 与数学研究。

压缩（Compression） — 用更少的符号/概念表达更多信息的机制；本片认为它是人类数学区别于全部形式演绎的本质特征。

人类数学 vs 形式数学（Human vs Formal Mathematics） — 形式数学指从公理出发的所有合法演绎（呈双指数爆炸）；人类数学指其中可被理解、可被压缩、人类真正关心的极小子集。Freedman 把 AI 智能体也归入「人类」一方。

MathLib — Lean 4 的大型数学定理库，约 50 万行代码，本研究用作「人类数学」的统计代理；组织为有向无环图（DAG）。

幺半群 / 宏（Monoid / Macro） — 幺半群是不要求有逆元的群状代数结构（最简例为自然数）；宏是加入的新概念/冗余生成元（如 10 的幂），能带来压缩。

打包/展开长度（Wrapped / Unwrapped length） — 打包长度是高层陈述的 token 数；展开长度是把所有定义递归展开到 Lean 基本项后的长度；二者之比衡量抽象/压缩程度。

Kolmogorov 复杂度（Kolmogorov complexity） — 基于最短生成算法的「全局」压缩度量，理论上不可计算；与数学家常用的「局部」压缩相对。

拉格朗日四平方和定理（Lagrange's / Waring's theorem） — 每个正整数都可表示为四个平方数之和（华林定理为其推广）；片中作为「更稠密宏集」的例子。

背景补充

Michael H. Freedman 是美国著名数学家，1986 年因证明四维庞加莱猜想获菲尔兹奖，是 20 世纪拓扑学的核心人物；他随后创立微软 Station Q 实验室，开创拓扑量子计算这一领域。本片讨论的论文《Compression is All You Need: Modeling Mathematics》（arXiv 2603.20396，2026 年）由 Vitaly Aksenov、Eve Bodnia、Freedman、Michael Mulligan 合著，部分定理由 Logical Intelligence 开发的 Lean 4 定理证明系统 Aleph 形式化验证，并有多种 LLM 参与证明。论文核心论点是：人类数学是形式数学这一双指数级空间中可压缩的多项式增长子集，可用幺半群建模并通过 MathLib 数据加以检验。

适合谁看

适合对 AI 与数学、自动定理证明、形式化数学（Lean/MathLib）、数学哲学与「智能本质」感兴趣的研究者、研究生与技术读者；也适合关注人机协作做科研未来的从业者。