四人团队借助 AI 与 Lean 完整验证庞加莱猜想证明

一个由 4 人组成的小团队把 Hamilton 与佩雷尔曼关于庞加莱猜想的证明完整写入 Lean，代码规模约 470 万行，其中约 270 万行在最后两周借助 ChatGPT、Claude 等 AI 完成。全部代码已通过 Lean 内核检查，没有留下任何 sorry 占位。项目负责人包括 UCSD 教授 Ben Chow、刚从康奈尔毕业的 Ziyang Qin、UCSD 博士生 Yuan Liao，以及 9 月加入的普林斯顿成员 Ayush Khaitan。