AxiomMath完成StacksProject形式化验证，为AI数学证明构建可信基座

2026年11月5日，成立不久的AI数学初创公司Axiom Math宣布完成一项关键里程碑：对数学界最具影响力的开源项目之一——Stacks Project实现全面形式化验证。这项工作将该项目约7,654页的数学内容翻译为约1600万行Lean语言代码，并通过证明助手逐行校验，确保其逻辑无误。在AI频繁产出数学论文却屡现错误的当下，这一进展被视为构建可信AI数学基础设施的重要一步。

Stacks Project由哥伦比亚大学数学家Johan de Jong于2005年发起，是一个持续更新的在线数学参考库，涵盖从本科代数到现代代数几何、数论等前沿领域的系统性结果。因其严谨性与完整性，被多位学者誉为“当代 Bourbaki”——后者是20世纪中叶由法国数学家群体发起、旨在重建数学基础的标志性工程。哥伦比亚大学教授Peter Woit曾评价：“Stacks Project在规模与深度上几乎没有可比对象。”

形式化验证并非新鲜概念，但其在数学中的大规模应用仍属罕见。该过程要求将传统手写证明转换为特定编程语言（如Lean）的代码，再由“证明助手”自动检查每一步推导是否符合逻辑公理。若通过验证，即意味着该定理在给定公理体系下必然成立。这一方法已在芯片设计、航空航天软件等领域用于保障关键系统安全，例如法国研究团队曾借此发现社保福利计算系统的隐藏漏洞。

Axiom Math 的目标远不止于存档现有知识。该公司由前DeepMind研究员领衔，融资达16亿美元,致力于打造一个“经验证的数学基础层”，供AI代理调用以生成可靠软件乃至科学模型。其核心理念是：面对OpenAI等机构短期内批量发布数百份数学预印本（如2026年10月6日单日发布722份，涉及372个问题），数学界亟需一套能抵御“AI slop”（AI粗制滥造内容）的防御机制。

事实上，2026年已成为AI冲击数学界的转折之年。除OpenAI密集发布成果外，多起标志性事件引发震动：7月19日，雅可比猜想反例被AI找到；9月9日，OpenAI宣称解决了千禧年难题之一——纳维-斯托克斯方程的存在性与光滑性问题（后因争议未被广泛接受）。尽管部分成果被撤回或质疑，但AI在反例构造、符号计算与模式识别上的能力已显著超越人类个体研究者效率。

北京大学博雅特聘教授董彬指出，过去十年数学发展相对迟滞，学科壁垒日益森严，而AI正打破这种封闭结构。“数学家穷尽一生可能只钻研某一类方程的特定解法，工具库极其有限；AI则能跨领域调用方法，加速工具迭代与建模突破。”他主张数学应“走出数学”，向科学与工程延伸，发挥底层支撑价值。

然而，信任危机随之而来。菲尔兹奖得主陶哲轩在10月UCLA举办的Science x AI Summit上发出警告：人类正将思考过程外包给AI，却逐渐丧失对解决方案的理解能力。他在《自然》杂志撰文强调，问题不在于AI能否给出正确答案，而在于人类是否保有检验、判断与理解答案的能力。尤其当AI介入电网调度、药物研发或芯片设计等现实系统时，表面正确的数学解可能因忽略物理约束而引发严重后果。

Axiom Math的路径正是对此回应：不拒绝AI参与数学创造，而是为其铺设一条“可验证”的轨道。通过将Stacks Project这样的权威知识库形式化，AI代理在推理时可直接调用已被证明无误的引理与定理，避免从零构建易错链条。这类似于为AI提供一套“经过ISO认证的数学零件库”，而非任其自由拼装未经检验的模块。

值得注意的是，形式化本身亦非万能。Stacks Project内部定理高度互联，验证不仅需确认单个命题，还需保证定义、引理与定理之间的依赖关系一致。Axiom Math团队动用数十名数学家与工程师协同工作，耗时数月才完成全部转化。即便如此，仍有部分高阶内容因Lean语言表达能力限制暂未覆盖。

当前，数学界对AI态度呈光谱分布：保守派坚持手写证明为核心；中间派接受AI辅助文献检索与计算；激进派如董彬，则主张将繁复推演交由AI，人类聚焦问题选择与方向把控。Axiom Math显然站在第三阵营，其愿景是让AI成为“数学的协作者”，而非替代者。

技术层面，Lean作为主流形式化工具，近年因Microsoft研究院与剑桥大学推动而迅速普及。2025年，Lean 4版本增强对代数几何的支持，为Stacks Project的转化扫清障碍。与此同时，Meta、Google DeepMind等机构也在开发新型证明语言与自动化策略，试图提升形式化效率。

从更广视角看，Axiom Math的实践揭示了一个深层趋势：当AI能力逼近甚至超越人类在特定任务上的表现时，关键竞争点已转向“可信度基建”。正如操作系统需要内核级安全模块，AI驱动的科学探索也需要一层经数学严格验证的“逻辑地基”。Stacks Project的验证完成，标志着这一地基的第一块大型基石已然落位。

未来挑战依然明确：如何扩展形式化范围至更动态的数学分支？如何平衡验证成本与实用性？如何让数学家愿意投入时间参与形式化工作？这些问题的答案，或将决定AI能否真正融入数学创造的核心流程，而非止步于外围辅助角色。

目前，Axiom Math已开放部分验证代码供学术界使用，并计划逐步纳入其他经典文献，如EGA（Éléments de Géométrie Algébrique）与SGA（Séminaire de Géométrie Algébrique）。其最终目标，是构建一个全球共享、持续增长的“形式化数学宇宙”，使任何AI系统都能从中安全调用经过千锤百炼的数学真理。