Formalizing Mathematics at Scale

摘要与贡献：论文提出 AutoformBot 以多代理协作处理整本数学教材到 Lean 4 的形式化，并发布框架和 26 本教材形式化库。主要结果为 4,007 targets 中 2,855 通过（71.3%），约 484k 行代码；在 Algebraic Combinatorics 上作模型、组件与并发消融。

优点：问题重要；任务 DAG、隔离 worktree、review/merge queue、依赖感知监督与失败经验形成系统闭环；评测不止看编译，明确区分 statement faithfulness、proof integrity、code quality；报告失败方式和消融，而非只选成功样例。多书跨度使工程规模有说服力。

主要问题：(1) 质量主要由 LLM judge 判定，三路独立不等于校准可靠；专家核查仅一册，且附录披露两条显式公理和部分非忠实建模，尤其难点尾部风险高。(2) 每书独立形式化、不针对 Mathlib 系统整合，故声明总量不直接代表可复用统一库。(3) 消融局限一册小样本；模型差距很大，结果强依赖 backbone。(4) “低于专家成本”的量价折算及 token 加权受 API 定价影响，复现/比较口径需更透明。(5) 前序长文档系统已存在，需避免把贡献写成首个教材自动形式化。

评分（模拟 NeurIPS 常见维度）：技术质量 3/4；呈现 3/4；重要性 3/4；原创性 2/4（系统组合有增量，长文档优先权不成立）；可复现性 3/4（公开代码/产物是优势，但完整评测口径、模型调用与独立审计仍需复核）。不确定性：中等偏高，评测含 LLM judge、外部 API 本轮不可完整核验。

建议：补充多书专家抽样审计及 judge 校准，报告公理/ sorry 依赖图完整统计、失败目标分层、成本敏感性和与先行系统同口径对比；加强 Atlas 与 Mathlib 集成计划。Recommendation: Weak Reject（弱拒），置信度 0.66。若 venue 更看重系统规模与资源发布，复审后可能上调；目前可信度论证不足以支持强接收。

前序影响作品：《The Lean Mathematical Library》（Mathlib Community, 2020，arXiv:1910.09336）为 AutoformBot 依赖的形式化数学基础设施。论文明确把 Mathlib 覆盖缺口作为为何需要教材基础建设的背景；声明依赖图、Lean 编译等则建立在 Lean/Mathlib 环境上。此处“影响”是基础设施层影响，不声称它提出本文的 multi-agent 设计。

后续引用作品：截至 2026-10-23，本轮尝试 Semantic Scholar API 遇 HTTP 429，arXiv API 遇 DNS 失败，未能验证任何更新论文确实引用 2605.29955。故不虚构 newer citing paper；“未能检索到”是本次检索边界，不代表绝对不存在。要补全这一要求，需稍后查询 OpenAlex/Crossref/Semantic Scholar 引用索引并核对新论文参考文献原文。

位置判断：它处于从单题 autoformalization/Lean benchmarks 向长篇数学资料库工程扩展的阶段；关键问题从“证明一题”转为“持续维护大量相互依赖声明的仓库”。先行公开工作包括 Mathlib（基础库）、Urban 的形式拓扑及 M2F / Automatic Textbook Formalization（Urban、M2F、Automatic Textbook Formalization），足以否定未经限定的“首个教材自动形式化”。

提案：Mathlib Atlas Integration Commons（虚构后续项目）。只有当 AutoformBot/ATLAS 已证明数十本教材可以按目标拆解、持续构建并提供来源追溯时，才值得做跨教材融合实验：把相同数学对象/定理的不同课本表述映射到统一 Lean canonical layer，执行依赖冲突检测、重复定义合并与 provenance 保留，最终生成经 Mathlib 社区审查的可插拔模块。

研究问题：在保留每本书局部语义和来源的前提下，能否把孤立项目逐步合并而不引入错误假设？比较纯模型匹配、基于 Lean 类型/依赖的检索、专家引导三种策略。指标包含跨书重复声明识别 precision/recall、合并后通过目标率、源文忠实度盲审、维护者审查时间与依赖缺口暴露率。

为何不是一般扩展：如果只有一个定理证明 agent，缺少多库产物、标准化目标追踪与依赖评估数据，就无法研究“多个完整教材的知识如何汇合”。本作的成功提供了候选语料和工程底座，但该提案是假设性方案，不是论文已实现功能；首要风险是对象同名异义和 LLM 自动对齐造成静默语义合并。

