我们展示一个案例研究：一个自动化AI系统将一本500多页的研究生水平代数组合学教材形式化到Lean中。所得的形式化代表了教材形式化规模与成熟度上的新里程碑，从早期本科拓扑学的成果以及现有库内容的重构，迈向了对一本研究生教材的完整独立形式化。该形式化包含13万行代码与5900个Lean声明，由总计3万个Claude 4.5 Opus智能体在一周内通过版本控制在共享代码库上并行协作完成，同时创下了多智能体软件工程产出可用成果的纪录。其推理成本与我们估计的人类专家团队所需薪资相当或更低，并且我们预计无需更好的模型仍有大幅提效的潜力。我们将代码、生成的Lean代码库以及一个并排对照的蓝图网站开源发布。
图 5：随着时间的推移，按所花费token的金额（左）和比例（右）划分的代理结果。有关代理结果的分类，请参阅第 3.4 节。该数据是 400 个代理的滚动窗口的平均值，不包括对存储库有微小贡献的短期调试运行。垂直虚线表示干预或重新启动（通常为提高效率和更好的可观察性而进行较小的代码更改）。运行的前几个小时内无法获得详细的令牌统计信息。可以看出，初始代码存在性能问题（尤其是 NFS 瓶颈、git worktree 超时和合并队列拥塞），导致大量令牌花费在中止代理上。后来的版本消除了这些问题，并且主要受到问题依赖性的影响，大量被阻止的代理就证明了这一点。这可以通过状态代理的有针对性的干预来解决，这些干预清理陈旧的问题，分析依赖关系并建议行动方案，从而提高运行最新阶段的成功率。请注意，合并的 PR 也可以专门触及问题文件，特别是在维护代理的情况下，因此应该可以实现接近 100% 的成功率。
