初创人工智能公司 Axiom Math 宣布，其自主智能体系统已成功对“Stacks Project”的全部内容完成了正式且程序化的验证（Formal Verification），该项目被认为是历史上由数学家编写的最庞大的开源数学参考资料之一。
将数学知识转化为可审计的代码
Stacks Project 由哥伦比亚大学数学教授 Johan de Jong 于 2005 年发起，包含约 7,654 页内容，涵盖了从代数和代数几何原理到数论高级理论的广泛领域。Axiom Math 的智能体集群已成功将这些复杂且相互关联的文本转化为约 1,600 万行 Lean 代码。Lean 是一种专门的编程语言，允许审计软件逐行审查每个数学证明，以确保其严密的逻辑完整性。
该公司在由 Menlo Ventures 领投的首轮融资中筹集了 2 亿美元，目前市值达 16 亿美元。其目标是构建一个可靠且经过程序化验证的知识库，供未来的人工智能系统在软件开发和科学研究中使用，从而避免产生被称为“AI 垃圾”（AI slop）的误导性或不准确的结论。
智能体的程序化工作机制与结构关联挑战
25 岁的公司创始人兼首席执行官 Carina Hong 为了在 2025 年 3 月创立 Axiom 而退出了斯坦福大学的数学博士项目。她解释说，最大的挑战在于保持数千个定理之间的关联性，并避免任何概念上的矛盾。公司技术团队成员 Ashvin Swaminathan 指出，AI 智能体并非在每一步都接受直接指令，而是被赋予了一种灵活的层级结构，使其能够并行分配任务，并利用经过正确数学思维训练的专用模型，而非依赖通用的代码生成模型。
这一成就对科技领域意味着什么？
这一进展是填补计算机数学证明领域重大空白（特别是在代数几何等领域）的务实举措。形式化验证的益处不仅限于学术界；通过计算机代码记录证明可以提供一个可重用的基础环境。该公司押注于，开发者和敏感软件的开发者（如芯片设计和关键系统计算）将需要这些经过验证的规则，以防止因日益依赖智能体编写软件而导致的安全性漏洞和隐蔽错误。