打开网易新闻 查看精彩图片

数学家陶哲轩又整活了。这次他盯上的是Knuth《计算机程序设计艺术》里一道悬了半个世纪的题目——"Claude Cycles"问题。Knuth本人悬赏多年，解法始终没人交卷。

打开网易新闻 查看精彩图片

陶哲轩的打法很新鲜：不纯靠人脑，也不让AI单干。他把Claude当成"灵感生成器"，Lean 4证明助手当"逻辑安检员"，自己则负责判断哪些直觉值得追下去。三周下来，一个原本需要数年试错的方向被他筛了出来。

打开网易新闻 查看精彩图片

他在帖子里写了这么一句：「AI生成的候选解法中，大约有90%是错的，但剩下的10%里藏着人很难想到的结构。」这话说得实在。AI不是答案机，是块磨刀石——把你的思路磨得更刁钻。

最终证明被Lean 4完整验证，陶哲轩把过程开源到了GitHub。Knuth的支票大概已经在路上了，但更让人在意的是这套"人机混合"的模板：数学家负责提问和拍板，AI负责穷举可能性，证明助手负责堵住逻辑漏洞。分工明确，谁也不抢戏。

有同行在评论区问，以后数学系要不要开Prompt Engineering课。陶哲轩没回，但点了赞。