1956年，荷兰计算机科学家迪杰斯特拉在阿姆斯特丹一家咖啡馆里，花了大约二十分钟，想出了一个找最短路径的方法。三年后这个算法正式发表，此后六十七年，它稳稳地待在全世界计算机专业的教科书里。你手机里的地图导航、快递的物流规划、网络的数据路由，底层都有它的影子。

几天前，这块基石被撬动了一下。动手的不是哪位数学家，是十个AI。

十个AI，一块留言板，吵了733次

事情是美国AI评测公司Vals AI做的实验。他们让十个Claude Opus 5.5智能体（Anthropic刚发布的旗舰模型）进入同一个沙盒环境，任务是：设计一个在某些场景下比Dijkstra更快的最短路径算法，并且必须用Lean这门形式化验证语言写出完整数学证明。

Lean是什么概念？它是"数学证明的编译器"，每一步推理都要经过机器内核逐行核验，含糊一点都过不去。也就是说，AI不能靠"听起来有道理"蒙混过关。

这十个智能体被放进一块共享的虚拟留言板里。有的负责提构想，有的专门挑漏洞，有的负责把思路翻译成机器能检验的语言。它们互相质疑、推翻对方的方案，把失败的思路记录下来防止别人重复踩坑。十五个小时里，留言板累积了733条讨论记录。

最后交出的成果，是一个叫C-HD的新算法，外加289个Lean证明文件。按照证明结论，在一类特定密度的有向图上，C-HD的理论复杂度确实优于Dijkstra。数学层面，这是严格成立的。

十个AI用15小时走完了人类课题组可能要几年的路——提出猜想、互相辩论、构建证明、机器校验，一整套科研闭环。

然后反转来了

消息传开，算法圈沸腾了一天。很快，一位开发者连夜用C语言把C-HD完整实现出来，写了大约1900行代码，和经典Dijkstra放在同一环境里跑分。

结果相当尴尬：C-HD在真实机器上，比最朴素的Dijkstra版本还要慢1.4到2.8倍。

问题出在哪？不是证明错了——数学上它确实更优。问题出在"大O记号"这个东西本身。大O只关心数据规模趋于无穷大时的增长趋势，会直接忽略常数开销。C-HD省下了理论上的计算步骤，代价是巨量的预处理和频繁的标签处理。实测数据里，59%的运行时间花在16字节标签处理上，34%耗在预处理环节。只有当图的规模膨胀到现有硬件根本装不下的程度，理论优势才能兑现——而在真实世界里，这一天永远不会来。

换句话说：AI证明了一个算法是对的，但它不知道这个算法有没有用。

这件事真正值得琢磨的地方

先把话说清楚：这项成果还没经过外部专家同行评议，"AI推翻教科书"这种说法本身也夸张了——Dijkstra在自己的适用范围里依然是最优解，C-HD只是在这个基础理论的地图上，插了一面"此处曾有人到过"的旗子。

但有两件事是实打实的。

第一，AI第一次完整跑通了"提出新算法+机器可验证证明"的流程。过去这类硬核理论工作，只有顶尖数学家能做。莱特兄弟第一次试飞也飞不高，但重点是"机器能飞"这件事被证明了。

第二，也是跟普通职场人关系最大的：AI能产出"正确但无用"的成果，而且它自己意识不到。它擅长在给定规则里推导、组合、证明，却判断不了这项成果在现实中值几个钱。判断一件事值不值得做，目前还是人类的独活。

对上班的人，这意味着什么

说一个可能反直觉的数据。斯坦福数字经济实验室今年8月更新的研究显示：在AI暴露度最高的职业里，美国22到25岁劳动者的就业水平，比低暴露岗位的趋势线低了约19%——而且这个缺口主要来自"招聘减少"，不是集中裁员。翻译一下：企业不是把年轻人开除，是干脆不招了，因为那些用来练手的活儿——整理资料、写初稿、做基础分析——AI干得又快又便宜。

但同一个实验也给出了另一面的答案。AI产出的东西，需要有人判断好坏、决定取舍、对结果负责。实验室里那十个AI吵了十五个小时吵出个"对但没用"的算法，最终拍板说"这在工程上没有价值"的，是人。

所以真正拉开差距的，不是会不会用AI——会用AI很快会变成像会打字一样的标配——而是你有没有那份判断力：知道AI给你的东西哪些能用，哪些是"理论正确、现实跑不动"的花架子。机器负责把事做对，人负责判断什么值得做。

Dijkstra本人晚年回忆说，那个算法不过是咖啡馆里二十分钟的灵光一现。六十七年后，十个AI用十五个小时在它旁边画了个新记号，人类看了一眼说：数学很漂亮，先放抽屉里吧。

这个"看一眼"的动作，就是未来几十年里最值钱的技能。

职场AI生存系列