突破数学图书馆：智能体框架实现研究数学自动形式化

尽管大语言模型在数学推理方面展现出卓越能力，但常产生难以察觉的细微错误。形式化数学语言如Lean 4提供了机械化证明检查功能，这推动了自动形式化技术的发展——即将自然语言数学自动转换为可验证代码。最新趋势表明，针对通用编程优化的主流大模型在Lean任务上已超越专门微调的小型模型。基于这一转变，研究团队推出了由通用编码大模型驱动的智能体自动形式化框架。该系统的核心是一个协调器，负责管理专为研究级数学设计的多智能体流程。由于前沿研究常涉及Mathlib等现有库未涵盖的概念，该系统能动态扩展必要的类型定义，并通过创新的辅助引理技术在形式化主要定理前进行验证。团队在PutnamBench上测试了该方法，为32个随机问题生成了机器可检查的Lean证明。此外，系统在ACM计算理论研讨会（STOC）的五篇论文中进行了评估，涵盖组合数学、通信复杂度、机制设计和学习理论等领域，成功形式化了其主要定理，并由人类专家验证了生成的形式化结果。值得注意的是，其中两篇论文的证明仅依赖Lean内核公理。所有形式化成果已在项目网站公开。