元数学新突破：颠覆传统理论计算机科学

清华姚班大神再度引领理论计算机科学界革命！

历经50年，顶尖科学家们一直试图攻克「旅行商问题」等计算机复杂性难题，但进展甚微。

为何这些难题始终难以证明？

答案其实就藏在「元数学」的奥秘里。

去年，一篇名为《Reverse Mathematics Below the Turing Jump》的论文悄然发布。

作者仅有三位：清华姚班的陈立杰、本科生李嘉图，以及知名计算机学者Igor Carboni Oliveira。

论文地址：https://eccc.weizmann.ac.il/report/2024/060/

他们摒弃了从公理推导定理的传统路径，转而采用「元数学」中的「逆向数学」方法。

令人惊喜的是，许多看似毫无关联的理论，在底层逻辑中竟是等价的。

例如，「鸽巢原理」与图灵机的「回文下界」。

这篇论文彻底颠覆了人们的认知。

过去半世纪，计算机科学家们追求的「更强公理证明更难定理」思路，原来从一开始就偏离了正轨。

逆向思维：数学的新篇章

千年思维范式的革新

面对那些「硬骨头」难题，计算机科学家们似乎总是卡壳。

以著名的「旅行商问题」为例，这只是一个组合优化问题：

在地图上找一条经过每个城市恰好一次，最后回到起点的最短路线。

然而，城市数量稍多，科学家就怀疑：没有好的解决办法。但问题是，没人能证明这一点。

过去50年，计算复杂性理论领域的大咖们，尝试将这种「直觉」转化为数学定理。

实际上，他们一次次碰壁，找不到任何突破口。

这也让他们开始思考一个更棘手的问题：为何证明总是失败？

「元数学」（Metamathematics）把证明本身作为研究对象。

当研究人员用「元数学」研究复杂性理论时，他们试图理解——

不同的公理集究竟能证明哪些关于计算难度的结论，以及为何自己在证明「问题很难」时总是差一口气。

这篇论文做了一件前人不敢想的事：三人团队彻底颠覆了数学几千年的思维范式。

传统做法是，给定一套公理，推导出定理。

现在，他们反过来——用一个定理替换掉其中一条公理，再证明那条被替换掉的公理。

这就是所谓的「逆向数学」（Reverse Mathematics）。

它证明了，许多看似无关的「复杂性定理」，在逻辑上是等价的。

IBM复杂性理论家Marco Carmosino看到论文后表示，「我震惊了，他们居然能做出这么多东西」。

从鸽子原理到离经叛道

故事要从2022年夏天说起。

当时，陈立杰正准备MIT博士毕业，发现时间充裕，便决定研究一下元数学。

他表示，「因为我要毕业了嘛，也没多少研究任务了，就寻思着该学点新东西」。

陈立杰开始研究复杂性理论的一个分支——通信复杂性（communication complexity）。

主要研究两个或多个人为了完成任务需要交换多少信息。

在通信复杂性中，有个最简单的问题叫「相等性问题」（equality problem），就像个合作游戏：

两个玩家各自拿着一串字符串，目标是用最少的交流弄清楚对方手里的字符串是否相同。

陈立杰关注的不是「下界」本身，而是研究人员是如何证明的。

所有已知的证明都依赖于一个简单的定理——鸽巢原理（Pigeonhole principle）。

“离奇”的相等

于是，陈立杰与刚合作的清华本科生李嘉图开始了新的探索。

为了让这种联系在数学上成立，他们选定了一套公理作为「地基」。

他们选了一套流行的公理集PV₁，开始「逆向」研究。

因为PV₁足够强大，能证明计算复杂性中的一些重要定理。若在PV₁基础上加一条特定版「鸽巢原理」，就能证明「相等性问题」的下界。

他们在去年成功验证了这一猜想：互换定理位置后，证明依然成立。

“离经叛道”的等价关系网