把分数从模型身上挪到编排上
arXiv 2610.38174 给出的 EasyProver，是一套 Lean 证明系统。四个部件是：隔离上下文的递归智能体、异步搜索、并行 tactic 探测，以及可伸缩的 elaboration 服务。论文反复强调的一点是不动底座——用的是一台现成的前沿模型，没有额外训练，也没有点名具体型号。
结果是四组接近满格的数字：PutnamBench 解出 669 比 672，IMO 2026 的六道形式化题全部通过，NTP4VC 的验证条件解决 597 比 600，VERINA 的 189 个任务以证明或反驳的方式全部了结。九位作者来自 AWS 与凯斯西储大学等机构。
题快考满了，那就自己造题
作者自己也承认这批基准接近饱和，于是顺手做了另一件事：Aegis。它把竞赛编程题转成针对真实实现的更难验证任务——先写出安全的 Rust 解法，用 Aeneas 翻译成 Lean，再生成规约，最后给每条冻结的陈述打上内核检查过的证明或反驳标签。
产出是 2045 对经过差分验证的 Rust 与 Lean 程序对，以及 11533 条候选规约。这批题与手写基准的差别在于实现级义务：定宽算术、显式失败、生成的循环、类型转换、函数化的可变性。这些恰好是真实代码里容易出错、而竞赛题里几乎不出现的部分。
在分层抽样的 2000 条陈述上，每条给 30 分钟预算，EasyProver 证出 1054 条，占 52.7%。从 99.6% 到 52.7%，落差本身就说明这批新题确实更硬。论文也说，同一批题既能当其他证明器的基准，也能当强化学习的奖励信号。
证明通过了，不等于题意写对了
冷水要说足。其一，「证明通过」的前提是「形式化写对了题意」，而自动形式化这一步的语义落差并没有被这套系统消除；内核检查能证明 Lean 陈述与证明自洽，不能证明这条陈述忠实表达了原始问题。其二，论文只说用了现成前沿模型，未点名型号，也未披露单次证明的词元或算力开销；按每条 30 分钟、数千条的规模推算，成本并不低，这部分目前官方及行业暂未披露更多细节。
其三，52.7% 的分母来自作者自建的 Aegis，与其他证明器在旧基准上的数字不可比，也不该当成同一条曲线的延续。其四，基准同时被定位成强化学习的奖励信号，这个双重身份在解读结果时要记着：一套既当考题又当训练信号的题，长期会怎样被过拟合，是这类工作绕不开的问题。
本站此前记录过 Lean 内核之夏的工作：那次审查发现内核存在可靠性漏洞，并提醒自动形式化的信任账要一层一层算。EasyProver 的所有结果都建立在内核检查之上，那一层的可信度因此是这份成绩单的共同前提，而不是可以由它自己证明的部分。
对工程团队的含义相对直接：如果正在评估「用形式化验证兜住真实代码」这条路，现在有了公开的量化锚点——竞赛题几乎被清空，落到真实实现上还有接近一半证不出来。真正的差距不在模型会不会证明，而在规约与实现之间那一段。