Maestro 给 Lean 证明装上全局协调者，研究级定理比裸 agent 多证 63%

Maestro（UIUC 与 AWS AI Labs，arXiv 2610.25920）把 Lean 证明的失败处理从固定分解升级为全局协调者调度：worker 证不动时必须提交诊断，协调者可改写蓝图、删伪命题、弃路线，研究级定理集上比裸 agent 平均多证 63%（54 条对 33 条）。