网易首页 > 网易号 > 正文 申请入驻

菲尔兹奖得主Michael Freedman新作揭开数学真相

0
分享至

机器之心编辑部


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

Michael Freedman 是当代最具影响力的数学家之一,曾因解决四维庞加莱猜想获得菲尔兹奖。这一成果被认为是拓扑学领域的里程碑。

此后,他并未停留在纯数学领域,而是转向应用前沿,创立了 Microsoft StationQ,成为拓扑量子计算的重要推动者之一。

近年来,Michael Freedman又将研究兴趣延伸至人工智能,尝试用数学视角理解人类知识的结构与生成机制。



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

这种数学家们在几十层抽象之上轻松将庞大的演绎链条凝练为简洁的概念背后,揭示了一个被数学家们使用了 3000 年、却很少被言明的秘密:数学的本质,不是证明,而是压缩。

近日,Michael Freedman 在最新论文中直接喊出这一宣言:「压缩,就是你所需要的全部」(Compression is all you need)。



  • 论文链接:https://arxiv.org/pdf/2603.20396

在最近的一次采访中,Michael Freedman 对此论文进行了介绍,探讨了人类数学直觉与机器逻辑之间的巨大鸿沟。

他认为,人类数学数千年的演进,本质上是一部不断创造「宏」、构建抽象层级的压缩史。从 3000 年前的位值表示法,到现代复杂的微分方程,人类文明实际上一直在进行「数据压缩」实验。

人类做数学,从来不是在穷举推理路径,而是在一个几乎无限的空间中,不断寻找可以被压缩的结构。相较之下,AI 却是一直在「穷举」……

因此,在 AI 正处于关键发展阶段的当下,理解这一机制,或许正是人类与 AI 在数学领域实现真正协作的起点。

下面是此次 Michael Freedman 的采访内容,为了更好地阅读,我们在不改变原意的基础上进行了调整。

主持人:当我们谈到数学时,通常会认为它是一个严密、完美的逻辑体系,但你的研究似乎在说,人类真正使用的数学并不是这样。你能否从「压缩」这个概念开始讲起?

Michael Freedman:当然可以。在我们的论文中有个小玩笑:压缩其实早在 3000 年前就被发明了,也许就是数学的第一个伟大定理 —— 位值记数法(Place notation)。

比如「10」可以用一个「1」放在特定位置表示,「100」也是类似。就是通过把「1」放在不同的位置,从而用极少的符号表示极大的数。这种表示方式让整数的表达具备对数级增长,却能在有限符号中表达指数级数量的数。

这就是一种极其强大的压缩方式,它甚至和现代物理中的一些思想(比如自旋链状态)有关。但压缩远不止是数字表示,它贯穿整个数学体系。

主持人:能举一个更具体的例子吗?

Michael Freedman:我刚上大学时,第一次上微分方程课,教授在黑板上写下一个一个巨大的 Ω,并说它是「向量丛截面的芽层」(sheaf of germs of sections of a vector bundle)。

那一刻,我甚至不知道什么是向量丛?后来我才意识到要理解这句话,你需要理解背后的多层概念:向量丛、截面、层、芽,以及它们之间的映射关系。如果再往下深思,还涉及自然数、整数、有理数、实数、向量空间、流形等基础结构。

也就是说,数学家在思考时,其实是站在十几层抽象之上。这就是为什么微分方程「看起来不难」,因为大量信息已经被压缩了。

这就是「压缩」的力量:大量信息被隐藏在高层概念中。

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

在论文中,我们试图把这种直觉变成可量化的东西。我们使用 Lean 的数学库(mathlib,约 50 万行代码)作为「人类数学」的一个近似模型,对其结构进行了统计分析:一个定理如何调用其他引理、定义如何复合并相互嵌套。我们可以看到一种分层结构和压缩结构,它使得 Mathlib 中的命题以高层级( Wrapped,包装态)编写,但随后可以展开为基础的 Lean 术语(Unwrapped,解包态)。

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

主持人:我记得这可以达到一个非常荒谬的数字:10 的 104 次方,对吧?那我想问,你做这些事因为你想强调这本质上是数学的核心,对吗?

Michael Freedman:是的,我们将这个库中的内容视为人类行为的一个良好样本,虽然它在数学各领域的分布并不完美 —— 数论和代数几何比分析或拓扑多得多。它不是人类数学思想的完美副本,但它与「从一组公理出发进行每一种可能的逻辑推演」截然不同,后者会导致「混沌数学」。

