Axiom Math 希望将 AI 劣质内容排除在数学之外

Axiom Math 周三宣布正式验证 Stacks Project，其 AI 代理将约7654页数学译为约1600万行 Lean 代码。该验证填补代数几何形式化空白，为 AI 代理提供可复用的可靠数学基座。公司由 Carina Hong 于2025年3月创立，曾获 Menlo Ventures 领投2亿美元 A 轮融资。