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

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

洪乐潼这期不是。

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

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

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

这跟今天的 AI 很像。

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

天才当然迷人。

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

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

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

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

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

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

我很喜欢这个说法。

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

一个往前冲。

一个把它拽回来。

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

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

这也是 Axiom 的野心所在。

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

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

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

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

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

这个 sorry 特别妙。

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

但证明系统很残忍。

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

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

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

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

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

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

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

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

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

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

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

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

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

但你敢信？？？

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