当 AI 开始反哺计算机科学：工具、伙伴与最终责任

2026 年 10 月，OpenAI 公布了一项关于指数时间假设（ETH）的研究结果。简单来说，ETH 长期被用来描述一类计算问题有多难：随着问题规模增加，求解所需时间可能急剧增长。OpenAI 的系统给出了一种新的算法，并配套发布了自然语言论文与 Lean 形式化证明。官方同时邀请外部专家组织公开核验，说明这仍是一项需要学界继续解释和检验的研究，而不是一句“AI 已经解决计算机科学”的口号。

这件事有趣的地方，不只是一条理论结论，而是它形成了一个闭环：人类发明计算机，依靠计算机训练 AI；如今，AI 又开始寻找新的算法、检验新的证明，反过来推动支撑自身运行的计算机科学。

正方：AI 正从计算工具变成研究伙伴

支持者会说，研究工作的瓶颈往往不是缺少聪明人，而是候选路径太多、验证成本太高。一个研究者可能花数月尝试几十条思路，AI 却可以并行探索更大的组合空间，再把候选结果交给形式化系统逐步检查。

ETH 的案例提供了一个具体想象：如果一条长期被广泛采用的复杂度假设可以被重新检验，那么许多建立在它之上的条件性结论也值得回头审视。即使新算法暂时不能直接让普通软件提速，它仍可能改变研究者寻找算法的方向。

类似的价值也可能出现在工程里。例如，面对一个运行缓慢的编译器模块，人类工程师通常从经验出发挑选少量优化方案；AI 可以生成大量等价改写，再用测试和证明工具排除错误候选。此时，AI 不只是更快地执行指令，而是在帮助人类发现原本没有想到的路径。

反方：会证明，不等于会选择正确的问题

反对者担心的并不是 AI “不够聪明”，而是我们可能把可验证误当成有价值。形式化证明能够严格说明“某个结论符合某套定义”，却不能自动保证这套定义完整地表达了现实问题。

设想一个 AI 为数据库找到更快的查询算法，并在基准测试中显著领先。如果测试只计算响应时间，却没有计入内存、维护成本和异常数据，那么这个“最优方案”上线后仍可能拖垮系统。证明和分数没有错，错的是问题边界被写窄了。

ETH 研究也有类似边界。Lean 可以检查形式化表达中的推理步骤，但自然语言论文、形式化定理与学界真正关心的命题是否完全对应，仍需要专家审查；理论上的渐近改进，也不等于现实规模下立刻更快。机器可以把答案做得极其严谨，人仍要追问：我们证明的是不是原本想证明的事？

人的角色不会消失，而会向上移动

因此，AI 反哺计算机科学，并不必然意味着人类退出。更可能发生的变化，是人的工作从“亲自尝试每一条路径”，上移到三个位置。

第一是提出问题。什么值得研究，哪些约束不能省略，仍来自人的目标和处境。第二是审查边界。AI 给出的证明、代码或实验，必须核对前提、数据和适用范围。第三是承担责任。当一个结论被用于医疗、金融或公共系统时，决定是否采用它的人不能把后果交给模型。

未来最有竞争力的研究者，未必是最擅长和 AI 比拼计算速度的人，而是能提出好问题、设计好验证，并在证据不足时敢于说“还不能下结论”的人。

结语

计算机孕育了 AI，AI 也确实开始改变计算机科学。但“推动”与“主导”之间仍有一条重要界线：AI 可以扩大探索空间、加速证明和提出候选，人类仍要决定方向、解释意义并承担后果。

真正值得期待的未来，不是机器替我们决定一切，而是它让更多过去来不及探索的问题变得可探索，同时迫使我们更认真地学习如何提问。

参考资料

• OpenAI：《Working with academic communities to build scientific understanding》，2026-10-26：https://openai.com/index/building-scientific-understanding-with-academic-communities/
• OpenAI：《The Exponential Time Hypothesis is False》，2026-10-25：https://github.com/openai/math/tree/main/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026
• Fabio Dias、Yvens Lima：《Limits and Constants of OpenAI's Claimed ETH Refutation》，2026-10-31：https://arxiv.org/abs/2611.00517