Vero 的 audit 机制：让 agent 有权利说“这题出错了”
前几天翻到 8 月 13 号挂上 arXiv 的那篇 Vero，讲的是用 benchmark 评估 agent 在仓库级别同时写实现和写证明的能力。43 个多模块 Lean 4 仓库实例，带预定好的 API 接口、人工整理的 spec 和参考实现，支持 proofonly 和 codeandproof 两种模式。
Lean41 篇实战文章
前几天翻到 8 月 13 号挂上 arXiv 的那篇 Vero，讲的是用 benchmark 评估 agent 在仓库级别同时写实现和写证明的能力。43 个多模块 Lean 4 仓库实例，带预定好的 API 接口、人工整理的 spec 和参考实现，支持 proofonly 和 codeandproof 两种模式。