快讯
月之暗面发布 TCSExam，用形式化验证评测理论计算机科学任务
TCSExam 提供 100 个专家审阅任务及 20 题 Lite 子集，覆盖定理证明、求解器、构造与开放猜想。它强调可机械核验的结果，不等同于通用科研能力评测。
月之暗面研究团队公布理论计算机科学基准 TCSExam，相关论文于 11 月 5 日提交 arXiv。完整集合包含 100 个专家审阅任务，Lite 子集为 20 个，覆盖定理证明、求解器设计、构造问题和开放猜想四个方向。
任务通过 Lean 证明或程序执行等方式核验结果，减少单纯依赖文本评判的歧义。评测反映的是所选任务与验证条件下的表现，不能理解为模型已解决全部开放猜想或具备普适科研能力；项目仓库已公开。