丘成桐弟子带队用 Lean 与 AI 完成庞加莱猜想机器验证，470 万行代码零 sorry

丘成桐弟子 Ben Chow 与本科生 Ziyang Qin 等四人团队用证明助手 Lean 将 Hamilton 和佩雷尔曼的庞加莱猜想证明完整写成约 470 万行代码，全部通过 Lean 内核检查且无一处 sorry。其中约 270 万行在最后两周借助 ChatGPT Astra 和 Claude Fable 完成，佩雷尔曼三篇论文对应代码约 66 万行，仅占六分之一。