而无论如何进行形式化,发现结构都会呈双指数级增长。最终的结果就像你说的,我们在 Lean 库中找到的最长的解包命题(Unwrapped statement),其大小为 10 的 104 次方),比 Googol(10 的 100 次方)还要大。而它对应的包装命题(Wrapped statement)只有 600 个 Token。

这展示了惊人的膨胀,但反过来也展示了通过使用概念所获得的巨大压缩。

我想说的是,数学家和他们的智能体实际上在同一条船上。但当你看到像 Googol 这样的数字,即使我们的机器比我们快 100 万倍,100 万在 Googol 的尺度下也是微不足道的。

所以,真正的问题不是人类与机器将探索什么,而是在庞大的形式推理空间中,哪一部分是可以被压缩成我们和智能体能够理解的形式(我称之为形式数学)。

我相信人类数学(在此将我们的智能体也视为「人类」的一部分)正是如此。

主持人:在你们分析的这些方程中,是否发现存在某些方程或过程,不具备与其他事物相同的「公分母」?如果是这样,如何决定什么是「最基础」的?或如何知道自己「触底」?

Michael Freedman:对于 Lean 来说,很容易知道什么时候触底,因为库的结构就是这样设计的。

基本上,有原始项,你可以用它们构建更复杂的命题,所以这个「展开后长度」有时被称为树表示法。每个命题,你看它的子节点,即它是由什么构建的,然后你看那些子节点的子节点,形成一棵越来越深的树,直到它终止于原始的 Lean 项。之后统计所有这些节点的调用,每个节点根据其调用的先前节点的权重被赋予权重,从原始项权重为 1 开始。当把树上顶层的权重加起来时,就得到了展开后命题的巨大数字。

而压缩在于,人类设计并利用 Lean 表达了一种语言,可以用大约 600 个 token 写下这个 Googol 量级的数字。

我们在论文中使用的方法则是从数学物理中汲取了灵感。在物理学中尝试为自然的某部分建立一个模型以帮助进行数学分析时,这就是「玩具模型」(toy model),并非试图捕捉全部真相,而是抓住核心结构,有意选择一个现实的粗略投影,希望能够对其做出完整的分析,从而指导对更复杂问题的直觉。比如电磁学、量子力学、BCS 超导理论等,都是这样。

在论文中,我们使用「幺半群」(monoid)来建模数学。

幺半群类似于群,只是未必有逆元,最简单的幺半群就是计数数字,即自然数。在幺半群一侧,可以放入「宏」(macros),即「新思想」,代表新的抽象,可以帮助我们更高效地表达信息。

比如「10 的幂次方」,就是一个能实现压缩、高效表示整数的宏的例子。一旦在幺半群中有宏,就可以推导出层级属性、衡量压缩程度。

研究结果显示,宏越多,实现的压缩程度就越高;宏越少,压缩就越少,表达能力越弱。

而在数学这一侧,在 Lean 库中,我们不知道宏是什么,这有点像在问数学的使用手册,我们对此获得的洞察越多,「人类」(我们和智能体)在探索数学时就会越顺利,想法是去学习已经在数学中使用的机制:原则是什么?推论是如何组织的?

现在的主要挑战是解决「逆问题」,即看看在数学侧对应的「宏」到底是什么。

主持人:在数学推理中,机器往往需要遍历指数级的可能性,而人类却能以更慢、近似多项式的(速率)方式直接切中要点。这种差异是否源于一种「数学品味」?我们是如何从海量可能性中筛选出真正有意义的路径的,以及这种能力是否可以被建模和复制到机器中?

Michael Freedman:这是实验科学,正是我们试图发现的。我们试图在某种程度上循环分析数学的历史,试图理解是什么引导我们走向这些高度可压缩的形式推理领域,也许澄清这个概念,举一些宏的例子会更好,就能看到什么是可压缩、什么是不可压缩的。

主持人:有没有更为直观的例子?

Michael Freedman:比如有一个定理:任何整数都可以表示为四个平方数之和(拉格朗日定理)。

这意味着,如果你将「平方数」当作宏,那使用这种增长极快的宏,每个整数只需要四步就可以表示。

听起来很疯狂,但解释是表达这些平方数本身需要很多比特,所以这并不违背信息论。它只是,说明如果有更稠密的宏集,就可以用更少的步骤表达更多内容,即宏的「密度」决定表达效率,而「10 的幂次方」正好处于平衡点,在宏的简洁性(不要太大)和表达能力(能够大量扩展)之间找到了一个最佳平衡点。

我们在论文中有一个结论是:多项式增长的幺半群容易压缩,而指数增长的幺半群难以压缩。

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

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

