一个 Putnam 满分，是几千行 Lean 代码硬枚举出来的——洪乐潼自己讲得很清楚：那不是创造力，是"大力出奇迹"。AI 数学的硬骨头不在奥赛跑分，在另外三件事上。

今年春天有条新闻在数学圈流传：58 岁的美国数论学家 Ken Ono（小野肯）从终身教职上离开，加入一个 24 岁华人女孩的公司。这个女孩叫洪乐潼，Axiom 创始人和 CEO，00 后，MIT 数学本科。Axiom 刚完成 A 轮融资，估值 16 亿美元。

张小珺在硅谷的 Facebook House 采访她，谈了 4 小时 24 分钟。

这一期值得拎出来的判断只有一条：当所有人都在讲"AI 数学竞赛刷分了，AI 终于会做数学了"——洪乐潼这期讲的恰恰是相反的事：会解题，不等于会做数学。

Putnam 满分是真的，但她自己用了一个词来形容自己的 AI——"大力出奇迹"。在她的图谱里，AI 数学的真正战场不在奥数跑分，在另外三件事上：形式化证明（Lean）、auto-formalization（把人类数学翻译成 Lean）、conjecturer（提出有意义的猜想）。这三件事，今天的 AI 几乎没有真正触碰。

她不喜欢这个叙事

AI 数学能力的主流叙事大约是这样的：OpenAI o1 解奥数、Claude 在数学 benchmark 上刷出高分、DeepMind 拿了 IMO 银牌——所以 AI 已经会做数学了。

洪乐潼对这套叙事保持距离。她讲得很直白：会做题，是输入一道有答案的题，输出答案或一段证明。这一项 AI 现在做得相当好。但她认为这只是数学大陆的海岸线，离内陆还远。

她不喜欢"AI 会做数学"这个说法。她对自己公司 Axiom 的定位是另一套词："deep tech，像 SpaceX。" 不是调参，不是套壳大模型，是从 Lean 编译器、verify proof 加速、Mathlib 协作工具——他们造了 12 到 13 个辅助工具，因为开源社区的不够快、不够稳。这不是模型公司的活儿，是基建公司的活儿。

这种姿态本身就是一种判断：当大家都说 AI 会做数学的时候，她觉得地基都还没打完。

Putnam 满分的真相：大力出奇迹

按洪乐潼在节目里的原话：2025 年 12 月 6 日，Axiom Prover 当天拿到考卷，把 12 道题全部解了出来——是 Putnam 这一届竞赛的满分。她说，"人类历史上有五个满分，这是第六个，是一个 AI 拿到的"。

外界把这看作 AI 数学的里程碑事件。她自己怎么看？

她讲了一道题。Axiom 团队里有 Evan Chen，美国 IMO 国家队教练，极度天赋型选手。Evan 看到那道题，画了一条辅助线，会议室里所有人一眼就懂——就这么做。一图秒解。

AI 没找到这个解法。

Axiom Prover 给出的，是几千行 Lean 代码，硬生生分类讨论、暴力枚举，把这道题从头啃出来。 洪乐潼用的词是："大力出奇迹的 AI"。

这是她自己的原话。AI 拿了满分，解法是暴力枚举。Evan 那条辅助线代表的那种"一眼看穿"的解法——AI 没走那条路。

洪乐潼对这条路径不陌生。她说自己在 MIT 数学系是"最愚蠢的那一个"——同学任秋雨、张盛桐、高继扬，都是她"小时候看着新闻长大"的那批人。她做几何题的方式是把所有点都转成复数硬算，往往比天赋型选手多花两到三倍的时间。她管自己叫"打不死的小强"。

她懂暴力解法的价值，也懂它的边界。她说 AI 现在的位置是"拐杖和工具"——不是顶替数学家，是验证人写的代码、降低幻觉。

公众叙事把"满分"理解成"天才"，把"解题"理解成"创造"。她的拒绝里有一种数学家的洁癖：证明不是答案，是说服力。

三件套：AI 数学接下来要打的仗

洪乐潼描述 Axiom 的技术地图时，用了一个三件套：

prover（证明器）+ conjecturer（猜想器）+ knowledge base（知识库 / auto-formalization）

