菲尔兹奖得主Michael Freedman揭示数学本质：压缩就是一切，AI数学协作新视角

当谈及数学时，我们近乎本能地认为它是一个严谨、精确、不容置疑的完美逻辑体系。但在菲尔兹奖得主迈克尔・弗里德曼（Michael Freedman）看来，人类真正创造和关心的数学，本质上是「柔软且可塑」的。

迈克尔・弗里德曼是当代最具影响力的数学家之一，曾因解决四维庞加莱猜想获得菲尔兹奖，这一成果被视为拓扑学领域的里程碑。此后，他的研究并未停留在纯数学领域，而是转向应用前沿，创立了 Microsoft StationQ，成为拓扑量子计算的重要推动者。近年来，他又将研究兴趣延伸至人工智能，尝试用数学视角理解人类知识的结构与生成机制。

想象一下，一个仅需600个token写就的命题，展开后的长度竟能达到10的104次方——这是一个比古戈尔（googol）还要庞大的天文数字。这并非科幻，而是弗里德曼及其团队在分析现代数学形式化库Mathlib时发现的真实现象。

这种将庞大的演绎链条凝练为简洁概念的能力，揭示了一个被数学家们使用了三千年、却很少被言明的秘密：数学的本质，或许不是证明，而是压缩。

近日，弗里德曼在论文中直接提出了这一宣言：「压缩，就是你所需要的全部」（Compression is all you need）。

在近期的一次访谈中，弗里德曼阐述了这一观点，并探讨了人类数学直觉与机器逻辑之间的鸿沟。他认为，人类数学数千年的演进，本质上是一部不断创造“宏”、构建抽象层级的压缩史。从三千年前的位值表示法，到现代复杂的微分方程，人类文明一直在进行着“数据压缩”实验。

人类从事数学，从来不是在穷举推理路径，而是在一个近乎无限的可能性空间中，不断寻找可以被压缩的结构。相比之下，当前的人工智能则更倾向于“穷举”。因此，在AI发展的关键阶段，理解“压缩”这一机制，或许正是人类与AI在数学领域实现真正协作的起点。

以下是经调整的访谈主要内容：

主持人：我们通常认为数学是一个严密、完美的逻辑体系，但你的研究似乎指出，人类实际使用的数学并非如此。能否请你从“压缩”这个概念开始解释？

迈克尔・弗里德曼：当然。我们的论文中有一个小玩笑：压缩其实早在三千年前就被发明了，这可能就是数学的第一个伟大定理——位值记数法。

例如，“10”可以用一个“1”放在特定位置来表示，“100”也是如此。通过将“1”置于不同位置，我们能用极少的符号表示极大的数。这种表示方式让整数的表达实现了对数级增长，却能在有限符号中涵盖指数级数量的数。这是一种极其强大的压缩，它甚至与现代物理中的一些思想（如自旋链状态）相关。但压缩远不止于数字表示，它贯穿整个数学体系。

主持人：能否举一个更具体的例子？

迈克尔・弗里德曼：我大学时第一次上微分方程课，教授在黑板上写下一个巨大的Ω符号，并说它是“向量丛截面的芽层”。那一刻，我甚至不知道什么是向量丛。后来我才意识到，要理解这句话，你需要理解背后多层嵌套的概念：向量丛、截面、层、芽，以及它们之间的映射关系。如果再深入追溯，还涉及自然数、整数、有理数、实数、向量空间、流形等基础结构。

也就是说，数学家在思考时，其实是站在十几层抽象之上。这就是为什么微分方程“看起来不难”，因为海量的信息已经被压缩在这些高层概念之中。这就是“压缩”的力量：大量信息被隐藏在高层概念里。

而如果你用Lean这类形式化语言来表达，就必须把这些压缩全部展开。所以可以说：压缩是数学的核心，而且已经存在了三千年。

在论文中，我们试图将这种直觉量化。我们使用Lean的数学库（Mathlib，约50万行代码）作为“人类数学”的一个近似模型，对其结构进行了统计分析：观察定理如何调用其他引理，定义如何复合与嵌套。我们可以看到一种清晰的分层和压缩结构，它使得Mathlib中的命题能以高层级（“包装态”）编写，随后可展开为基础Lean术语（“解包态”）。

我们研究了两者的关系，发现这种层次结构能将相对简单的数学命题，变成源自基础Lean术语的、极其庞大的树状结构。

