摘要：2025年，AI初创公司Axiom Math完成6400万美元种子轮融资，估值达3亿美元。该公司由24岁的Carina Hong创立，致力于开发能够自主验证逻辑正确性的“AI数学家”。其核心创新在于使用Lean编程语言确保AI推理过程的每一步都可追溯和检查，以解决AI结果难以验收的信任难题。团队在2025年的Putnam数学竞赛中，其系统自主解决了12道题中的9道并完成了形式化验证。公司汇聚了来自Meta、Google的前核心研究员及知名数学家，共17人。其愿景是推动AI从生成答案转向提供可验证的严密证明，成为科研与工业领域可信赖的合作者。
线索：
* 投资机会：Axiom Math瞄准了当前AI落地中的核心瓶颈——结果的可信度与可验证性。其“可验收”的技术路径（基于形式化验证）在数学、芯片设计、科学发现、金融系统等对正确性要求极高的领域具有明确且广阔的应用前景。顶尖的跨界团队（AI研究员+数学家）构成了强大的技术壁垒。如果其技术范式获得成功，可能为AI在关键领域的深度应用设立新标准。
* 潜在风险：该技术路线高度专业化，依赖于Lean等小众形式化语言，技术难度与工程化挑战极大。将数学证明的严谨性推广到更普遍、更复杂的现实问题中存在不确定性。作为早期初创公司，其商业模式和产品化路径尚待验证，面临来自其他AI研究机构及科技巨头的竞争。高昂的估值也意味着市场对其未来成长性有极高预期。
正文：
2025年，人工智能领域广泛关注AI模型的能力边界，但企业应用面临一个关键障碍：如何证明AI产生的结果是正确的？许多AI产品在演示中表现良好，但在实际部署中可能出现难以定位的错误、无法厘清的责任以及不可复现的结果，导致最终无法通过验收。
总部位于旧金山的AI初创公司Axiom Math提出了不同的解决方案：其重点不在于追求AI能做什么，而在于证明它做对了什么。该公司由24岁的Carina Hong创立，并在2025年10月完成了6400万美元的种子轮融资，由B Capital领投，估值达到3亿美元。该公司的目标是开发一个能够独立给出答案并自行验证对错的“AI数学家”。
Carina Hong出生于广州，拥有麻省理工学院、牛津大学（罗德学者）和斯坦福大学的学术背景，在斯坦福攻读数学与法学联合博士学位期间退学创业。她认为，让AI理解并验证数学，是解决AI可信度问题的关键途径。
Axiom Math的技术核心是使用名为Lean的数学编程语言。与常见的大语言模型不同，该系统要求所有的公式、步骤和证明都必须像程序一样被清晰书写，并且每一步都能被机器验证。这意味着AI的推理过程必须留下可检查的痕迹，最终像软件通过测试一样完成“验收”。
为验证该方法，Axiom Math的系统“AxiomProver”参与了2025年美国Putnam大学生数学竞赛。该竞赛约有4000名参赛者，题目难度极高。AxiomProver自主解决了12道题目中的9道，并在Lean语言中给出了完整的形式化证明，且全部通过了自动验证。此举不仅展示了解题能力，更证明了AI具备自主检查并确认结果正确性的能力。
该公司团队规模为17人，但成员背景深厚。首席技术官Shubho Sengupta曾任Meta FAIR团队核心研究员，参与过OpenGo、CrypTen等项目及早期CUDA架构工作。核心研究员François Charton早在2019年便开始研究使用Transformer解决数学问题。另一位成员Hugh Leather专注于深度学习与编译器的结合。此外，57岁的知名数学家Ken Ono（Carina Hong在MIT时期的导师，拉马努金理论专家）已于2025年12月初辞去弗吉尼亚大学终身教职，全职加入Axiom Math，担任创始数学家，负责设计难题以测试模型推理的极限。
Axiom Math的愿景分为多个阶段：首先是用形式语言表达定理并模仿逻辑结构；其次是验证旧问题的不同解法并提出新的证明路径；最终目标是提出新的数学猜想。该公司目前正在研究著名的未解难题“Collatz猜想”。其Transformer模型虽未直接证明该猜想，但在预测涉及万亿级数字的Collatz序列时达到了99.8%的准确率，且产生的错误具有可解释的规律，而非随机幻觉。这表明AI正在学习数学思维，而非单纯记忆答案。
创始人Carina Hong认为，数学是人类最严密的语言，也是诸多科技领域的底层逻辑。一旦AI能够进行可验证的数学推理，它将能从“只能试试看”的辅助工具，转变为在密码学、芯片设计、物理建模、金融系统及法律等容错率低的领域中“可以放心用”的可靠合作者。她将“可验收”视为AI真正实现广泛应用的下一个及格线，其核心是可信度而非单纯的能力扩展。
发布时间：2025年12月26日08:52
评论 ( 0 )