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