主持人:论文中还提到,建议使用类似 PageRank 算法来识别数学中高中心性的节点和核心定义,即那些支撑整个结构发挥最大作用的节点。那我们如何在这些庞大的证明网络中识别、找到它们?如果能识别出,是否定义了一种数学家与 AI 协作的新模式?

Michael Freedman:这是个好问题。PageRank 基本上是一种寻找马尔可夫链平衡的算法。

换句话说,它是寻找某个微分方程的吸引不动点,你有许多互相交流的节点,想通过观察谁调用了谁来确定谁最重要。这是一种分配重要性的自然想法,但它需要对结构和互连有全局性的了解 。

但论文中我们提出了更简单的指标,因为数学依赖抽象,有一些比例我们分别称为「还原压缩」(Reductive compression)和「演绎压缩」(Deductive compression)。

「还原压缩」是「展开长度」与「压缩长度」的比值,如果一个陈述处于极高的抽象水平,展开后会变得巨大,那么这个比值就会非常大。这不仅是自动智能体可以使用的局部指标,还可以用来判断是在提升还是降低抽象层级。

「演绎压缩」则是观察证明长度与命题长度的比值,这个比例告诉我们有多少数学工作被压缩进了那个命题中。比如费马大定理,可以用一句话描述,但证明需要数百页。这个比例证明了现象级的力量:该命题具有极高的「压缩密度」。

AI 可以在探索证明路径时追踪这些指标,以此感知它正在穿越的「景观」。

主持人:其实从整体来看,这篇论文在研究数学智能的本质时提出了一个非常大胆的宣言,且似乎与 LLM 发展有关,当初为什么选择这个特定方向?想传达的核心是什么?

Michael Freedman:我们论文标题「Compression is all you need」(「压缩,就是你所需要的全部」)本身就是一个强观点。大胆的措辞陈述观点是好事,这样人们可以反驳它,从而引发更好的讨论。

而至于我个人为什么选择这个研究方向?

从宏观上来看,我认为我们正处于一个非常特殊的历史节点。从文艺复兴到科学革命、工业革命,再到高科技革命和现在的 AI,历史似乎真的在奔向「奇点」时刻,世界即将发生巨变。你可以说「外星人已经抵达了」,只是它们是我们制造出来的。而我,更想作为参与者而非观察者进入这个时代。

更具体来说,我们正在学习,寻找能够引导发现「有趣数学」(即人类数学)的简单组织原则将是富有成效的。我们已经看到,这种可压缩性在数学中有着非常不同的形式。

论文中提到的可压缩性是「局部」的:你将一组符号压缩成新符号(如 10 的幂次方)。但像柯尔莫哥洛夫(Kolmogorov)这样的人通过算法研究了更一般类型的可压缩性,即「全局」压缩。

所以,数学家使用局部压缩,而全局压缩是不可计算的。但可能存在某种中间地带,通过仔细研究压缩,我们和智能体也许能探索超越局部压缩的新思维模式。这是一个模糊的想法,但我想呈现给大家。

所以,我认为我们和 AI 在某种意义上是「同一条船上的人」。它们也无法通过暴力计算探索全部空间,必须像我们一样依赖「直觉」。而未来的关键是:我们如何与 AI 一起,发展新的数学直觉。

这篇论文,其实是在尝试画出一张「数学的地形图」,帮助我们理解这个空间。

https://arxiv.org/abs/2603.20396

https://x.com/SAIRfoundation/status/2036916216913330552

特别声明:以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布,本平台仅提供信息存储服务。

Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.

相关推荐
热点推荐
戴着妈妈的项链去面试,被董事长看到,董事长震惊问:你妈妈是谁

戴着妈妈的项链去面试,被董事长看到,董事长震惊问:你妈妈是谁

千秋文化
2026-04-18 19:08:36
世锦赛:丁俊晖横扫吉尔伯特终结两连败,中国一哥创造历史进16强

世锦赛:丁俊晖横扫吉尔伯特终结两连败,中国一哥创造历史进16强

世界体坛观察家
2026-04-20 19:42:44
中国历史第5人!杨瀚森季后赛首秀52秒0分 工作室:在场即是成长

中国历史第5人!杨瀚森季后赛首秀52秒0分 工作室:在场即是成长

醉卧浮生
2026-04-20 11:45:27
60岁武大中南医院王行环被抓!女医生曝其恶心勾当,简直太愤怒

60岁武大中南医院王行环被抓!女医生曝其恶心勾当,简直太愤怒

奇思妙想草叶君
2026-04-20 15:07:28
这个国家快被中国“买”下!美女遍地,10个移民中就有9个中国人

这个国家快被中国“买”下!美女遍地,10个移民中就有9个中国人

凡知
2026-04-20 15:39:02
记者:皇马没有联系穆里尼奥,也不会寻找少帅

