论文精读：不重训模型的两种极致——EASYPROVER 把 Lean 证明基础设施推到基准饱和，TokenEconomizer 把经验复用做成外挂成本控制器
本期精读两篇共享同一哲学的论文：AWS 与 Case Western 的 EASYPROVER 用无训练的递归子代理加弹性 Lean 推理服务，在不做任何微调的前提下拿下 PutnamBench 669/672、VERINA 189/189，并用 AEGIS 管线自动生成 11,533 条带证明或反驳双极标签的可验证任务；UC Berkeley 与 Microsoft Research 的 TokenEconomizer 把已完成轨迹变成资产，作为外挂控制器为 Claude Code、Codex、Copilot CLI 在 30 个仓库设置单元上全部降本 18.4-30.9% 且 Pass@1 四升一平。一个把基础设施规模化推向极限，一个把经验资产化做到通用，两者共同勾勒出 training-free 工程路线的完整光谱。