Anthropic 用 Claude 自动验证现有代码并生成数学证明
Anthropic 使用 Claude 为现有软件生成数学证明，并由独立验证程序 Rocq 自动检查；Anthropic 称，Claude 在数周内生成约 1.8 亿行证明代码。验证条件限于特定处理器架构、单线程程序和小于 64 MB 的输入，单项证明可能消耗数亿个 tokens。
#编码
The Decoder精选AI 评分7676 The DecoderAI 评分6666 研究比较三种编码 Agent harness：成本差异明显，通关率大多相近
Liu 和 Han 的研究比较了 Claude Code、OpenCode 和 mini-SWE-agent 对编码 Agent 任务表现与成本的影响，发现多数 harness 间的通关率差异落在测量波动范围内。