Avigad、Buzzard、Commelin 等提出“形式化全部数学”的质量路线：可复用库优先于一次性 AI 代码堆积

Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash 与 Adam Topaz 于 10 月 16 日发表共同文章，回应 AI 快速 autoformalization 后“尽快形式化全部数学”的呼声。作者支持大规模形式化目标，但强调形式 artifact 的价值不仅是 correctness，还在于能否被数学家理解、维护、重构和继续用于新研究；以 AI sphere-packing code、Anthropic 1300 万行 FLT formalization 和 OpenAI 数学发布为案例，警告低质量一次性代码可能浪费资源并破坏社区激励。文章提出以 Mathlib、Formal Conjectures、AnnalsChallenge、Tau Ceti、Formal Frontier 与 Palomar 等互补机制为基础，由数学家控制 roadmaps、library design、hosting 与治理。