姚期智、杨植麟联合署名论文推出TCSExam，评测9个前沿大模型的理论计算机科学能力
姚期智团队联合杨植麟等发表署名论文《TCSEXAM：在TCS研究的全范围内评估前沿大型语言模型》，推出TCSExam评测，把定理证明、求解器工程、构造和开放猜想四类任务纳入同一考卷，由Lean内核等机器验算。
入选理由论文把理论计算机科学的定理证明、构造、求解器与开放猜想纳入统一评测，研究者可据此判断大模型在哪些数学任务上已能产出可机器核验的结果。
全部动态
按时间排列的全部内容。默认只显示通过双重评分的入选条目；切换到“全部收录”可以检索所有抓到的资料。
18 条入选报道，更新于 20:37
11月9日
星期一，1 条10月28日
星期三，2 条OpenAI 宣布数学、计算机科学与物理学三项成果，发布方式引发科研界不满
OpenAI 于当地时间周一宣布在数学、计算机科学与物理学领域取得三项突破，并称将调整成果发布方式。数学方向称已在全部维度上证明挂谷猜想，AI 生成的推导内容直接放出交由学界解读；计算机科学方向称证伪指数时间假说，由 OpenAI 组建外部研究小组解读；物理学方向围绕量子色动力学与杨-米尔斯理论，暂不公开，交由外部专家团队决定发布形式。
入选理由三项成果的公开程度各不相同，研究者可据此判断核验门槛与参与空间在哪里。
OpenAI 与 Anthropic 称模型推翻指数时间假说，计算机科学家组织公开讨论
OpenAI 发布了对三个数学难题的解答，其中一项声称推翻了计算机科学中长期使用的指数时间假说（ETH），Anthropic 随后也发布了自己的 ETH 反驳结果。
入选理由报道呈现了计算复杂性领域对 AI 证明的公开回应与后续核查安排，研究者可据此判断这类成果的验证路径。
10月27日
星期二，3 条OpenAI公布数学、计算机和物理学3项新发现，涉及挂谷猜想与杨–米尔斯理论
OpenAI于当地时间10月26日宣布在调和分析、复杂性理论和量子场论三个方向取得新发现，称其模型给出了局部光滑猜想在所有维度下的证明，并证明指数时间假设（ETH）为假，还严格证明了包含规范场与费米子的四维相互作用量子场论。
入选理由三项成果均待学界独立验证，外部专家团队参与核查的安排，为研究者判断AI产出可信度提供了参照。
OpenAI 公布数学、计算机与物理三项 AI 成果，并引入外部专家把关
OpenAI 公布三项由 AI 产出的“重大”成果：数学上给出欧氏波动方程局部光滑性的证明，并称由此解决 Kakeya 猜想与 Stein 限制性猜想；计算机科学上给出确定性算法，称 3-SAT 情形可反驳指数时间假设（ETH）；物理上给出含规范场与费米子的四维相互作用量子场论的数学严格存在性证明，涉及 QCD 与标准模型统一完成，但物理部分未全文公开。
入选理由OpenAI 公布数学、计算机科学与物理三项 AI 输出，并首次引入外部专家把关，同时其数学顾问小组反对这种指定专家先看结果的做法。
OpenAI 称模型在数学、算法与量子场论取得三项成果，部分证明已公开
OpenAI 宣布其模型在数学、计算机科学和物理学取得三项成果：证明适用于所有维度的局部光滑猜想并由此解决挂谷猜想与斯坦因限制猜想，给出推翻指数时间假设（ETH）的证明，以及提出量子色动力学和纯杨-米尔斯理论存在性的严格数学证明。
入选理由三项成果分别涉及调和分析、计算复杂性假设和量子场论存在性，数学与算法部分已公开 Lean 形式化证明，物理部分仍在专家审查中。
10月25日
星期日，1 条h1 用简单智能体循环在 Lean 4 中刷新形式化定理证明基准并解决 8 个开放问题
研究团队提出 h1，一个给模型提供 Lean 4 高效接口、依靠验证器反馈与自我反思持续尝试的简单 harness，不预设分解或搜索结构。
入选理由对做形式化证明的研究者来说，这篇给出了一个反直觉的对照结果：简单智能体循环加高效 Lean 接口，可能比人工设计的分解与搜索流程更划算。
10月23日
星期五，1 条黎曼 ζ 函数临界零点比例新进展：从 Montgomery 到 Anthropic 与 Lamzouri
Caroline Turnage-Butterbaugh 在 Terence Tao 博客客座撰文，梳理黎曼 ζ 函数临界线上非平凡零点比例下界的研究脉络，从 Selberg、Levinson、Conrey 到 2020 年 Pratt 等人的 41.7%。
入选理由作者以第一手视角梳理黎曼 ζ 函数临界零点比例的最新进展，并解释 Anthropic 模型与 Lamzouri 两条证明路径的差异。
10月22日
星期四，1 条微软研究者证明 31 年未解的 KLS 猜想，AI 智能体参与探索证明路径
微软研究院机器学习与优化组的 Xinzhi Zhang 与合著者 Zhao Song 证明了 1995 年提出的 Kannan-Lovász-Simonovits（KLS）猜想，证明该关系在高维下由固定常数界定、不随维度增长。
入选理由微软研究者用人类主导的智能体搜索证明 KLS 猜想，展示了 AI 在数学证明中承担探索、研究者负责判断的分工。
10月19日
星期一，1 条OpenAI 宣称证明准黎曼猜想，数学家如何评价
OpenAI 在 2026 年 10 月 6 日公布的 377 项结果中，有一项宣称解决了准黎曼猜想，即黎曼猜想的一个较弱版本。斯坦福大学的 Jared Duker Lichtman 称这项新证明是迄今 AI 用于数学最重要的成果，且领先幅度相当大。
入选理由材料交代了 OpenAI 宣称解决准黎曼猜想及数学家对其分量的评价，可据此判断 AI 在数学证明中的位置。
10月18日
星期日，1 条Épi 自主研究智能体产出 120 项纪录结果并给出 Tuza 猜想新证明
研究团队发布技术报告，介绍跨会话持续运行的自主研究智能体 Épi，它结合分层记忆、版本化分支和独立评审，在固定验证规则下产出 120 项纪录结果，包括 20 项数值界纪录和 100 项构造纪录，其中 n-queens 常数区间收窄约 84 倍，四次 Feigenbaum 吸引子维数的严格区间收窄超过 360 万倍。
入选理由作者团队公开了可核查的构造与证书，研究者能据此判断自主研究智能体在数学与算法设计上已能产出何种可检验结果。
10月16日
星期五，2 条Claude 查明 NIST ECDSA 曲线种子来源：由 Unix 时间戳初始化的 lrand48 生成
Anthropic 称，一名员工让内部研究模型 Claude 在不提供线索的情况下追查 NIST 椭圆曲线种子来源，Claude 在不到半小时内查明 P-192。
入选理由NIST 椭圆曲线种子来源这一长期悬案被 Claude 在半小时内解开，密码学与数学研究者可据此复核并复现。
Claude 自主设计出更省资源的量子电路，八项任务均优于已发表方案
Anthropic 用自然语言规格和自动评分器让 Claude 在闭环中设计量子电路，在化学、优化、量子模拟、数论和数值计算共八项任务上给出比已发表最优方案使用更少量子比特和门的新设计，部分提升达一个数量级以上。
入选理由Anthropic 让 Claude 在闭环中自主设计量子电路，八项任务均优于已发表设计，为量子算法资源估算提供了可复用的自动化路径。
10月15日
星期四，1 条上海AI实验室许地生团队用书生-S2 人机协同证明三维Ghys猜想
上海人工智能实验室访问学者、大湾区大学教授许地生团队依托书生科学多模态大模型S2（书生-S2），通过人机协同完成困扰数学界30余年的三维Ghys猜想证明，论文已发布在预印本平台arXiv，形式化代码在GitHub公开。
入选理由材料完整呈现了人机协同证明数学猜想的流程与形式化验证环节，研究者可据此判断大模型在自身领域承担长程推导的可行边界。
10月2日
星期五，1 条UCLA 团队发布 Ansatz：用持续图记忆的数学研究智能体解出多个开放问题
UCLA 团队提出数学研究智能体 Ansatz，其核心是持续图记忆（Continual Graph Memory），用依赖图组织事实、计划与反例等中间结果，并支持跨问题复用经验。
入选理由数学研究智能体 Ansatz 用图记忆组织证明搜索，在十个基准问题上全部通过，并独立给出四个开放问题的完整解。
10月1日
星期四，1 条Google DeepMind 发布 Gemini 4 Argon，输出上限提至 100 万 token
Google DeepMind 发布前沿模型 Gemini 4 Argon，先通过 Fairwind Program 向受信任的网络防御方开放，随后逐步扩展到开发者、企业和消费者，起步价为每百万输入 token 2 美元、每百万输出 token 10 美元。
入选理由Gemini 4 Argon 把长程推理和百万级输出用于代码迁移、漏洞发现与科研优化，研究者可据此判断它在自身工作流中的位置。
9月21日
星期一，1 条上海AI实验室发布开源科学基础大模型书生-S2，科学任务评测领先并即将接入书生·端砚平台
上海AI实验室在2026浦江创新论坛上发布书生多模态大模型S2（书生-S2），称其在知识、代码、智能体等通用能力上处于开源模型第一梯队，在Biology-Instructions。
入选理由上海AI实验室公开了书生-S2的权重与体验入口，并说明其可插拔专业记忆如何在不重训基座的情况下扩展学科能力，研究者可据此判断能否用于长程科研任务。
8月3日
星期一，1 条Qwen 发布 Qwen3.8-Max：2.4 万亿参数，主打长周期自主科研与工程任务
Qwen 团队发布 Qwen3.8-Max，称其为 Qwen 系列迄今最强模型，参数规模 2.4 万亿（95B 激活），已通过 QwenCloud 提供 API，权重将于下周在 Hugging Face 和 ModelScope 开源。
入选理由材料展示了模型在论文复现与改进、量化因子挖掘、芯片设计等长周期科研任务上的自主执行过程，研究者可据此判断其能否介入自己的实验与计算流程。