AREX Feed Article
曾揭穿 GPT-5 数学宣传的 Thomas Bloom 背书 Astra 成果为"大新闻"；$2,000 总成本与 Altman 华盛顿演示细节曝光
曼彻斯特大学数学家 Thomas Bloom——正是他去年 10 月当场揭穿 OpenAI 前 VP Kevin Weil 关于"GPT-5 解决 10 个 Erdős 问题"的虚假宣传——在 Astra 公告发布当日便在 X 上给出了正面评价："Big news！……从构造的角度来说，这很重要。"他明确将 Astra 的 10 项成果排在 5 月单位距离反例之上。这条帖文获得 372 次点赞、42,553 次浏览，其分量在于：Bloom 是 erdosproblems.com 的维护者，也是此前对 OpenAI 数学声明最有力的外部监督者之一。
Bloom 从"打假者"到"背书者"的转变，为围绕 Astra 的争论增添了重要砝码。此前包括 Gary Marcus、Henry Yuen、Francesco Fournier-Facio 在内的批评者主要聚焦于透明度缺失、证明风格和原创性归属——而 Bloom 的评估恰恰从"成果本身是否重要"这一维度给出了肯定判断。
$2,000：从"登月叙事"到"账单叙事"
SiliconANGLE 和 Forbes 的报道确认了一个此前未被披露的关键数字：OpenAI 表示 10 个解法的总 token 成本约 $2,000（按 Sol API 费率计算），平均每题约 $200。Noam Brown 将此轻描淡写为"我们没有在每个问题上花很多钱"。
这一数字同时承担两种解读：支持者将其视为"科研平权"——边际成本趋近于零意味着任何有微量经费的实验室都能参与前沿研究；怀疑者则指出这只是"分子"——OpenAI 未公布尝试但失败的问题数量（Brown 承认"我们也尝试了其他重大问题但没有成功"），真实实验成本未知。
Altman 在公告三天前已向华盛顿演示
The Information 于 7 月 31 日率先报道：Sam Altman 在 Astra 数学公告发布前三天（7 月 29 日），亲自向华盛顿的政策制定者和监管机构演示了 Astra。这一时机与 TRAINS 框架的推进重合——Astra 据称是首个将经过该联邦审查流程的模型。在公告中，OpenAI 明确引用了数学界 6 月发布的 Leiden Declaration，并拒绝将人类署名归于任何一项证明——这一姿态可被解读为对新监管框架的合规示范。
GitHub 仓库上的 Lean 证书"抱歉计数"（sorry count）为零——意味着 10 项证明中没有任何一个逻辑步骤未经编译器验证。但这不改变一个问题：外界仍无法接触 Astra 模型本身，只能验证其输出。