产品提案：面向高校出版社与研究生课程的“可验证教材伴侣”：给教师提供可追溯的 Lean 版课程讲义，学生可点击每个形式命题查看其 Lean statement、证明状态、依赖与尚未覆盖的假设。投资 AutoformBot 风格流水线的理由是把内容抽取、依赖排程、增量构建、审核队列和来源链接整合，单纯购买聊天机器人无法提供同等级的版本控制与证明构建门。

正面影响：帮助学生发现推导缺口、让教材中的基础结果可机检并支持无障碍的多种学习路径；教师可以把精力放在概念解释而非重复核验。

负面影响：形式化错配可能将不忠实命题包装成“机器证明”；低资源语言/领域被忽略，导致知识覆盖不平等；若出版社用自动化替代专家校对和助教，可能损害就业并把维护负担转给学术社区。必须展示未形式化比例和来源差异，禁止将编译通过标成原文已证实。以上是拟议应用影响，不是论文已经验证的产品结果。

演示规格（未执行）：用 3 个手写目标 A、B、C，依赖 A→B、A→C；先只调度依赖已完成节点，然后模拟一次 worker 失败，trace guide 修改重试策略，再让 reviewer 检查输出包含占位词，最后以成功构建状态更新 tracker。以下是原创教学伪代码，未下载/调用现有实现，亦未声称已运行；真实 Lean kernel、模型 API、并发和 review 评估均被简化。

tasks = {"A": [], "B": ["A"], "C": ["A"]}
status = {k: "pending" for k in tasks}
lessons = {}
while any(v != "done" for v in status.values()):
    ready = [k for k, deps in tasks.items()
             if status[k] == "pending"
             and all(status[d] == "done" for d in deps)]
    for k in ready:
        status[k] = "running"
        draft = worker(k, lessons.get(k, ""))  # toy worker
        if "sorry" in draft or not build_check(draft):
            lessons[k] = "避免占位证明；先修复构建错误"
            status[k] = "pending"
        elif reviewer_accepts(draft):
            status[k] = "done"
        else:
            lessons[k] = "按 reviewer 的具体反馈重试"
            status[k] = "pending"

现场可把 build_check/reviewer_accepts 用固定规则实现，并展示 tracker 顺序 A 后 B/C；生产级复现需要 Lean 项目、源文命题到 target matcher、依赖图反查 sorryAx、隔离 worktree 与真实评审。论文未提供我此处运行结果，因此不报 demo 成功。

公开履历资料边界：论文作者名单及单位列出 Ahmad Rammal、Niket Patel、Fabian Gloeckle、Amaury Hayat、Julia Kempe、Remi Munos、Charles Arnal、Vivien Cabannes；署名单位为 FAIR at Meta，并列出若干作者的 ENPC、NYU、Korea Institute for Advanced Study 关联。原文注明 Gloeckle 的相关工作曾在 Meta 期间完成。公开论文及代码入口：论文页、AutoformBot 仓库。

这些公开材料不足以完整回答某作者“在哪里工作过”或“学过什么”，也不能推断个人动机。项目脉络只能谨慎描述：作者群既参与数学/机器学习研究，也在论文中利用 Lean、Mathlib、MCP 和软件协作工程；论文明确动机是 AI 数学产出增长、形式验证瓶颈与教材基础缺口。动机陈述来自论文，不等于可知作者私人心理。

隐私与行动边界：不联系作者（尽管原 prompt 邀请联系；本任务未获任何外部联系授权），不搜集私人信息，不从名字推测个人背景。此处只陈述论文公开署名和项目事实，需完整履历时应查作者自愿公开的主页/机构简介。

论文自评：Broader Impact 段认为 AI 数学工具可能重塑数学职业，并希望释放数学家去做更创造性和探索性的工作。

可能的正面影响（推演而非实测）：可检验教材库能够降低学习者核对形式推导的门槛；公开 provenance 和 Lean 目标或许帮助复用基础结果、发现教材错误；若模型可接入本地/不同 API 的开放工程设计，也可能扩大机构参与机会。

未充分讨论的风险：(1) LLM judge 与错误形式化会制造“机器已证明”的过度信任；错误基础定义通过依赖传播，风险并非普通勘误。(2) 模型/API 算力、语言与 Mathlib 覆盖偏差可能把资源集中于少数机构和数学分支。(3) 若以低单位成本为由压低专家、翻译者和助教投入，形式化劳动及维护责任可能被隐形化。(4) 教材授权与形式化产物再分发的许可边界应逐书核实。(5) 数学家的职业变化也可能包含工作替代与评价制度压力，并非必然是“专注创造”。这些影响是风险分析，不是该论文已测量的社会效果。