Axiom Math 希望将 AI 垃圾挡在数学之外
内容摘要
估值 16 亿美元的初创公司 Axiom Math 已对 Stacks 项目——人类编写的最大的数学文库之一——进行了形式化验证，利用 AI 代理将其 7,654 页内容翻译成约 1600 万行计算机可检查的 Lean 代码。形式化验证类似于芯片设计和软件调试中使用的方法，通过证明助手逐行检查代码来确保逻辑严谨性。Stacks 项目由 Johan de Jong 于 2005 年发起，涵盖代数、几何和数论，其相互关联的定理对 Axiom 的代理构成了重大挑战，这些代理在宽松的层级结构下并行工作，并被训练出数学品味。这一成果填补了形式化代数几何的重大空白，为未来证明和 AI 生成的软件提供了可复用的验证基础，通过让代理在可信数学基础上构建而非从头开始，解决了对“AI 垃圾”的担忧。
(来源：TechCrunch)