Axiom 数学人工智能定理证明器 | AI生成和翻译
Axiom Math (axiommath.ai) 正在构建一个 AI 数学家——一个旨在求解、生成并形式化验证数学证明的系统，而非仅仅输出看似合理的答案。
实际功能
- 接收自然语言数学问题
- 将其转化为形式化证明语言 (Lean)
- 分解为子目标
- 搜索或发明引理
- 生成完全验证的证明
- 转换回人类可读的解释 这意味着每一个推理步骤都经过数学检验，而不仅仅是预测。(Sacra)
该平台也提供工具（如 AXLE），用于：
- 验证证明
- 提取定理
- 变换证明
- 快速实验形式化推理 (axiommath.ai)
与普通大语言模型的不同之处
典型的大语言模型：
- 生成看似合理的数学内容
- 可能产生幻觉
- 无法保证形式正确性
Axiom Math：
- 生成形式化证明
- 使用 Lean 定理证明器
- 验证每一步
- 旨在实现可证明的正确推理 (Sacra)
他们的目标
其长期目标：
- “AI 数学家”
- 自动发现新定理
- 为金融、密码学、软件验证提供推理引擎 (Sacra)
他们还发布了诸如 Axplorer 等工具，旨在发现数学模式并帮助解决复杂问题。(EULAB)
简而言之
Axiom Math = 形式化证明AI + 定理证明器 + 数学发现引擎
并非：
- 仅仅是一个计算器
- 仅仅是一个聊天AI
- 仅仅是符号数学
而是：
- 机器检验推理系统
这更接近：
- Lean 证明器
- Coq
- Isabelle
- DeepMind AlphaProof 的方向
……但同时结合了大语言模型风格的搜索与证明验证。
参考文献：
- https://axiommath.ai
- https://sacra.com/research/axiom-math
- https://eulab.ai/articles/2026-03-25/axiom-math-releases-axplorer-ai-tool-for-mathematicians