用AI批量将数学教材转为可验证的机器代码
Formalizing Mathematics at Scale
- 多智能体系统协同处理数学文本形式化
- 建成超4.5万条声明、50万行代码的验证库
- 适合数学研究者与形式化验证从业者
我们提出AutoformBot，一个用于在Lean 4中大规模构建自动化形式化教科书库（Atlas）的多智能体系统。该系统调度数千个大语言模型智能体，配备形式化验证工具、依赖感知任务调度和协作版本控制，将非形式化教材内容转化为机器可验证的定义与证明。我们在26本开放获取教材上应用该方法，覆盖分析、代数、拓扑、组合数学和概率论，生成了包含超过45,000条Lean 4声明和50万行代码的Atlas库。我们发布了两个成果：(i) AutoformBot开源多智能体框架；(ii) Atlas形式化库。结果表明，以经济和技术可行性实现研究生级数学内容的大规模自动形式化已成可能，为人类与机器生成数学的自动化验证开辟新路径。
原文摘要 · Abstract (English)
We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task scheduling, and collaborative version control, to translate informal textbook prose into machine-checked definitions and proofs. We apply our methods to a corpus of 26 open-access textbooks spanning analysis, algebra, topology, combinatorics, and probability, producing Atlas: a verified library of over 45,000 Lean 4 declarations and 500 thousand lines of code. We release two artifacts: (i) AutoformBot, the open-source multi-agent framework; and (ii) Atlas, the resulting formal library. Our results suggest that autoformalizing the core content of graduate-level mathematics at scale is now economically and technically feasible. This opens the door to the automated verification of both human- and machine-generated mathematics at a research level.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。