Axiom Math 完成 Stacks Project 形式化验证，用 AI 智能体防止数学领域出现 AI 垃圾

Axiom Math 宣布已对 Stacks Project 完成形式化验证，其 AI 智能体将该数学库约 7,654 页内容转换为约 1,600 万行 Lean 代码。这家估值 16 亿美元的初创公司希望为 AI 智能体提供经过验证的数学基础，未来可用于编写软件乃至开展科学研究。CEO Carina Hong 称，智能体在并行工作中自主寻找任务，公司还专门训练了擅长数学的自有模型。