OpenAI 内部 Astra 模型攻克十道数学难题，成本低于 2000 美元
评分
68披露了具体成本、形式化验证和复盘文档，但缺少失败案例与提示词，信息有增量但非完整。
来源为知名博主且引用原始仓库与论文，但属于二手转述，分析深度有限。
对数学研究者和 AI 应用者具有启发意义，但暂无直接可复用的实操细节。
该事件为近期发布，且与当前 AI 数学研究热点高度相关。
Simon Willison 是可信的技术博主，内容链接到官方仓库和论文，可靠性较好。
基础分 75.5 × T2 信源权重 ×0.9 = 68
精选线 70未达精选线
精选理由
内容具有高信息增量，但缺乏失败案例和提示词细节，评分取中高位。
AI 点评
「这则新闻真正值得关注的点不是 AI 解了几个题，而是成本降到了 2000 美元以下——这让自动化数学发现第一次具有了日常可用的经济性。对数学家和 AI 研究者来说，提示词与失败数据的缺失是最大悬念，建议去翻原仓库和论文核对细节。」
速览
继 Anthropic 用 Claude 发现密码学弱点后，OpenAI 也展示其下一代模型 Astra 的实力：在十个至少十年无进展的数学问题上取得突破，每个问题耗费的 token 成本不到 2000 美元。OpenAI 公开了 Lean 4 形式化证明、论文以及由模型根据推理轨迹生成的复盘 PDF，透明度较高，但未披露提示词。数学家群体对此反应类似“深蓝时刻”。陶哲轩曾提出“大数学”愿景，认为 AI 将成为人机协作解决复杂数学问题的关键催化剂。
- OpenAI 用内部 Astra 模型解决了十个搁置超过十年的数学难题，单个问题 token 成本低于 2000 美元。
- 项目开源了 Lean 4 形式化证明和论文，并附有模型基于推理轨迹生成的复盘 PDF。
- OpenAI 未公布具体提示词，数学家们惊呼这是 AI 的“深蓝时刻”。
正文
Ten advances in mathematics and theoretical computer science
A few days ago it was Anthropic discovering cryptographic weaknesses with Claude using Mythos Preview, spending $100,000 on tokens and with prompts that included "again we are not looking for low hanging fruit, we want proper research to find genuinly hard findings."Now it's OpenAI's turn to flex. They set "an internal version of Astra, our next major model" on finding solutions to ten mathematical problems that "have seen no progress on the main result for at least a decade". They claim to have spent less than $2,000 at GPT-5.6 Sol token prices on each one.
(No news on how many problems they spent $2,000 on without reaching a solution though.)
The openai/ten-proofs repository has Lean 4 formalizations of their results, and there's also a paper describing the solutions and an additional LLM-generated PDF where the model "reconstructs how the proof came together" based on the unpublished reasoning traces.
That's a decent level of transparency, but I want to see the prompts they used!
A lot of mathematicians online are experiencing a collective burst of Deep Blue.
OpenAI's results reminds me of what Terence Tao described as "big mathematics" in IEEE Spectrum in June:
Unlike some of his peers, Tao is neither dismissive of AI nor fearful. Instead, he sees it as the catalyst for a fundamental shift in the discipline—a transition toward what he calls “big mathematics.” He envisions a future of large-scale, decentralized collaborations between humans and machines, where complex mathematical tasks can be diced and sliced, with humans claiming the creative parts and AI doing the lion’s share of the technical grunt work.
Via Hacker News
Tags: mathematics, ai, openai, generative-ai, llms, deep-blue
相关条目
精选DeepSeek V4 在 OpenRouter 上的代币份额翻倍，智能体工作负载成主要驱动力
DeepSeek V4 的快速采用表明市场对高性能、低成本推理模型的强烈偏好，尤其是智能体场景将重塑 AI 部署格局。
91
精选启用两项设置使ARC-AGI-3基准测试分数提升三倍
这项发现太关键了！它表明模型的性能不仅取决于训练，还取决于推理时的配置。对于AI工程师和研究者来说，这是一个必须注意的优化方向。特别是那些在资源受限设备上部署模型的团队，可能会因此找到低成本提升能力的方法。
91
精选GPT-5.6：前沿智能与前沿效率的融合
这条消息值得关注，因为它标志着大模型竞争从单纯拼参数转向拼效率。对于AI开发者和企业决策者来说，GPT-5.6意味着可以用更少预算获得更高性能，尤其适合那些被推理成本挡在门外的长上下文或Agent场景。OpenAI这一步，可能重新定义‘前沿’的标准。
91
精选LFM2.5-Encoder：面向CPU快速长上下文推理的新模型
这篇博文让我眼前一亮，因为它直接解决了大模型在CPU上跑长上下文的痛点。对于没有高端GPU的团队或个人开发者，LFM2.5-Encoder系列提供了可立即使用的开源方案。尤其推荐给做RAG、文档搜索或代码分析的朋友——现在用普通服务器就能处理百万级token的文档了。
91
精选GPT-Red：OpenAI通过自我对弈实现AI红队自动化，提升模型鲁棒性
GPT-Red 是红队测试从人工到自动化的里程碑，特别适合安全工程师和对齐研究者关注。它直接降低了测试成本，但也引发了对“自动攻击”本身的伦理讨论——值得所有关注AI治理的人深入思考。
91
精选OpenAI推出GPT-5.5生物漏洞赏金计划
这个计划值得关注，因为它首次将AI漏洞赏金制度拓展到生物安全领域，不仅为安全社区提供了新的研究方向，也为AI风险治理提供了实际演练场。对模型安全研究者、生物安全专家以及关心AI双重用途的从业者尤其重要。
91
精选vLLM推出原生速度Transformers建模后端，大幅提升推理性能
这项更新对于AI工程团队非常关键：无需格式转换意味着能更快地迭代模型，而2-5倍的速度提升直接降低GPU成本。如果你正在做LLM在线服务或者批量推理，这几乎是必读的技术更新。
90
精选Google DeepMind 发布手语转文本模型 SL2T，助力聋人用户
这则消息的意义不仅在于技术突破，更在于AI开始真正关注边缘群体的需求。对开发者而言，SL2T的架构思路和技术路径值得深入研究；对无障碍倡导者来说，这是推动行业标准的重要案例。