prover 是当前最热闹的那块。给一道题，AI 给出形式化证明，Lean 代码可以跑，跑通即验证。DeepSeek Prover、AlphaProof、HyperProver 都在这条线上。这是公众能看到的 AI 数学。

prover 重要，但她认为另外两件事被严重低估，尤其是 auto-formalization——把人类已经写好的数学，从 arXiv 的 PDF，翻译成 Lean 代码。

她讲了一个很硬的事实：全世界所有 Lean 代码加起来，token 数量"没多少"。 这意味着什么？大部分人类数学的定义不在 Lean 里——AI 连题目都写不出来，更别提证明。这才是 AI 数学的真正地基缺失。

陶哲轩、Kevin Buzzard、Alisa Kontorovich 这些数学家组织过几个大型形式化项目，把一篇大证明拆成"蓝图"（blueprint），分发给全世界的本科生各认领一块去填，星星之火可以燎原。这是当前形式化大型数学的主要路径——用人力。

洪乐潼想把这一步自动化。把一篇 20 页的 arXiv 论文，拆解成几百页的细粒度蓝图，再翻译成 Lean。她说这一步"比 proving 还难"。原因很现实：你不只是在验证已知答案，你在定义——给机器一种它从来没见过几个 token 的语言，让它把人类数学的全部存量翻译进去。

至于 conjecturer——更难。证明题有 reward 信号：证出来是 1，没证出来是 0。但猜想好不好，怎么衡量？ 你不能让 AI 提出"1+1=2"这种平庸到无意义的"猜想"。Self-Play Improver 那篇论文用证明长度做"优雅过滤器"——一个题比它的证明长还是短——但洪乐潼说这"很粗糙"，做到本科以上数学就不够用。有意义的猜想，今天还没有 reward 函数能描述。

拉马努金的处境：AI 像那个不会证明的天才

洪乐潼自己讲了拉马努金的类比。这可能是这一期 4 小时里最锋利的一段。

拉马努金从印度来到英国，给 Hardy 和 Littlewood 看草稿本："这些都是对的，我没受过训练，我不知道怎么去证明它。" Hardy 们花了大量时间帮他补证明。

她问：证明是什么？她自己回答："证明其实某种程度上它是影响力，就是我只要能够去把这个东西严丝合缝地逻辑证明出来，我这个数学的发现就是可以被接受的。" 证明是说服背景不一样的人接受发现的工具。

然后她说了那句关键的话："这正好是 AI 的处境。"

AI 像拉马努金，给出一个对的结果，但需要 Lean 来"证明"它，让人类相信它的输出可信，而不是幻觉的产物。形式化证明，是 AI 与人类数学共同体之间的翻译官。

这里有一个被很多人忽略的翻转。传统叙事里，证明是创造性的束缚——天才直觉飞出去了，证明的繁文缛节把它拉回地面。在洪乐潼的框架里恰恰相反：证明是创造性的基础设施。 没有证明，直觉无法流通。没有 Lean，AI 的直觉就无法被人类接受。

更深的一层是 Curry-Howard 对应——一个数学定理，也是 Lean 这门语言存在的哲学根基。Curry-Howard 说的是：每一个数学证明，可以等价地写成一个计算机程序。Math is code, code is math. Lean 既是定理证明系统，也是编程语言，因为这两件事在数学上本来就是同一件事的两面。

不是抽象。Axiom 把数学 prover 训练好之后，团队把同一个模型放到代码验证的 benchmark VeriBench 上跑——结果让团队自己惊讶。一个被训来证数学的 AI，在写出可被证伪的代码这件事上，自然就强。因为它们本来就是同一种活儿。

同一个范式：AI 生成 + 经典系统执行

读到这里，熟悉声入商业的读者可能已经感到一个共鸣。

胡渊鸣在 008 那期对谈 里讲过一个核心判断：在游戏渲染上，AI 永远是生成器，不是执行器。系统不是纯神经网络，是 AI 生成 + 经典图形学引擎执行的 hybrid——生成负责不确定性，执行保证确定性。

洪乐潼讲的，是同一个范式在数学里的镜像。

