北京
分享至
数学家陶哲轩又整活了。这次他盯上的是Knuth《计算机程序设计艺术》里一道悬了半个世纪的题目——"Claude Cycles"问题。Knuth本人悬赏多年，解法始终没人交卷。
陶哲轩的打法很新鲜：不纯靠人脑，也不让AI单干。他把Claude当成"灵感生成器"，Lean 4证明助手当"逻辑安检员"，自己则负责判断哪些直觉值得追下去。三周下来，一个原本需要数年试错的方向被他筛了出来。
他在帖子里写了这么一句：「AI生成的候选解法中，大约有90%是错的，但剩下的10%里藏着人很难想到的结构。」这话说得实在。AI不是答案机，是块磨刀石——把你的思路磨得更刁钻。
最终证明被Lean 4完整验证，陶哲轩把过程开源到了GitHub。Knuth的支票大概已经在路上了，但更让人在意的是这套"人机混合"的模板：数学家负责提问和拍板，AI负责穷举可能性，证明助手负责堵住逻辑漏洞。分工明确，谁也不抢戏。
有同行在评论区问，以后数学系要不要开Prompt Engineering课。陶哲轩没回，但点了赞。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
