EasyProver 系统在 Lean 定理证明上逼近基准饱和并推出更难的 Aegis

EasyProver 用递归智能体、隔离上下文、异步搜索和并行 tactic 探测构建 Lean 证明系统，无需额外训练，在 PutnamBench 上解决 669/672 题，并完成全部 6 道 IMO 2026 形式化题目。在代码验证方向，它解决了 597/600 个 NTP4VC 验证条件和全部 189 个 VERINA 任务。由于这些基准接近饱和，团队推出 Aegis，将竞赛编程题转换为基于真实 Rust 实现的更难验证任务，产出 2,045 个经差分验证的 Rust-Lean 程序对和 11,533 条候选规格。在 2,000 条语句的分层抽样中，EasyProver 在每题 30 分钟预算内证明了 52.7%。