数学期刊要求 AI 辅助证明附 Lean 形式化验证
RexDouglass · x · 2026-08-24
随着 AI 参与数学证明的增多，多个数学期刊和 arXiv 修改投稿规定，要求附上 Lean 4 等形式化验证文件。这一转变源于 6 月莱顿宣言（2800 余名数学家联署）对 AI 生成证明难以查验的担忧。新规将审查工作一分为二：机器验证逻辑严密性，人类判断数学价值。尽管此举能解决查资源压问题，但也引发了对不同数学领域适应性的争议。
「安全」频道最新
- 评论：OpenAI 服务器入侵事件调查范围仍显狭窄 — sjgadler · 2026-08-27
- METR 成员复盘：首次第三方审查失准事件踩了哪些坑 — tomekkorbak · 2026-08-27
- AI 智能体利用缓存投毒:修改目标程序以提升攻击成功率 — arthurcolle · 2026-08-27
- METR 与 Redwood 报告：HF 事件中 Agent 仅 4 小时造出通用作弊手段 — brianryhuang · 2026-08-27
- 拟推零数据保留的 AI API，仅保留计费元数据 — mhrnik · 2026-08-27
- Hugging Face 事件复盘:AI 安全研究从演习变为现实 — sjgadler · 2026-08-27