记者:皇马没有联系穆里尼奥,也不会寻找少帅

懂球帝
2026-04-20 16:10:39
邓亚萍和温瑞博的深层关系,温瑞博会以双重身份参与伦敦世乒赛

邓亚萍和温瑞博的深层关系,温瑞博会以双重身份参与伦敦世乒赛

小皷拍客在北漂
2026-04-20 08:01:11
什么原因?仅仅一百五十年,江阴靖江长江江面居然缩窄了80%

什么原因?仅仅一百五十年,江阴靖江长江江面居然缩窄了80%

抽象派大师
2026-04-20 01:27:38
上海市委书记同快递小哥、外卖骑手深入交流,表达了什么?

上海市委书记同快递小哥、外卖骑手深入交流,表达了什么?

上观新闻
2026-04-20 16:06:17
城市更新大潮来了!中央定调:20年房龄老房子,2026年起或又吃香

城市更新大潮来了!中央定调:20年房龄老房子,2026年起或又吃香

混沌录
2026-04-20 16:38:07
国乒三喜临门!莎莎断层领跑、小胖满血归来、14岁天才绝境封王!

国乒三喜临门!莎莎断层领跑、小胖满血归来、14岁天才绝境封王!

衔春信
2026-04-20 19:09:02
宿茂臻:于指导把天津队带得不错;王大雷比目鱼肌有些拉伤

宿茂臻:于指导把天津队带得不错;王大雷比目鱼肌有些拉伤

懂球帝
2026-04-20 18:27:08
补授的四位开国将军

补授的四位开国将军

祁州校尉
2026-04-16 11:00:14
小S首谈大S赴日旅行原因,至今自责靠酒精麻痹,酒后在家大哭大闹

小S首谈大S赴日旅行原因,至今自责靠酒精麻痹,酒后在家大哭大闹

开开森森
2026-04-20 20:03:09
人民日报:已投放500万辆!新国标电动车为何突然反转,有3大原因

人民日报:已投放500万辆!新国标电动车为何突然反转,有3大原因

电动车的那些事儿
2026-04-18 07:37:58
武大杨景媛被投诉辞职后续:已考公进复试!笔试成绩还挺高

武大杨景媛被投诉辞职后续:已考公进复试!笔试成绩还挺高

林大师热点
2026-04-20 20:18:56
浙江一男子收到陌生账号转账8万余元,三天后奢侈品牌CELINE商家找来:员工误将其收款码给客户

浙江一男子收到陌生账号转账8万余元,三天后奢侈品牌CELINE商家找来:员工误将其收款码给客户

台州交通广播
2026-04-20 14:13:51
《八千里路云和月》大结局:田家泰被暗杀!七哥真实身份曝光意外

《八千里路云和月》大结局:田家泰被暗杀!七哥真实身份曝光意外

肆季娱乐
2026-04-20 20:29:42
土耳其美女来中国旅游,回国后大哭,坦言土耳其与中国差距太大了

土耳其美女来中国旅游,回国后大哭,坦言土耳其与中国差距太大了

千秋历史
2026-04-08 20:11:37
疯狂!种马男星沃伦睡过12775名女友,性欲成瘾缠着女友不让下床

疯狂!种马男星沃伦睡过12775名女友,性欲成瘾缠着女友不让下床

钱小刀娱乐
2026-04-14 10:39:13
2026-04-20 21:20:51
机器之心Pro incentive-icons
机器之心Pro
专业的人工智能媒体
12813文章数 142633关注度
往期回顾 全部

科技要闻

华为Pura90逆周期定价,4699元起,未涨价

头条要闻

19岁女孩挪用自家1700万当"榜一大姐" 亲爹带女儿自首

头条要闻

19岁女孩挪用自家1700万当"榜一大姐" 亲爹带女儿自首

体育要闻

阿森纳已拼尽全力,但你早干嘛去了...

娱乐要闻

鹿晗生日上热搜,被关晓彤撕下体面

财经要闻

利润暴跌7成,字节到底在做什么

汽车要闻

把天门山搬进厂?开仰望U8冲上45度坡的那刻 我腿软了

态度原创

亲子
教育
家居
本地
数码

亲子要闻

上海首家儿童运动医学中心成立,推行微创优先、医护康一体化服务

教育要闻

定了!西城两所超级牛校大幅扩招!“五金刚”终于凑齐!

家居要闻

自然慢调 慢享时光

本地新闻

12吨巧克力有难,全网化身超级侦探添乱

数码要闻

存在致死风险!1.8万台PC电源召回:呼吁用户立即停用

无障碍浏览 进入关怀版