主持人：我记得这能达到一个非常巨大的数字：10的104次方，对吧？这是否意味着你想强调，这本质上就是数学的核心？

迈克尔・弗里德曼：是的。我们将这个库中的内容视为人类数学行为的一个良好样本——尽管它在各数学领域的分布并不完美（例如数论和代数几何的内容远多于分析或拓扑）。它并非人类数学思想的完美副本，但它与“从一组公理出发进行每一种可能的逻辑推演”截然不同，后者会导致“混沌数学”。

无论如何进行形式化，结构的发现都会呈双指数级增长。最终的结果正如你所说，我们在Lean库中找到的最长的“解包命题”，其大小约为10的104次方，比古戈尔（10的100次方）还要大。而它对应的“包装命题”只有600个token。这展示了惊人的膨胀，但反过来也揭示了通过使用抽象概念所能获得的巨大压缩比。

我想说的是，数学家和他们的智能体（AI）实际上在同一条船上。但当你看到像古戈尔这样的数字时，即使我们的机器比我们快一百万倍，这个倍数在古戈尔的尺度下也微不足道。

所以，真正的问题不是人类与机器将探索什么，而是在庞大的形式推理空间中，哪一部分可以被压缩成我们和智能体都能够理解的形式（我称之为“形式数学”）。我相信，人类数学（在此我将我们的智能体也视为“人类”的一部分）正是如此。

主持人：在你们分析的这些结构中，是否发现存在某些方程或过程，不具备与其他事物相同的“公分母”？如果是这样，如何决定什么是“最基础”的？或者说，如何知道自己已经“触底”？

迈克尔・弗里德曼：对于Lean来说，很容易知道什么时候“触底”，因为它的库结构就是如此设计的。

基本上，存在一些原始项，你可以用它们来构建更复杂的命题。这个“展开后长度”有时被称为树表示法。你审视每个命题的子节点（即它由什么构建），再看那些子节点的子节点，形成一棵越来越深的树，直到它终止于原始的Lean项。之后，我们为所有节点分配权重（原始项权重为1，上层节点权重由其调用的下层节点权重累加）。当把树顶层的权重加起来时，就得到了展开后命题的那个巨大数字。

而压缩的精髓在于，人类设计并利用Lean表达了一种语言，使得可以用大约600个token写下这个古戈尔量级的结构。

我们在论文中使用的方法从数学物理中汲取了灵感。在物理学中，当我们尝试为自然的某部分建立一个模型以进行分析时，会构建“玩具模型”。它并非试图捕捉全部真相，而是抓住核心结构，有意选择一个现实的粗略投影，以期能对其进行完整分析，从而指导对更复杂问题的直觉。电磁学、量子力学、BCS超导理论等都是如此。

在论文中，我们使用“幺半群”来对数学结构进行类似的建模分析。

幺半群与群类似，但未必包含逆元。自然数及其加法即构成一个简单的幺半群。在幺半群中，可以引入“宏”（macros），即代表新抽象概念的“新思想”，它们能帮助我们更高效地表达信息。

例如，“10 的幂次方”就是一个宏，它能压缩并高效地表示整数。一旦幺半群中引入了宏，就能推导出层级结构并衡量压缩程度。

研究表明，宏越多，压缩程度越高；宏越少，压缩能力越弱，表达能力也越有限。

在数学形式化系统（如 Lean 库）中，我们尚不清楚这些“宏”具体是什么。这就像在探寻数学的使用手册——我们对此了解得越多，人类与智能体在探索数学时就会越顺畅。关键在于学习数学中已有的机制：其原则是什么？推论是如何组织的？

当前的核心挑战是解决“逆问题”：找出数学侧对应的“宏”究竟是什么。

主持人：在数学推理中，机器往往需要遍历指数级的可能性，而人类却能以近似多项式级的速度直击要害。这种差异是否源于一种“数学品味”？我们是如何从海量可能性中筛选出有意义路径的？这种能力能否被建模并复制到机器中？

Michael Freedman：这是一个实验科学问题，也正是我们试图探索的。我们尝试在某种程度上循环分析数学史，以理解是什么引导我们走向这些高度可压缩的形式推理领域。或许通过澄清概念并举例说明哪些是可压缩的、哪些是不可压缩的，能更好地理解这一点。

