大规模数学形式化

我们提出AutoformBot，一个用于在Lean 4中构建大规模自形式化教科书库（Atlas，Autoformalized Textbook Library At Scale）的多智能体系统。AutoformBot协调数千个配备形式化验证工具的LLM智能体，借助依赖感知的任务调度与协作式版本控制，将非正式的教科书文本翻译为经机器校验的定义与证明。我们将该方法应用于涵盖分析、代数、拓扑、组合与概率的26本开放获取教科书，产出Atlas：一个包含超过45,000个Lean 4声明与50万行代码的经过验证的库。我们发布两个成果物：(i) 开源多智能体框架AutoformBot；(ii) 由此得到的形式化库Atlas。我们的结果表明，大规模自形式化研究生级别数学的核心内容如今在经济与技术上均已可行。这为在研究层面对人类生成与机器生成的数学内容进行自动化验证打开了大门。