Import AI 478：用数学助力对齐、ProgramBench、Mirendil 展示什么是 RSI
AI 安全公司 Resolution 自动形式化了统计学习理论相关数学命题（奇点消解），用编排智能体协调多个智能体写 Lean 和纸笔推导，耗时约一周、花费约 135,000 美元 token、产出约 60 万行 Lean 代码。
#编码
Import AIAI 评分4848
The DecoderAI 评分6767 研究称花哨编码 Agent 框架推高成本但不提升通过率
Liu 和 Han 的研究用 Qwen3.6、Qwen3.8、Deepseek-V4-Flash、GLM-5.3-Flash 和 HY4-Preview 五个模型在 Claude Code、OpenCode 和 mini-SWE-agent 三个框架上测试，发现换框架带来的任务结果波动与同设置重跑相当，通过率差异多在测量噪声内，唯一稳定落后的是 OpenCode，最多落后九分。
GitHub Blog · AI & MLAI 评分5454 GitHub 发布开源基准 ReviewBench 用于评测 AI 代码审查
GitHub 发布开源离线基准 ReviewBench，用于评测 AI 代码审查 Agent，现已开放使用。基准基于 1.039 亿 GitHub 真实 pull request 构建分布，语料包含 19 种语言的 219 个公开 PR，采用多来源 golden set、Claude Sonnet 5 作为 LLM 评分器，资深工程师独立复核与基准一致率达 96.6%。
Berkeley AI Research精选AI 评分6161 K-Search 通过 CUDA 到 MLX 翻译层将内核优化经验迁移到 Apple Silicon
研究者基于 UC Berkeley Sky Lab 的 K-Search 演化式内核搜索框架，新增 MLX 后端和结构化 CUDA 到 MLX 翻译层，让现有 CUDA 内核知识自动适配 Apple Silicon。
推荐理由：原文给出结构化 CUDA 到 MLX 翻译层的做法和可复现步骤，读者能了解跨硬件迁移内核优化经验的可行路径。