超越库：用于研究数学自动形式化的智能体框架

针对大语言模型在数学推理中易产生隐蔽错误的问题，本文提出一种基于通用编码大模型的智能体自动形式化框架。该系统核心为编排器，管理面向研究级数学的多智能体流水线。针对现有库（如 Mathlib）未覆盖的概念，系统能动态扩展类型定义，并通过新颖的辅助引理技术进行验证，随后形式化主要定理。实验在 PutnamBench 及五篇 STOC 论文上成功生成并验证了机器可检查的 Lean 证明，部分证明无需额外公理。