EasyProver
基于递归智能体与 Lean 定理证明器的形式化验证系统，通过隔离上下文的智能体并行搜索证明，无需专门训练模型即可达到高验证通过率
时间轴 (近 90 天)
EasyProver 是一套由递归智能体驱动的 Lean 证明系统，每个智能体拥有隔离的上下文，配合异步搜索、并行 tactic 探测与弹性 elaboration 服务。
EasyProver 使用现成的前沿模型，没有额外训练。
EasyProver 在 PutnamBench 上证明了 669/672 道题。
EasyProver 完成了全部六个 IMO 2026 形式化问题。
EasyProver 在 NTP4VC 上解决了 597/600 个验证条件。
EasyProver 完成了 VERINA 的全部 189 个任务，方式包括证明与反证两种。
EasyProver 的作者指出 PutnamBench、IMO 2026、NTP4VC、VERINA 等基准已接近饱和，并因此转向构建新基准 Aegis。
在一份包含 2,000 条语句的分层样本上，EasyProver 在每条语句 30 分钟的时间预算内证明了 1,054 条，占 52.7%。
EasyProver 在 Aegis 分层样本上的 52.7% 通过率表明，固定宽度算术与显式失败等实现细节仍是难点，系统在更大规模代码库、更长证明链上的表现以及 Aegis 生成规约的质量分布仍需独立分析检验。
全部知识事实 (9)
EasyProver 是一套由递归智能体驱动的 Lean 证明系统，每个智能体拥有隔离的上下文，配合异步搜索、并行 tactic 探测与弹性 elaboration 服务。
50%待验证EasyProver 使用现成的前沿模型，没有额外训练。
50%待验证EasyProver 在 PutnamBench 上证明了 669/672 道题。
50%待验证EasyProver 完成了全部六个 IMO 2026 形式化问题。
50%待验证EasyProver 在 NTP4VC 上解决了 597/600 个验证条件。
50%待验证EasyProver 完成了 VERINA 的全部 189 个任务，方式包括证明与反证两种。
50%待验证EasyProver 的作者指出 PutnamBench、IMO 2026、NTP4VC、VERINA 等基准已接近饱和，并因此转向构建新基准 Aegis。
50%待验证在一份包含 2,000 条语句的分层样本上，EasyProver 在每条语句 30 分钟的时间预算内证明了 1,054 条，占 52.7%。
50%待验证EasyProver 在 Aegis 分层样本上的 52.7% 通过率表明，固定宽度算术与显式失败等实现细节仍是难点，系统在更大规模代码库、更长证明链上的表现以及 Aegis 生成规约的质量分布仍需独立分析检验。
50%