主持人：能否给出更直观的例子？

Michael Freedman：以拉格朗日四平方和定理为例：任何整数均可表示为四个平方数之和。如果将“平方数”视为宏，那么使用这个增长极快的宏，每个整数只需四步即可表示。

这听起来或许令人惊讶，但解释在于：表达这些平方数本身需要很多比特，因此并不违背信息论。它只是表明，如果拥有更稠密的宏集合，就能用更少的步骤表达更多内容——即宏的“密度”决定了表达效率。而“10 的幂次方”正处于一个平衡点，在宏的简洁性（不过于庞大）与表达能力（能大幅扩展）之间取得了最佳折衷。

我们在论文中得出一个结论：多项式增长的幺半群易于压缩，而指数增长的幺半群难以压缩。

根据经验和数值研究，我们发现数学具有高度可压缩性。如果数学能被一个幺半群很好地表示，那么它必须是一个多项式增长的幺半群，才能呈现出我们所见到的这种压缩现象。

因此可以推测：数学的结构本质上是多项式的。

主持人：论文中还建议使用类似 PageRank 的算法来识别数学中具有高中心性的节点与核心定义，即那些支撑整个结构的关键部分。我们应如何在庞大的证明网络中识别并定位它们？如果能够识别，这是否定义了一种数学家与 AI 协作的新模式？

Michael Freedman：这是个很好的问题。PageRank 本质上是一种寻找马尔可夫链平稳分布的算法，即通过求解某个微分方程的吸引不动点来评估节点重要性。它基于节点间的相互引用关系来分配重要性，但这需要对整体结构和连接有全局了解。

在论文中，我们提出了更简单的指标。由于数学依赖抽象，我们定义了两种比例：“还原压缩”与“演绎压缩”。

• 还原压缩是“展开长度”与“压缩长度”之比。如果一个陈述处于极高的抽象层次，展开后变得非常庞大，那么这个比值就会很大。这不仅是自动智能体可用的局部指标，还能用于判断当前是在提升还是降低抽象层级。
• 演绎压缩是“证明长度”与“命题长度”之比。这个比例告诉我们有多少数学工作被压缩进了该命题中。例如，费马大定理可以用一句话陈述，但其证明长达数百页。极高的比例体现了该命题强大的“压缩密度”。

AI 在探索证明路径时可以追踪这些指标，从而感知其所穿越的数学“景观”。

主持人：整体来看，这篇论文在研究数学智能本质时提出了一个非常大胆的宣言，并且似乎与大型语言模型的发展相关。当初为何选择这个特定方向？希望传达的核心信息是什么？

Michael Freedman：我们论文的标题“压缩就是你所需要的全部”本身就是一个鲜明的观点。用大胆的措辞陈述观点是好事，它能引发讨论甚至反驳，从而推动更深入的探讨。

至于我个人为何选择这个研究方向？

从宏观历史视角看，我认为我们正处在一个非常特殊的节点。从文艺复兴到科学革命、工业革命，再到高科技革命和当前的人工智能浪潮，历史似乎正加速奔向某个“奇点”时刻，世界即将发生巨变。可以说，“外星人已经抵达了”，只不过它们是我们自己创造的。而我更希望以参与者而非旁观者的身份进入这个时代。

更具体地说，我们正在学习。寻找能够引导发现“有趣数学”（即人类所从事的数学）的简单组织原则，将是富有成效的。我们已经看到，可压缩性在数学中呈现出非常不同的形式。

论文中讨论的可压缩性是“局部”的：将一组符号压缩成新符号（如 10 的幂次方）。但像柯尔莫哥洛夫等人从算法角度研究的是一种更一般的“全局”压缩。

数学家运用的是局部压缩，而全局压缩是不可计算的。但或许存在某个中间地带，通过对压缩的深入研究，我们与智能体或许能探索出超越局部压缩的新思维模式。这仍是一个模糊的想法，但我希望将其呈现出来。

因此，我认为我们与 AI 在某种意义上是“同舟共济”的。它们也无法通过暴力计算探索全部空间，必须像我们一样依赖“直觉”。未来的关键在于：我们如何与 AI 共同发展新的数学直觉。

这篇论文，实质上是在尝试绘制一幅“数学地形图”，以帮助我们理解这个空间。

关注“鲸栖”小程序，掌握最新AI资讯