QUANTUM · AI · SCIENCE
每日快读，追溯证据；每周梳理技术与产品机会。
Dor Minzer与Yumou Fei、Shuo Wang在OpenAI公布AI生成证明前，抢先发布了对Khot“2-to-1游戏”猜想弱化版的“4-to-1游戏”证明。三人用95页论文证明了经典图着色问题的一项困难性结果；OpenAI随后公布包含Lean形式化验证的“2-to-1游戏”猜想证明及376项其他数学结果，但报道指出其手稿由AI生成，未经人工编辑或独立专家评审。
本站判断：文章对比人类研究者与OpenAI在“唯一游戏”相关猜想上的证明路径，呈现AI生成数学证明带来的研究竞争、验证与长期项目风险。
OpenAI 公布内部前沿模型在数学开放问题上的新结果，并在 GitHub 分享 Lean 证明形式化与研究细节。当前材料仅为摘要，未说明具体问题、模型名称、结果范围或代码许可。
本站判断：原文公开了数学开放问题的模型结果、Lean证明形式化与研究细节，为评估相关推理方法及其形式化证据提供入口。
Ai2 开源 AstaBrief 8B，用于根据研究问题和检索到的文献片段生成带引用的报告，并已作为 Asta 的 Fast mode 提供。该模型基于 Qwen3-8B，采用监督微调和直接偏好优化；作者称 Fast mode 平均生成时间为 51.1 秒，对比 Thinking mode 的 178.5 秒快约 3.5 倍。
本站判断：文章公开了模型、训练数据与报告生成流程，并说明数据过滤和简化系统设计对速度与引用归因的影响。
Matthew Schwartz介绍如何围绕当前LLM擅长的可验证编码问题构建开源BootLoops工具包，并将其用于定量科学研究。文章称，Claude在数周内完成了15个已知结果的复现和15个此前未计算的积分，并将相关方法扩展到生态学、群体遗传学、经济学和语言学等领域。作者同时强调，当前模型仍需要人类提供问题方向、领域判断和结果审查。
本站判断：文章把适配模型能力的问题选择、专家校验与可复核计算串成可复用流程，并给出BootLoops的开源入口。
Anthropic称，Claude通过约950个Agent、21小时搜索和2.1亿个token，从大规模DNA数据中发现了新型酶系统ART。初步实验显示，ART的重复序列可表达为一组不同的短RNA，但其主要功能和具体机制仍在研究中，相关预印本和技术报告已发布。
本站判断：Anthropic公开了Claude自主筛查DNA数据、提出候选并经实验检验的研究流程，适合了解AI Agent参与生物学发现的早期案例。
企业主题按主体汇集资料；量子与通用 AI 进展按具体任务区分。