AI 初创公司 Axiom Math 提交的 8 篇数学论文中有 5 篇被学术期刊接收，其 AI 系统 AxiomProver 能生成形式化证明，创始人洪乐潼已为公司融资 2 亿美元。
📝 详细摘要
本文报道了 AI 数学初创公司 Axiom Math 的最新进展。该公司由 2001 年出生的 MIT 天才洪乐潼创立，其 AI 系统 AxiomProver 能够将自然语言数学问题转化为 Lean 形式化证明，并通过独立检测器验证每一步。从 2026 年 2 月开始提交的 8 篇论文中，已有 5 篇通过同行评审登上学术期刊，横跨数论、组合、代数几何等多个领域。Axiom 在 3 月完成 2 亿美元融资，估值达 16 亿美元。文章还介绍了洪乐潼的成长经历——14 岁立志 MIT，三年完成数学物理双学位，从斯坦福退学创业，以及团队中知名数学家 Ken Ono 的加入。AxiomProver 曾在普特南数学竞赛中拿下满分，并解决了两个 Erdős 猜想。公司的长期愿景是打造能够自我改进的超级智能推理器，其技术路线可能扩展到其他学科和高风险决策场景。
💡 主要观点
- Axiom Math 的 AI 系统 AxiomProver 能生成可验证的形式化数学证明。 系统将自然语言问题翻译成 Lean 形式化证明，再由独立检测器验证每一步，解决了传统大模型自然语言证明可能存在的逻辑缝隙问题。
💬 文章金句
- AI 将编写所有代码，但数学将证明其是否有效。
- 创业者要选最难的问题，甚至需要 5 到 10 年才能解决的那种。
- AI 没有代替人类，而是实践了一种新的人机协作模式。AI 负责生成或形式化可检查证明，人类数学家负责问题表达、论文解释和审稿沟通。
📊 文章信息
AI 初评：86
来源：量子位
作者：梦晨
分类：人工智能
语言：中文
阅读时间：7 分钟
字数：1606
标签： Axiom Math, AI 数学证明, 形式化验证, 洪乐潼, Lean