丘成桐弟子带AI狂写470万行，庞加莱猜想证明首次被机器完整验证！ **新智元报道** 刚刚，千禧年难题庞加莱猜想的完整证明，被整个写成了代码！ 干成这件事的，只是一个四人小团队。 带头的是丘成桐的弟子，一位研究了几十年Ricci流的老教授，冲在最前面的是一个刚毕业的本科生，身后是一群24小时连轴转的AI。 他们用证明助手Lean，把Hamilton和佩雷尔曼的证明从头写到尾，总共约470万行代码。 其中约270万行，是最后两周在ChatGPT、Claude等AI的帮助下赶出来的。 这470万行已经全部通过Lean内核的检查，没有一处用sorry留着「以后再证」。 过去，一个大证明要让数学界说一句「没毛病」，得靠同行花上好几年逐页审读。 这一回，说了算的换成了机器，写证明的主力也换成了AI。 佩雷尔曼的毕生心血，竟然只占六分之一** 我们把整个仓库下载下来，顺着最终的庞加莱定理，把它直接和间接引用的代码全部找了出来。 真正用到的有14197个代码文件、约402万行，最长的一条引用链串起了353个文件。 其中，佩雷尔曼三篇论文对应的代码加起来约66万行，只占六分之一。 论文写得越简略，L