AI写470万行代码验证庞加莱猜想

近日，人工智能在数学领域的应用取得突破性进展。一个由四人组成的科研团队，在UCSD数学教授Ben Chow（丘成桐的学生）的带领下，成功将庞加莱猜想的完整证明转化为计算机代码，共计470万行，并通过机器内核检查无遗漏。这是千禧年七大数学难题中首个被机器形式化验证的证明，开创了AI参与复杂理论证明的新纪元。

该团队采用证明助手Lean作为开发工具，将佩雷尔曼关于Ricci流的证明从头到尾编码完成。值得注意的是，约57%的代码（270万行）是在项目最后两周内由AI协助生成的，其中包括ChatGPT Astra和Claude Fable等大型语言模型。团队统计显示，最终依赖链共包含14197个代码文件，总计约402万行核心代码。其中，佩雷尔曼三篇论文对应的代码仅占约66万行，不足总量的六分之一，其余部分涵盖了分析学、微分几何等基础数学领域。

这项成就的关键在于团队创新的协作模式：人类研究者负责定义数学方向和验证结果，而AI则承担代码编写、错误检测和资料查找等具体任务。专家认为，这一成果不仅推动了数学证明的形式化发展，也为AI在科学研究中的应用开辟了新路径，未来类似的协作模式可能扩展到更多复杂的数学问题甚至其他科学领域。

庞加莱猜想是千禧年七大数学难题之一，其证明过程极为复杂。团队的工作展示了AI在科学探索中的潜力，随着技术的不断发展，AI与人类科学家的合作模式将进一步深化，为解决更多复杂的科学问题提供新的可能。