Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

这项工作把自然语言数学研究转成 Lean 4 形式化证明，重点不在刷现有 Mathlib 覆盖的题，而是处理研究论文中超出现有库的概念。系统用 orchestrator 管理多代理流水线，必要时动态扩展类型定义，并通过 Auxiliary Lemma 技术验证这些扩展后再形式化主定理。实验包括 PutnamBench 32 个随机样本和 5 篇 STOC 论文，覆盖组合、通信复杂性、机制设计和学习理论；其中所有五篇都形式化了主定理和证明，两篇不依赖 Lean kernel 之外公理，给 research-level autoformalization 提供了更具体的可行性证据。