四人团队用 Lean 把庞加莱猜想证明写成 470 万行代码

四人团队用证明助手 Lean 把庞加莱猜想的完整证明全部代码化，总量约 470 万行，由 Lean 内核逐行验证通过，没有留下用 sorry 占位待补的证明。这次形式化改走了一条 alternative blow-up 路线，而不是 Hamilton 原始的规范化流证明。

更值得注意的是人力构成与速度：**约 270 万行是在最后两周完成的**,由 ChatGPT、Claude 等 AI 工具协助生成。团队内核包括一位丘成桐弟子、一位资深 Ricci 流研究者，以及一名刚毕业的本科生。以往这种体量的大证明要靠同行逐页人工审阅、耗时数年，这次把验证交给了机器内核 —— 具体证明细节与仓库情况见原文。

💡 为什么值得看AI 证明千禧年难题，470 万行机器验证。