AI用30个代理一周内自动形式化500页高等代数组合学教材，代码量达13万行。
Automatic Textbook Formalization
- 30个AI代理并行协作，通过版本控制在一周内完成教材形式化。
- 产出13万行代码、5900个声明，达到研究生级别教材形式化新高度。
- 成本低于人工团队，开源代码与对照网站，适合形式化研究者参考。
我们展示了一个案例研究：一个自动AI系统将超过500页的研究生级代数组合学教材完整形式化为Lean语言。这一成果标志着教材形式化在规模和熟练度上的新里程碑，从早期本科拓扑学成果到现有库重构，迈向了完整的研究生教材独立形式化。形式化包含13万行代码和5900个Lean声明，由总计3万次Claude 4.5 Opus代理并行协作，通过版本控制在一周内完成，同时创下可交付成果的多智能体软件工程新纪录。推理成本与估算的人类专家薪资相当或更低，且预计无需更优模型即可实现更大效率提升。我们开源了全部代码、生成的Lean代码库及侧边对照网站。
原文摘要 · Abstract (English)
We present a case study where an automatic AI system formalizes a textbook with more than 500 pages of graduate-level algebraic combinatorics to Lean. The resulting formalization represents a new milestone in textbook formalization scale and proficiency, moving from early results in undergraduate topology and restructuring of existing library content to a full standalone formalization of a graduate textbook. The formalization comprises 130K lines of code and 5900 Lean declarations and was conducted within one week by a total of 30K Claude 4.5 Opus agents collaborating in parallel on a shared code base via version control, simultaneously setting a record in multi-agent software engineering with usable results. The inference cost matches or undercuts what we estimate as the salaries required for a team of human experts, and we expect there is still the potential for large efficiencies to be made without the need for better models. We make our code, the resulting Lean code base and a side-by-side blueprint website available open-source.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。