OpenAI研究员于8月1日宣布，该公司未发布的Astra模型成功证明了10项前沿数学难题并提供了Lean证书[1]。这些难题的主要结论至少十年未被推进，其中不少搁置长达数十年[1]。根据研究员Noam Brown的介绍，寻找这10项解法的推理成本折合不到2000美元[1]。
令人瞩目的是，Anthropic研究员Levent Alpöge仅用不到24小时的时间，便利用公开可用的Fable模型独立复现了其中5项成果[1]。这5项分别是第4、5、6、7、8项难题[1]。值得注意的是，Fable是Anthropic早已公开的模型，任何人都可以调用[1]。Fable的复现条件严格遵循了完全自主、通用提示词、全程无网络、防止泄漏等要求[1]。
这次对标展示凸显了AI在数学前沿领域的能力进展，同时反映出首发优势的快速缩水——从以年计的差距，如今已压缩至仅保持24小时的窗口期[1]。
OpenAI researchers announced on August 1 that their unreleased Astra model had proven 10 cutting-edge mathematical theorems and provided Lean certificates for each [1]. The proofs were completed at a computational cost of less than $2,000 according to researcher Noam Brown [1]. The 10 problems targeted represented major unsolved questions in mathematics, with many having remained stalled for decades and no progress made on them for at least the past 10 years [1].
Within less than 24 hours, Anthropic researcher Levent Alpöge independently reproduced 5 of the 10 proofs using Fable, Anthropic's publicly available model [1]. Specifically, Alpöge reproduced problems 4, 5, 6, 7, and 8 [1]. Fable's reproduction was conducted with complete autonomy using only generic prompts, operated entirely offline to prevent information leakage, and required no external assistance [1]. This rapid reproduction underscores how quickly technological advantages in AI research are diminishing—what once represented a lead measured in years has now compressed to a single day [1].
