编辑精选 · 布衣云水客 · 2026/10/23 10:09

Claude 生成 1.8 亿行形式化证明，由独立检查器核验

Claude写下1.8亿行证明，裁判却不是Claude

Anthropic 与 Theorem 宣布 Claude 在数周内为 123 个开源库的 239 个测试入口生成约 1.8 亿行证明，由独立 Rocq 检查器核验安全规则。该进展将形式验证扩展到多个开源库，并提及 Carbon-X 开放权重及 Perplexity 本地决策模型。

精选理由：原文展示了AI生成形式化证明的规模与独立核验机制，提供了判断当前技术边界和可信度的参考。