Maestro 论文：为 Lean 证明装上全局协调者

UIUC 与 AWS AI Labs 等团队发布论文（arXiv 2610.25920），提出 Lean 定理证明的多 agent 框架 Maestro：把失败处理从固定分解升级为由全局协调者统一调度，在研究级定理集上比裸 agent 平均多证 63%（54 条对 33 条）。 机制上，worker 证不动某一步时必须提交“为什么失败”的诊断；能看到整张证明蓝图的协调者据此决定是重试、补引理、改写或删除伪命题，还是整条路线弃掉重换。 论文称 Maestro 全程开源、探索过程可审计，但 HTML 版暂未给出代码仓库的直接链接。

AI 根据报道生成 · 2 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。