开源动态8

Specula：数小时揪出开源系统382个深层bug

机器之心2026-08-26

AI 摘要

Specula团队：Specula让coding agent自动完成代码规约、模型检查等，在67个开源系统找到382个bug，将原本数月的形式化验证缩短至几小时，让形式化方法成普通开发者可用工具。

关注公众号

扫码关注
第一时间收到每日精选

公众号专辑

九章云极问鼎陶哲轩数学挑战赛

本文报道九章云极言表实验室在陶哲轩发起的数学蒸馏挑战赛第二阶段拿下全部赛道满分，解决28个未解决开放数学问题，介绍了其可验证AI+强化学习的AI4S布局。

OpenAI公开722篇由内部未发布前沿模型生成的数学成果，覆盖多数学方向，部分附带形式化证明，发布后引发数学界巨大冲击，消化验证需数年，不少青年学者研究项目遭毁灭性打击，本文梳理各方反应与争议。

顶尖数学学者Rishikesh Gajjala靠AI攻破博士课题，却宣布退出学术圈。他认为AI生成证明虽精巧但难验证，“漂亮证明未验证和垃圾无异”。他投身形式化验证领域，而AxiomProver完成“246定理”形式化验证。

AutoClip是基于AI的开源智能视频切片处理系统，能自动从多平台下载视频、提取精彩片段并生成合集。适合UP主、内容创作者等，有多平台支持、AI智能分析等特性，部署方式简单。