# AxiomMath 希望用形式化验证阻止 AI 劣质内容进入数学领域

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

- 来源：TechCrunch · AI
- 发布时间：2026-11-05T16:16:45.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/lklp17ehbasw7t4y1n3a5hhjr
- 原文：https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/

## 摘要

AxiomMath 周三宣布已对 Stacks Project 完成形式化验证，希望为 AI 智能体提供可靠的数学基础。其智能体将约 7,654 页数学内容转为约 16 million 行由计算机检查的 Lean 代码，并保留定理与定义之间的依赖关系。公司称，这些已验证结果可供后续数学证明复用，并希望将这一方法扩展到软件开发和科学研究。