科技 · zh
丘成桐弟子带AI狂写470万行，庞加莱猜想证明首次被机器完整验证
刚刚，千禧年难题庞加莱猜想的完整证明，被整个写成了代码！ 干成这件事的，只是一个四人小团队。 带头的是丘成桐的弟子，一位研究了几十年Ricci流的老教授，冲在最前面的是一个刚毕业的本科生，身后是一群24小时连轴转的AI。 他们用证明助手Lean，把Hamilton和佩雷尔曼的证明从头写到尾，总共约470万行代码。 其中约270万行，是最后两周在ChatGPT、Claude等AI的帮助下赶出来的。 这470万行已经全部通过Lean内核的检查，没有一处用sorry留着「以后再证」。 过去，一个大证明要让数学界说一句「没毛病」，得靠同行花上好几年逐页审读。 这一回，说了算的换成了机器，写证明的主力也换成了AI。…
