高德纳的难题被AI攻破，但谁来检查AI写的代码？

01高德纳的未解难题被Claude攻破，数学家与AI的新关系正在被改写

「Shock! Shock!」87岁的计算机科学家高德纳在斯坦福发出的这封短信，让整个数学社区为之一震。他花了数周研究的一个开放问题，刚被Anthropic的混合推理模型Claude Opus 4.6解决了。

这个问题来自高德纳正在撰写的《计算机程序设计艺术》新卷，涉及有向哈密顿圈的分解：给定一个由三维模运算构成的有向图，能否将所有弧分解为三个哈密顿圈？高德纳本人解决了m=3的情况，却卡在了一般化推广上。他的朋友Stappers接过挑战，用实验方法验证到m=16，但始终找不到通用构造。

Stappers决定把问题原封不动地交给Claude。接下来的过程值得细看：Claude先将问题重新表述为置换选择问题，然后尝试了暴力搜索、模拟退火、纤维分解等至少31轮探索。每一轮都按指令把进展写入计划文档，失败了就换方向。第15轮，它发现了一种「纤维分解」视角，把三维结构按坐标和的模投影到层状图上。第27轮接近成功，用循环坐标旋转构造出三个哈密顿圈，但仍有少量顶点冲突。第30轮，它回头审视之前模拟退火碰巧找到的一个解，从中注意到每层的选择只依赖单个坐标，由此在第31轮写出了一个Python程序，对所有奇数m都给出了完美分解。

Stappers验证了m=3到m=101的全部奇数情况，每一个都成功。但Claude的贡献止步于此——严格的数学证明由高德纳本人完成，他在论文中逐步推导了为什么这个构造确实生成长度恰好为m的三次方的圈。偶数情况至今仍是开放问题。

高德纳在论文中写道，这让他不得不「修正自己对生成式AI的看法」。但他同时强调，Claude在探索偶数情况时表现明显退化，Stappers不得不中止。这不是AI独立攻克数学的故事，而是一种新的协作模式：AI负责大规模算法探索和模式发现，数学家负责提炼、验证和证明。

02AI代码代理越来越能写，但「谁来验证」的问题越来越尖锐

阿里最新的Qwen3-Coder-Next只激活80B参数中的3B，就在主流代码基准上跑出接近旗舰模型的修复能力，证明小参数也能撑起强代码代理。

但BeyondSWE讲了另一个故事。这个覆盖500个真实案例的基准测试把评估从「单仓库bug修复」扩展到跨仓库推理、依赖迁移和整库生成，当前最强代理的表现断崖式下降。单仓库修复中得分亮眼的模型，碰上跨代码库理解依赖关系的任务，几乎完全失效。

矛盾在于：代理在简单任务上越来越可靠，开发者自然会信任它处理更复杂的任务，但能力边界不会提前通知你。定理证明工具Lean的创建者最近撰文直问：当AI写的代码越来越多，谁来验证？de Moura认为形式化验证将从学术课题变为工程必需品，用数学证明程序正确性，不再只属于航天和金融。

BeyondSWE的数据佐证了这个判断：代理不是在所有任务上「差一点」，而是在特定任务类型上完全失效，且失效模式不容易靠人工审查发现。

03Simon Willison发布AI代理工程指南，「反模式」清单直指行业共性问题

「不要把你没审过的代码扔给协作者。」独立开发者Simon Willison在最新发布的AI代理工程指南中，把这条列为首要反模式。他描述的场景在开发团队中已经越来越常见：有人用代理生成了几百甚至上千行代码，未经审查就提交了Pull Request，实际上是把验证工作转嫁给了队友。

这份指南在Hacker News上获得471票和274条评论，讨论热度本身说明了一个问题——AI代理工程目前没有行业标准，开发者在各自摸索中积累的经验碎片，正在充当事实上的规范。Willison的总结之所以引发关注，不是因为他说了什么新鲜事，而是因为他把很多人隐约感觉到但没有系统表达的实践问题写成了清单。

指南覆盖了代理工程的多个层面，但反模式部分最具实用价值。除了未审查代码的问题，他还警告了过度依赖代理输出、忽视上下文管理等常见陷阱。这些反模式的共同特征是：开发者把代理当成了可以完全信任的同事，而非需要持续监督的工具。

这种信任错位在个人项目中代价有限，但在团队协作中会迅速放大。一个人提交的未审查代码，消耗的是整个团队的审查资源和技术信任。当越来越多团队引入AI代理，「谁为代理生成的代码负责」正在从技术问题变成协作问题。