EasyProver以现成模型在多个Lean基准上取得高通过率，并推出更难的Aegis验证基准。
资讯摘要
论文提出EasyProver，一个由递归智能体构成的Lean证明系统，采用隔离上下文、异步搜索、并行策略探测和弹性精化服务，使用现成前沿模型、无需额外训练。作者报告其在PutnamBench上证明669/672题，完成IMO 2026全部六道形式化，并在NTP4VC与VERINA上分别解决597/600和全部189项任务。因基准接近饱和，论文还提出Aegis，将竞赛编程题转为真实实现上的更难验证任务，生成2045个经差分验证的Rust-Lean程序对和11533个候选规约；在2000条分层抽样语句上，EasyProver在每题30分钟预算内证明1054条（52.7%）。
要点速读
- EasyProver用现成前沿模型、无额外训练，报告证明PutnamBench 669/672题并完成IMO 2026全部六道形式化。
- 在NTP4VC解决597/600验证条件、VERINA全部189项任务，方式为证明或反驳。
- 论文提出Aegis，将竞赛编程题转为真实实现上的验证任务，产出2045个Rust-Lean程序对与11533个候选规约；抽样2000条语句中证明1054条（52.7%）。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/11/1 08:00:28（北京时间）。