扩展 Lean 定理证明以验证真实世界代码

我们提出了 EasyProver，这是一种由具备隔离上下文的递归代理、异步搜索、并行策略探测和弹性 elaboration 服务构建的 Lean 证明系统。在无需额外训练的情况下，使用现成的前沿模型，它证明了 669/672 个 PutnamBench 问题和全部六个 IMO 2026 形式化问题，并通过证明或反驳解决了 597/600 个 NTP4VC 验证条件以及全部 189 个 VERINA 任务。由于这些基准已经接近饱和，我们还引入了 Aegis，将竞赛编程问题转换为针对真实实现的难度高得多的验证任务。该流水线编写安全的 Rust 解法，使用 Aeneas 将其翻译为 Lean，生成规格，并为每个冻结的命题标注经内核检查的证明或反驳结果。它生成了 2,045 对经过差分验证的 Rust-Lean 程序，以及 11,533 个候选规格。不同于手写基准，这些任务包含来自定宽算术、显式失败、生成的循环、类型转换和函数化变更操作等方面的实现级义务。在由 2,000 个命题构成的分层样本上，EasyProver 在每个命题 30 分钟的预算内证明了其中 1,054 个（52.7%）。这些任务还可用于评测其他证明器，以及作为强化学习的奖励。