丘成桐弟子带队用AI写470万行代码，庞加莱猜想证明首次被机器完整验证
RecodeX 重构消息，一个四人小团队借助证明助手Lean，将Hamilton与佩雷尔曼关于庞加莱猜想的完整证明写成约470万行代码，并全部通过Lean内核检查，未留一处sorry占位。其中约270万行是在最后两周借助ChatGPT、Claude等AI完成。
团队由UCSD数学教授、丘成桐弟子Ben Chow带领，成员包括今年5月刚从康奈尔毕业的本科生Ziyang Qin、UCSD博士生Yuan Liao以及普林斯顿的Ayush Khaitan。仓库中约402万行代码最终服务于一个仅23行的文件，其定理即庞加莱猜想本身。
据团队开源工具包，AI系统由研究者直接对话的“领队”主会话守住数学路线，后台“调度”智能体负责拆解与验收任务，临时智能体执行写证明、挑错与查资料。9月27日凌晨，拓扑版庞加莱证完，距计划表排出不到一周。