夜雨聆风当整个AI行业都在追逐更大的模型、更强的生成能力时，一个25岁的年轻创业者，偏偏选择去做了一件最不性感、也最难商业化的事——
用数学验证AI。
她的公司叫Axiom，成立不足两年，员工只有20多人，最近拿下2亿美元A轮融资，投后估值高达16亿美元，折合人民币超过110亿元。
而她本人，17岁考入MIT，三年修完数学和物理双学位，曾获全美女性数学家最高荣誉，是典型的"天才少女"创业者模板。
这个人，叫洪乐潼。
AI最大的软肋：幻觉
要理解洪乐潼在做什么，先要理解AI最大的问题。
今天的AI，尤其是大语言模型，有一个致命缺陷：幻觉。
所谓幻觉，就是AI会把答案说得很像对的，甚至真的做对题，但你没法确认它到底是真正推理出来的，还是只是"猜对了"。
一个例子很能说明问题：
2024年底，ChatGPT o3被曝光在数学测试中可能存在"作弊"嫌疑——它回答的准确率虽然高达96%，但一旦要求展示推理过程，得分率就骤降至5%。
这暴露了大模型的根本问题：推理过程无法被验证。
现有的AI，本质上是概率黑盒。它通过海量数据学习模式，基于统计规律给出答案，但推理过程是黑箱，无法量化，无法证明。
这就是Axiom要解决的问题。
形式化验证：用数学给AI装上"验算纸"
Axiom做的，是"形式化验证"。
原理听起来不复杂：
- 让大模型负责猜想和搜索——它可以大胆假设
- 用一种叫Lean的形式化验证语言，对每一步推理进行数学验证
- 如果Lean检查发现过程不对，就退回去继续改
- 只有每一步都经过数学证明的结论，才被认为是"可靠的"
关键在于Lean这个语言：它是一个可以自验证的数学编程语言。
"如果用英语写出数学证明，我没办法知道5000行的证明是否正确，需要找高水平专家验证。但Lean是自验证的，只要跑通了就是对的。"洪乐潼这样解释。
形式化验证的核心逻辑是：不管答案是什么，只管结论是否从前提一步步合法推导出来。
这就从根本上切断了AI"瞎猜"的路径。
实测：攻克数学难题，碾压顶级竞赛选手
2025年12月，Axiom交出了一份令行业震惊的成绩单：
- 他们的核心系统AxiomProver在无人干预的情况下，攻克了困扰数学界数十年的两道埃尔德什难题
- 同一时间，AxiomProver在美国最负盛名的普特南大学生数学竞赛中斩获满分，12道题全对——过去近百年仅有5个人类选手拿到过满分
这两项成绩，放在任何一个数学研究机构都是重磅成果何况来自一个成立不到两年的20人小团队。
豪华团队：57岁数学泰斗给24岁学生"打工"
Axiom的团队构成，是另一个让人意外的故事。
公司只有20多人，但成员背景堪称豪华：
- 首席科学家François Charton：将Transformer架构引入数学推理领域的先驱
- 第15号员工小野健（Ken Ono）：模形式领域顶尖学者，美国数学学会前副会长，拿过古根海姆奖、斯隆奖等荣誉，曾拒绝Google和Meta的邀请
57岁的小野健为什么要加入一家20多人的初创公司，给一个24岁的年轻人"打工"？
他自己的话是："如果我的猜想能被机器在3天内推广到10个维度，我愿意当一个'标注工'。"
洪乐潼给他的合同条件是：不设教学任务，不设行政工作，100%专注科研。
这对一个热爱数学的学者来说，诱惑太大了。
行业启示：AI可靠性的赛道正在升温
从行业视角看，Axiom的崛起踩中了一个明确的技术趋势：
AI正在从"能用"向"可靠"升级。
2024年底，Meta FAIR和斯坦福大学联合发布了一份立场论文，标题是《Formal Mathematical Reasoning: A New Frontier in AI》。
论文明确提出：过去的AI数学路线走错了——喂很多题、让模型输出答案是远远不够的。下一步要把形式化验证系统真正接入模型，让AI真正理解数学推理过程。
这个判断正在成为行业共识。
据钛媒体等多家媒体追踪，Meta今年已经发布了半形式化推理技术，让大语言模型能够在不执行代码的情况下验证代码补丁，准确率达到93%。
竞品公司方面，Harmonic在2026年1月获得英伟达投资，估值达14.5亿美元；Theorem、Cajal等一批初创公司也在近两年纷纷进入这个赛道。
形式化验证，这个曾经冷门到几乎没有竞争的领域，正在变得拥挤。
商业模式：挑战刚刚开始
然而故事并不只有光鲜的一面。
洪乐潼最初的商业设想是服务对冲基金和量化交易公司，快速解决资产定价和股市预测相关的复杂数学问题。
但这个蓝图至今仍停留在构想阶段。高频交易公司对技术的要求极高、验证周期长，大额商业化订单尚未落地。
2亿美元融资给了Axiom足够的 runway，但商业模式能否跑通，仍然是这个年轻公司面临的最大挑战。
启示
Axiom的故事，对关注AI应用的人有几点重要启示：
1. AI可靠性是下一个大赛道
随着AI在金融、医疗、军工、芯片等高可靠性要求场景加速落地，如何让AI的输出可验证、可追责，将成为刚需。
2. 跨界人才的价值被重新定价
洪乐潼的背景极其特殊：MIT数学+物理双学位、神经科学、斯坦福数学与法律双学科博士——这种跨学科背景在AI与垂直行业结合的当下，比任何时候都更值钱。
3. 技术领先不等于商业成功
Axiom技术很强，但商业化仍在探索。这提醒我们：好技术不等于好产品，更不等于好生意。
AI赛道的机会很多，但选对赛道只是第一步。
我是星禾，我们明天见。
【来源：钛媒体《专治AI说谎，25岁天才少女公司估值过百亿》，2026年4月】
