新智元报道
编辑：桃子 好困
【新智元导读】50年未解计算复杂性「天坑」，竟被姚班大神搞定了！他选了一条「逆向数学」的新路，正把理论计算机科学倒过来重写。
清华姚班大神，再度引爆理论计算机科学圈！
50年来，顶尖科学家都在死磕「旅行商问题」等这类计算机复杂性难题，却迟迟没有进展。
为什么一直证明不出来？
实际上，答案藏在了「元数学」的领域。
恰在去年，一篇名为《Reverse Mathematics Below the Turing Jump》论文低调上线。
作者仅有三个人，清华姚班陈立杰、本科生李嘉图，以及著名计算机领域学者Igor Carboni Oliveira。
论文地址：https://eccc.weizmann.ac.il/report/2024/060/
他们不再死磕从公理推导定理的传统路径，而是另辟蹊径，采用了「元数学」中「逆向数学」的方法。
结果惊喜地发现，许多看似风马牛不相及的理论，竟在底层逻辑中是完全等价的。
比如，「鸽巢原理」与图灵机的「回文下界」。
这篇论文一出，彻底颠覆了人们的「世界观」。
过去半个世纪，计算机科学家们苦苦追求「更强公理证明更难定理」的思路，原来从一开始就走偏了。
把数学「倒过来」
颠覆千年思维范式
一提到那些「硬骨头」难题，计算机科学家们似乎就卡壳了。
就以著名的「旅行商问题」为例，表面上看，这只是一个组合优化问题：
在地图上找一条经过每个城市恰好一次，最后还能回到起点的最短路线。
可是一旦城市数量稍多，科学家也就怀疑：根本没有很好的办法。但问题是，没人知道怎么证明这一点。
过去50年来，计算复杂性理论领域的大佬，都尝试把这种「直觉」，转化成板上钉钉的数学定理。
实际上，他们一次次铩羽而归，根本找不到任何突破口。
这也让他们越来越多地开始琢磨一个相关但更让人摸不着头脑的问题：为啥证明老是不成功呢？
「元数学」（Metamathematics），却把证明本身当成了研究对象。
当研究人员用「元数学」研究复杂性理论时，他们试图搞清楚——
用不同的公理集，到底能证明/不能证明关于计算难度的哪些结论。
为啥自己在证明「问题很难」这条路上，总是差了一口气。
2024年4月这篇论文，做了一件前人都不敢想的事：三人团队彻底颠倒了数学几千年来的思维范式。
传统的套路是，给到一套公理，推出一串定理。
而现在，他们反过来——用一个定理替换掉其中一条公理，然后去证明那条被替换掉的公理。
正如论文题目所示，这一过程称之为「逆向数学」（Reverse Mathematics）。
它证明了，一大堆看起来完全不相关的「复杂性定理」，其实逻辑完全等价。
IBM复杂性理论家Marco Carmosino看到论文后的第一反应，「我震惊了，他们居然能做出这么多东西」。
谁看了肯定都会说，就是它把我拽进了「元数学」这个坑的！
鸽子证明，离经叛道
故事还得从2022年夏天说起。
当时，陈立杰正准备MIT博士毕业，发现手头突然多出了一大把空闲时间，便决定花几个月钻研一下元数学。
他表示，「因为我要毕业了嘛，也没多少研究任务了，就寻思着该学点新东西」。
读着读着，陈立杰开始琢磨起复杂性理论的一个分支——通信复杂性（communication complexity）。
主要研究两个或多个人为了完成某项任务，必须交换多少信息。
在通信复杂性里，有个最简单的问题叫「相等性问题」（equality problem），就像个合作游戏：
两个玩家各自拿着一串0和1组成的字符串，目标是用最少的交流，弄清楚对方手里的字符串是不是一模一样的。
最笨的办法就是，一个玩家把自己的字符串整个儿发给对方检查。
除此之外，复杂性理论家几十年前就证明了：没招，不行。
要解决「相等性问题」，至少得发送跟字符串长度一样多的比特数。理论家把这个字符串的长度称为所需通信量的「下界」（lower bound）。
陈立杰关注的不是这个「下界」本身，而是研究人员当初是怎么证明它的。
而所有已知的证明都离不开一个简单的定理——鸽巢原理（pigeonhole principle，也叫「抽屉原理」）。
这原理说的是：如果你把一堆鸽子塞进比鸽子数量少的洞里，那至少有一个洞里得挤着不止一只鸟。
这听起来好像是废话，但在复杂性理论以及更多领域里，这可是个威力巨大的工具。
于是，陈立杰敏锐地捕捉到一个重要的线索——
「相等性问题」和「鸽巢原理」之间的联系，没准是双向的。
用鸽巢原理来证明相等性问题的下界很容易。那能不能反过来，用下界来证明鸽巢原理呢？
离奇的相等
于是，陈立杰拉上了刚合作完一篇论文清华本科生李嘉图（Jiatu Li），开始了新的探索。
为了让这种联系在数学上站得住脚，他们得选定一套公理作为「地基」。
他们选了一套很流行的公理集，叫PV₁，开始「逆向」。
因为PV₁本身足够强，能独立证明计算复杂性里的一些重要定理，若在PV₁基础上，再加一条特定版「鸽巢原理」作为额外公理，就能证明「相等性问题」的下界。
2022年12月，他们成功了！
结果恰恰验证了陈立杰最初的猜想：把定理的位置互换一下，证明也依然成立。
在PV₁逻辑框架中，两个定理是完全等价的。
当他们跟华威大学的复杂性理论家Igor Oliveira聊起结果时，突然意识到——
「逆向数学」大法，可能也适用于复杂性理论中其他八竿子打不着的领域。
在接下来几个月里，他们系统地证明了许多其他定理也是等价的。
陈立杰说，「刚开始，我们要证的等价东西只有俩，但现在我们手里已经织出了一张大网」。
这个团队发现的最惊人的联系，是把同一个版本的「鸽巢原理」，跟学生们在复杂性理论入门课上学到的最早那批定理之一联系了起来。
这一经典定理，设定了一种理论计算机，即单带图灵机（single-tape Turing machine），在判断一串0和1是不是回文（正着读反着读都一样）时，所需时间的下界。
「逆向数学」证明了：在PV₁框架内，这个「回文下界」定理跟鸽巢原理竟然是等价的。
就连陈立杰难以置信地表示，「如果你直接告诉我这个结论，我肯定不信。听起来太扯了」。
这一结论之所以让人大跌眼镜，是因为两个定理表面上差得太远了。
「鸽巢原理」本质上跟计算没任何关系，是个关于数数的简单道理。
而回文下界呢，是关于特定计算模型的一条陈述。
这个新结果意味着，这些看似路子很窄的定理，其实比它们看起来要通用得多，基础得多。
Oliveira表示，「这说明我们想要理解的这些复杂性下界，其实更加触及根本」。
未知领域，还需打好地基
令人欣喜的是，这张新的「等价关系网」也帮科学家们看清了PV₁的局限性。
大家早就相信，光靠PV₁的公理是证明不了「鸽巢原理」的。
所以，论文的结果就意味着，网里的其他等价定理，在PV₁里多半也是证明不了的。
牛津大学的复杂性理论家Ján Pich感叹道，「我觉得这太美了」。
但他同时提醒道，「逆向数学」这种方法，可能最适合用来揭示那些已经被证明出来的定理之间的新联系。
「对于那些我们还不知道怎么证明的陈述，就目前来看，它能告诉我们的关于其复杂性的信息并不多」。
要搞懂这片未知领域，对「元数学」研究人员来说还是个遥远的目标。
但这丝毫没有浇灭李嘉图对这个学科的热情。
2023年进入MIT攻读研究生，他最近还专门为复杂性理论家写了一份长达140页的元数学指南。
论文地址：https://eccc.weizmann.ac.il/report/2025/086/
这也是一个大趋势的缩影：即便坐了几十年的冷板凳后，「元数学」正日益吸引着更广泛的研究人员群体的目光，他们正给这个领域带来全新的视角。
Carmosino表示，「大家已经厌倦了被卡在原地不动，是时候退一步，好好把地基搞搞清楚了」。
作者介绍
陈立杰
陈立杰是加州大学伯克利分校电气工程与计算机科学系（EECS）的助理教授，也是伯克利理论组的一员。
早在高中时期，陈立杰就已在信息学竞赛圈封神，展现出了超越同龄人的编程天赋与数学洞察力。
2012年NOI大赛中，陈立杰以金牌成绩脱颖而出，提前锁定了清华大学的保送资格。
紧接着，在第25届IOI上，他又以569分（满分600分）的惊人成绩夺得全球第一。
一直以来，他还在Codeforces、TopCoder等国际编程平台上长期霸榜，因其解题速度极快、思路极其实用，被国内外选手膜拜。
保送到清华大学后，陈立杰在交叉信息研究院「姚班」获得学士学位，师从李建教授。
2016年，他曾获得了清华本科生特等奖学金，答辩视频一度火爆全网。
随后，他在MIT获得了博士学位，师从Ryan Williams。
当时，他的主攻方向是「计算复杂性理论」和「细粒度复杂性」。
2019年，他包揽了理论计算机科学领域两大顶级会议（STOC和FOCS）的最佳学生论文奖。
2022年博士毕业后，他获得了极具声望的加州大学伯克利分校米勒奖学金（Miller Fellowship），成为该校的博士后研究员，合作导师是Avishay Tal和Umesh V. Vazirani。
他对理论计算机科学有着广泛的兴趣，特别是复杂度理论中的基础性问题。同时，也致力于将理论计算机科学的思想应用到其他科学领域，例如量子物理和AI安全。
-
如何在P vs. NP问题上取得进展？
-
随机性对于高效计算而言是不可或缺的吗？（即BPP是否等于P？）
-
量子复杂度理论如何帮助我们理解量子物理？
-
如何应用理论计算机科学的思想，为AI系统建立安全理论保障？
科研，只是陈立杰众多兴趣之一。在清华一次采访中，他曾提到如果未来不做研究，就做音乐游戏玩家。
成为一名真正的理论计算机科学家，这个想法从中学时期在他的内心就已生根发芽。
如今，回看他的研究和职业生涯，正是朝着这个方向一直在发光发亮。
李嘉图
李嘉图是MIT理论组的二年级博士生，师从Ryan Williams。
此前，他在清华大学交叉信息院「姚班」获得学士学位。期间，他曾与华威大学的Igor C. Oliveira以及清华大学的陈一镭教授有过合作。
他的研究集中在证明计算的固有难度（即电路复杂度）、证明系统（即证明复杂度），以及探究为什么这个研究方向如此困难（即元复杂度）。
最近，他对以下方向也很感兴趣：有界算术（Bounded Arithmetic）的强度，值域规避问题（Range Avoidance Problem）的复杂度，证明无条件复杂度下界，以及使用Coq和Lean编写形式化数学证明。
在他看来，复杂度理论研究者的使命，就是「解救」那些试图攻克固有难题的勇士们。有时候，这些难题的故事也能治好密码学家的失眠（譬如这篇：Cryptographers Seldom Sleep Well）。
Igor Carboni Oliveira
Igor C. Oliveira是华威大学理论与基础学部（FoCS）以及离散数学及其应用中心（DIMAP）的成员。
此前，他在哥伦比亚大学计算理论组获得了博士学位，并曾是牛津大学算法与复杂度理论组的博士后研究员，加州大学伯克利分校Simons研究所的研究员，以及布拉格查理大学数学学院的博士后。
他研究集中在计算复杂度理论，以及该领域与算法、组合数学和数理逻辑之间的联系。研究兴趣是高效计算的可能性与局限性，以及我们能对此证明些什么。
参考资料：
https://www.quantamagazine.org/reverse-mathematics-illuminates-why-hard-problems-are-hard-20251201/
秒追ASI
⭐点赞、转发、在看一键三连⭐
点亮星标，锁定新智元极速推送！
