佩雷尔曼的证明被AI自动形式化了？我选择不信

有人把佩雷尔曼证明庞加莱猜想的完整论证丢进AI，宣称已经自动形式化完成。我第一反应是：认真的吗？那套Ricci flow正则性定理横跨几百页非正式推导，当年整个学界花了数年才理清。现在一个GitHub仓库声称一键搞定？ 说句不客气的判断：当前自动形式化工具的天花板还停在组合优化和代数几何的浅层，拿它硬啃百年几何猜想的核证明，勇气可嘉，可信度很低。但如果哪天真成了，那将是AI进军数学前沿的地震级事件。先当个信号，不当结论。

原文：Hamilton–Perelman's proof of Poincaré conjecture is claimed to be autoformalized · 来源：Hacker News