一道数学题做成了一家公司——洪乐潼访谈Ai潮局

那个不爱创业的数学女孩，把 AI 拉回证明桌

洪乐潼、Axiom，以及 AI for Math 最让人上头的那部分

事情是这样的。

我把这份四个多小时的访谈转写看完，原本以为会看到一个很标准的硅谷天才叙事。年轻、华尔街、数学背景、AI for Math、融资、估值、自己导师名教授加入。你看，这些词放在一起，已经足够写出一篇很热闹的文章。

但真正打动我的，反而不是这些。

是她在访谈里反复说，自己不是天赋型选手。是她说自己是「蛮力型选手」。是她聊融资时那句特别诚实的「没人喜欢融资」。也是她谈 AI 的时候，几乎没有把它讲成一个魔法，而是讲成一个系统，一堆模型，一堆验证，一堆要被补上的 sorry。

这就有意思了。

这篇我想聊三件事。

· 为什么「我不是天才」这句话，反而是这期访谈最好的入口

· 为什么 AI for Math 的关键，不是让模型更会聊天，而是让它能被验证

· 为什么这家公司最危险也最迷人的地方，是它把科学雄心和商业责任绑在了一起

1、最反常识的地方，是她不愿意演天才

很多人物访谈最没劲的地方，是被访者会自动进入一种成功者叙事。小时候如何早慧，后来如何一路开挂，关键节点如何被命运选中。听多了以后，大家都很疲惫。不是故事不好，而是这种叙事太平滑，平滑到不像真的人生。

洪乐潼这期不是。

她讲自己小时候做几何题，做不出那种漂亮的几何直觉，就用复杂的代数方法硬推。她在 MIT 数学系里，看左边右边都是 IMO 金牌和天赋怪，自己的感受是，完了，我可能就是最笨的那个。

说真的，这种坦白很珍贵。

因为它把 AI for Math 这件事从神话里拽了回来。数学不是只有闪电击中的瞬间，很多时候就是一张纸、一支笔、三个月没想出来，六个月没想出来，然后继续想。

这跟今天的 AI 很像。

我们总喜欢把 AI 描述成天才，像它下一秒就会自己悟道。但真正能工作的系统，往往不是一个天才模型在空中飞，而是一群很笨但很执着的过程，一遍遍搜索，一遍遍验证，一遍遍把中间缺掉的步骤补上。

天才当然迷人。

但能把天才的灵光拆成工程过程的人，可能更稀缺。

图一：形式化证明系统工作流 — 每一步都离不开心甘情愿的「sorry」

2、数学不是 AI 的装饰品，是刹车片

过去两年，我们见过太多会说话的 AI。它能把一句需求扩成一页方案，能把一段报错解释得像个资深工程师，能把一个商业点子包装得特别完整。

问题是，很多场景里，像，不够。

你写篇公众号，像就像了。你写一段没上线的脚本，错了还能改。可如果 AI 写的是金融系统、芯片验证、关键软件，甚至科学推理，那一个漂亮但错的答案，就不是小尴尬了。

所以洪乐潼在访谈里讲到一个特别关键的配比——语言负责突破边界，数学负责往回收。

我很喜欢这个说法。

语言模型擅长生成，它会猜，它会联想，它会往外走。Lean 这样的形式化证明语言擅长验证，它不负责哄你开心，只负责问，这一步过不过。这就是两种完全不同的气质。

一个往前冲。

一个把它拽回来。

DeepMind 在 2024 年用 AlphaProof 和 AlphaGeometry 2 做到 IMO 银牌水准，拿到 28 分，离金牌线只差 1 分。这个节点很重要，因为它让很多人第一次意识到，AI 做数学不只是算答案，它可以进入证明这件事。

但奥赛题只是入口。更难的，是研究数学，是没有标准答案的领域，是那些一开始甚至不知道该怎么提问的问题。

这也是 Axiom 的野心所在。

图二：生成负责把世界打开，验证负责把世界关紧

3、Axiom 赌的不是一个模型，是一套工作流

很多朋友看到 Axiom 的融资，第一反应可能是，怎么又一个 AI 独角兽。

公开报道里，Axiom 在 2025 年完成 2 亿美元 A 轮，估值 16 亿美元。数字很大，听起来也很硅谷。

但访谈里真正有料的地方，不是她怎么把估值聊上去，而是她怎么描述这个系统。

她讲到一种很具体的路径，先让 informal 模型给出思路，再把思路变成 formal 的 Lean 结构，然后把中间那些 sorry 一个个填掉。

这个 sorry 特别妙。

在 Lean 里，它大概就是，我这里先欠着，你先假设它是对的。听着很像人类写草稿，对吧。我们写任何复杂东西时，都会先用一个「这里以后再补」把坑占住。

但证明系统很残忍。

你不能永远 sorry。你要把它补上。补不上，这个证明就不能算过。

这就是 AI 工作流很可能要走的方向。不是一个大模型包打一切，而是一个系统里有负责猜的，有负责翻译的，有负责搜索的，有负责验证的，还有一堆便宜但可靠的规则工具，先把能解决的解决掉，剩下的再交给更贵的推理。

这听起来没有一句「AGI 来了」刺激。

但我反而觉得，这才像真的。

4、她最厉害的地方，可能是知道这事会痛苦

这期访谈里，我还有一个很喜欢的点。

她并没有把创业讲成热血爽文。她说融资就是累。你像复读机一样，一次一次讲同样的事情，接同样的问题。她也知道，拿了钱以后，事情并不会变轻松，反而要对员工、投资人、方向、执行速度负责。

这句话听着不燃，但很成年。

AI 创业这几年，大家太容易被漂亮词汇带着走。大模型、Agent、推理、自动化、科学发现，每个词都闪闪发光。但公司不是词汇的集合，公司是很多具体的人每天醒来以后，要在有限时间里做选择。

你看，每一个都不是口号能解决的。

但也正因为这样，我反而更愿意相信这家公司值得被认真看待。一个创始人如果只会把愿景讲得巨大，我会有点紧张。一个创始人能把愿景讲大，也能把里面的痛苦讲清楚，这事就开始有可信度了。

坦率的讲，我不知道 Axiom 最后会走到哪里。

它可能真能把数学验证变成 AI 基础设施的一部分，也可能会卡在产品化、数据、研究问题、商业化之间。洪乐潼自己也说，这家公司可能是很 binary 的 outcome，不是登月成功，就是中途炸掉几次。

但你敢信？？？

在 AI 这么多热闹故事里，我现在反而最想追踪的，是这张证明桌。

如果只看融资，Axiom 是一个很标准的 AI 独角兽故事。

但如果把这期访谈认真听完，它更像另一个问题。

当 AI 终于可以很便宜地生成无数答案，人类接下来最值钱的能力，可能不是继续制造更多答案，而是建立一套判断什么能被相信的系统。

以前我们问 AI，能不能帮我想。

以后我们可能要问，能不能证明你想的是对的。

这才是我觉得 AI for Math 真正让人兴奋的地方。不是机器抢走数学家的浪漫，而是它逼我们重新理解，什么叫严肃地思考。