Axiom Math 希望将 AI 垃圾挡在数学之外

英文原标题：Axiom Math wants to keep AI slop out of mathematics

本文为英文原文的机器翻译摘要，原文见：TechCrunch AI ↗

• AxiomMath 宣布已对 Stacks Project 完成形式化验证，这是人类编写的最大数学文献之一，包含约 7,654 页内容。
• 该公司利用 AI 代理将 Stacks 翻译成约 1600 万行 Lean 代码，并通过证明助手逐行检查，确保逻辑严密。
• Stacks 的定理和定义相互关联，Axiom 团队为代理设定松散层级，让它们并行工作并自主寻找任务，同时训练自有模型掌握数学品味。
• 此举填补了代数几何领域形式化数学的空白，此前研究者用 Lean 检查新工作时缺乏基础。
• Axiom 认为数学是构建可验证基础的起点，未来 AI 代理编写软件也需要类似的可复用知识库，以避免产生低质量内容。

关键数据

• OpenAI 上月发布了 719 份手稿，声称解决了某些最难的数学问题。
• AxiomMath 估值 16 亿美元，于 2025 年 3 月由 25 岁的 CEO Carina Hong 创立，同年 3 月完成由 Menlo Ventures 领投的 2 亿美元 A 轮融资。
• Stacks Project 由哥伦比亚大学的 Johan de Jong 于 2005 年启动，内容涵盖从大学代数到代数、几何和数论的前沿成果。
• Axiom 将 Stacks 的约 7,654 页内容转化为约 1600 万行计算机可检查的 Lean 代码。

引语

• “生活中，大的东西和精致的东西就是无法共存。”
• “我们不确定 vibe coding 能否保留 Stacks 的美感。”
• “你看数学中已经形式化的部分，有一个巨大的黑洞。这个黑洞覆盖了代数几何。”
• “形式化的证明越多，你能制造的形式化证明就越多。”
• “我公开挑战所有编程公司，在这个规模上做形式化。”

为什么值得看：AxiomMath 通过大规模形式化验证 Stacks Project，为 AI 代理提供了可依赖的数学基础，可能影响未来软件和科学研究的可靠性。