补充三个官方报告里没写在推文上的硬核内幕：

1. 投入产出算术反差：OpenAI 在发布会上透露，外部客户复现这个全流程等效算力账单约 1500 万美元，而克雷数学所官方悬赏才 100 万美元，OpenAI 明确表示放弃领取奖金。
2. 戏剧性抢跑内幕：据称 OpenAI 是 9 月 1 日听到学界同行（包括 Anthropic 员工）也在攻坚该问题的风声，才临时立项启动 1 万个 Agent，短短 88 小时强行“饱和轰炸”超车抢发。
3. 机器自证闭环：这次证明用 Lean 语言完成了机器形式化验证。哪怕全人类数学家还没来得及逐行读完，编译器已经确认逻辑无缝闭合。

当科学研究变成 1500 万美元一次的算力工业军备竞赛，中小科研机构和独立学者以后该怎么玩？欢迎在评论区聊聊。