AI（大语言模型）做 Draft 和 Sketch，生成方向和草图——这一步允许幻觉和猜测。Lean 做 Proof，经典形式化系统来执行和验证——这一步要么跑通，要么报错，没有中间地带。

她说得很具体：能用 deterministic 系统解决的，就不上 probabilistic 的 AI。 Lean 里有个工具叫 Grind，"没有任何 AI 成分"，但能解掉一些其他公司拿出来 demo 的题。先让规则系统工作，AI 作为补充。这是工程经济账，不是技术情怀。

胡渊鸣在游戏世界里发现了它，洪乐潼在数学里发现了它。再往前一点，012 期 阿岛和 Hermes 在 Agent 应用层讲的也是同一种结构：Harness 是 Agent 的"车"，模型是"发动机"。三期放在一起：AI 变强不靠暴力扩参数，靠找到正确的"执行层"把生成锚定住。 在游戏里是物理引擎，在数学里是 Lean，在 Agent 里是 Harness。

004 谢赛宁那期 讨论世界模型时提的是相邻问题——AI 对物理规律的内化，那条线讨论的是怎么让生成本身符合规律，与本期不严格同构，但站在同一个问题意识里。

一个创业者的克制

技术之外，洪乐潼这期还有一个反复出现的姿态——降低预期。她说自己在 MIT 数学系是"最愚蠢的"。她预期过自己读不上数学博士，本来准备大一暑假去桥水做量化。是疫情把桥水实习挪到线上，又恰好 Ken Ono 教授给本科生的暑期数学研究项目（REU）的候补名单把她排到靠前——一连串偶然让她留在了数学里。

这跟"24 岁 CEO、58 岁教授来打工"的钩子近乎矛盾。但她讲到一个细节：博士级别的概率论那门课，期中满分 40 分，全班平均 9 分，她和几个大一的同学拉了后腿。她那天的反应不是沮丧，是把 Rudin 的实分析重新捡起来从头学一遍。

她说自己对苦难上瘾——借用黄仁勋讲过的 pain and suffering 那套话。她说大部分 founder 都这样。

访谈里有一个少被注意的概念，叫 bounded vs free attention。被框架住的注意力 vs 自由注意力。她说好创业者和平均创业者的差距，就在 free attention 上——那些每天把日程排满的人，执行效率高，但失去了漫游的时间。她怀念小时候走路上学时大段的"游神"时间。

把这些自述放在一起，钩子里那个少年得志的 CEO 形象会让位给另一个：一个习惯被动接受坏消息、然后回去重新打地基的人。Axiom 在做的事——把 auto-formalization 这种没人想啃的硬骨头啃下去——和这副脾气是同一种来源。

声入商业说

这一期的核心是一句话：会解题，不等于会做数学。 AI 数学接下来要打的，是 prover、conjecturer 和那个被严重低估的知识库——auto-formalization 这三件套，不是奥数刷分。

AI 拿了 Putnam 满分，用的是暴力枚举。这个满分是真实的——它说明 AI 已经能在特定条件下达到顶级人类水平。但它也说明 AI 还没有真正"看见"那些题目。

更深的部分——conjecturer，auto-formalization，让 AI 从"解题工具"变成"数学发现者"——几乎还没有人开始打。洪乐潼在那里。她说一个 AI 能提出有意义猜想的"ChatGPT 时刻"，"五到十年有可能"。这个时间表在当下 AI 行业里算保守。

她说自己墓碑上不想写 founder，想写学徒。一个 24 岁、刚拿了 16 亿美金 A 轮估值的 CEO 能说出这个词，是这一期访谈里走出去之后还会反复回想起来的一句。

评论区留给你：如果有一天 AI 证明了一个困扰人类几百年的猜想，但用了一个现有数学体系里没有的公理——你会接受这个证明吗？

点击"阅读原文"可以收听完整访谈——4 小时 24 分钟，是这一年里关于 AI 数学最不"宣传"的一期。也推荐去小宇宙搜索"商业访谈录"订阅这档播客——张小珺主持，004 期我们写过她对谢赛宁的 7 小时访谈，是我们的常规选题索引。