对洪乐潼的4小时访谈：AI for Math、Lean与AI数学家的未来

概览

本期围绕洪乐潼的个人成长、数学观、AI for Math 技术路线，以及 Axiom 的创业过程展开。访谈从“被数学击中”的体验谈起，逐步进入数学是被创造还是被发现、证明与直觉的关系、形式化证明和 Lean 在 AI 数学家中的作用。

核心讨论是：AI for Math 不只是让模型会做题，而是把数学转化为可验证的形式化语言，让 AI 能生成、验证、积累并最终扩展数学知识。洪乐潼认为，证明系统、猜想系统、知识库和自动形式化共同构成 AI 数学家的技术版图。

访谈后半段转向创业：Axiom 如何从咖啡馆里的讨论变成融资、招人、做系统、冲 Putnam 满分和研究级数学问题。她反复强调，这家公司更像 deep tech 或登月项目，而不是单纯的模型公司；第一市场可能是验证，长期目标则是自我验证的高级推理能力。

分段落总结

[00:11] 开场与嘉宾背景

[事实] 主持人在硅谷 Facebook House 开场，介绍洪乐潼是本节目最年轻的嘉宾之一，方向是 AI for Math，所创办公司 Axiom 完成高估值融资。 [事实] 开场提到外界关注点之一是“57岁的美国终身教授辞职，去给24岁的华人女孩打工”。 [推测] 节目一开始就把个人传奇、数学技术和创业融资放在同一个叙事框架里。

[02:02] 被数学击中的时刻

[事实] 洪乐潼说，自己解题时这种体验较低频，但看别人漂亮解法时常被数学之美打动。 [事实] 她举了模形式与椭圆曲线之间联系、初等数论推到二次互反律等例子。 [推测] 她理解的数学之美，常来自不同领域之间突然建立联系。

[04:28] 数学是什么

[事实] 洪乐潼认为数学像人类创造的一套文明体系，从被接受的公理出发向上搭建。 [事实] 她说数学不只是解题，更包括从例子中发现规律、提出自然的问题并证明它。 [推测] 她把数学放在艺术与科学之间，强调结构、审美和可证明性共同存在。

[06:10] 数学被创造还是被发现

[事实] 她认为同一领域、相似训练背景的数学家之间，会形成对“自然”的默契。 [事实] 她用拉马努金、张益唐、James Maynard 等例子说明，证明是让新发现被共同体接受的方式。 [推测] 在她的叙述中，数学发现需要直觉，但数学共同体最终通过证明来建立共识。

[08:47] 直觉派、蛮力派与几何题

[事实] 洪乐潼说自己一直希望成为直觉派天才，但更像“蛮力型选手”。 [事实] 她小时候做欧式几何题困难，常用复杂数法把几何转成符号计算。 [事实] 她提到 AlphaGeometry 将几何问题转成符号表达，背后的哲学与她当年解几何题的方式相似。 [推测] 这段为后面“AI也可以用非人类方式解数学题”埋下了线索。

[12:11] AI数学家与自动定理证明

[事实] 她把 AI 系统中的模型分成能快速列证明大纲的“聪明型”和一步步写 tactic 的“蛮力型”。 [事实] 她提到 Axiom Prover 在普特南竞赛中拿到满分，而某些题的人类解法很优雅，AI 解法则可能是几千行 Lean 代码。 [事实] 她区分 ATP 自动定理证明和 ITP 交互式定理证明，并说现在只是把 ITP 中的人类换成 AI。 [推测] 她强调 AI 的数学能力并不必然模仿人类直觉，也可以通过形式化和搜索形成不同路径。

[16:35] 广州成长与自由注意力

[事实] 洪乐潼在广州出生长大，住得离学校近，常在走路上学时想数学题。 [事实] 她区分 bundled attention 和 free attention，认为自由注意力对数学家和创业者都很重要。 [事实] 她说小时候很多事情像玩，而不是像工作。 [推测] 她把童年的自由探索视为后来数学兴趣和创造性思维的重要来源。

[18:52] 创始人类型与Facebook文化

[事实] 她把创业者分成 visionary、executor 和 salesman，并认为自己更接近 visionary。 [事实] 她称扎克伯格更像执行型创始人，Sam Altman 更像销售型创始人。 [事实] 她说 Axiom 早期很多人来自 Facebook，因此部分继承了 Facebook 自下而上的文化。 [推测] 她对公司文化的理解，很受硅谷技术组织和早期团队构成影响。

[22:37] 竞赛、阅读与正和游戏

[事实] 她小时候喜欢百家讲坛、中国文学和历史，也喜欢课外看高等数学书。 [事实] 她认为数学竞赛像零和游戏，而学习高等数学更像正和游戏，可以自己探索深度和广度。 [事实] 她因为喜欢数论，考试时有时会先做最后的数论题，策略上并不最优。 [推测] 她对“荣誉”和“排名”的复杂感受，与早年竞赛环境有关。

[29:20] 小部落与合作式数学

[事实] 她回忆初中时和三到五个朋友研究跳马走满棋盘的问题，并尝试用归纳法构造证明。 [事实] 她把这种小团队合作联想到形式化证明项目中多人拆分任务、共同完成大型证明。 [推测] 她从早期游戏式探索中形成了对协作数学的好感。

[32:45] 高等数学的迁移效应

[事实] 她认为学习高等数学也会潜移默化提升竞赛数学能力。 [事实] 她提到 AI 中也有类似 transfer learning，即一个数学能力强的模型在编码能力上也可能表现好。 [推测] 她个人学习经验后来成为理解 AI 泛化能力的参照。

[38:32] 荣誉与失败默认态

[事实] 她说自己在每个阶段都觉得自己是环境中最愚蠢、最努力也看不到结果的人。 [事实] 她准备奥赛时曾短时间刷75套卷子，但仍没选上比赛。 [事实] 她说失败像默认状态，但自己并没有因此陷入痛苦。 [推测] 这种长期不在舒适区的体验，塑造了她对创业高压的接受度。

[40:18] MIT的困难课程与团队奖赏

[事实] 她在 MIT 大一第一学期选了博士概率论，第一天就遇到测度论，期中考试40分满分只拿个位数。 [事实] 她说当时的奖励感来自小团队一起面对难题、决定不退课。 [事实] 疫情后小团队消失，她逐渐学会从困难事情本身获得快乐。 [推测] MIT 的环境强化了她“什么难做做什么”的长期主义倾向。

[50:00] 服务型领导力与大学数学

[事实] 她认为最好的领导力更像服务型领导，像登山队后面递水的人，而不是拿喇叭的人。 [事实] 她说高等数学像搭乐高，可以从新定义、新概念出发搭出小宇宙。 [事实] 她去 MIT 是因为从小对 MIT 有很强信念，并在草稿纸上写 MIT。 [推测] 她对领导力的理解，与她后来把 CEO 角色描述为“递水的人”一致。

[57:20] 物理、牛津神经科学与AI

[事实] 她本科读数学和物理，选择物理部分因为想理解概率、随机曲面等数学研究在物理中的意义。 [事实] 她硕士去牛津学神经科学，后来因动物实验经历转向计算神经科学。 [事实] 她在英国接触到与 AI 紧密相关的计算神经科学研究者，并发现自己的快乐更多来自 AI。 [推测] 她的跨学科路径不是线性规划，而是不断被新的智力问题牵引。

[63:36] 法学、文本主义与AI for Math契机

[事实] 她在斯坦福读数学和法学，对宪法解释中的 originalism、textualism 和 living constitutionalism 很感兴趣。 [事实] 她说自己偏 textualist，喜欢按文字和定义严谨解释。 [事实] 她想到如果 AI 能看宪法文本的意义，也应该能做数学；而 Lean 把数学变成代码，提供了更结构化的呈现。 [推测] 法学训练让她更敏感于“定义、文本、规范和验证”的关系。

[70:45] Verve咖啡馆与Shubo

[事实] 她在 Palo Alto 的 Verve 咖啡馆读法律案例，因常坐同一张桌子认识 Shubo。 [事实] 两人先是普通聊天，后来发现彼此都有数学和 AI 背景。 [事实] 他们持续一两年聊科学、历史、技术，后来在这家咖啡馆讨论 AI for Math 创业。 [推测] Axiom 的起点很像硅谷式偶然相遇加长期高密度讨论。

[76:30] 决定创业前的自证

[事实] 2024年秋天，她开始认真考虑融资做 AI for Math，但先花两个月劝退自己。 [事实] 她读科学史、读 AI for Math GitHub 列表中的论文摘要和全文，并用费曼式过程推演技术方案。 [事实] 她得出的判断是：这个问题不一定是纯研究问题，也可能是工程问题。 [推测] 她把“先确认自己没有在骗投资人”看作创业前的道德门槛。

[80:00] 反浮躁创业与招揽早期作者

[事实] 她说自己过去很反感“AI founder”的浮躁感，更想做教授。 [事实] 她研究 ATPBoost、PatternBoost、Into Int 等论文，后来这些论文作者陆续加入 Axiom。 [事实] 她曾问竞争对手公司是否招人，对方问她是什么 PhD，她回答数学 PhD 后，对方说他们只知道计算机 PhD。 [推测] 她从“想加入别人”走向“自己做”，部分来自现有团队结构无法容纳她想做的问题。

[86:40] Axiom团队构成

[事实] 她说团队包括 AI、强化学习、agents、代码生成、编译器、Lean/Mathlib、元编程和纯数学等多类人才。 [事实] 她强调 Axiom 并不全是数学家，也需要非常强的工程能力。 [事实] 她希望数学家在团队中更多做对抗式 benchmark，找系统弱点。 [推测] 她相信多元背景会产生更多技术想法，而不是单一学科主导。

[92:00] AI for Math技术史

[事实] 她回顾了 2016 年 Google 的 Holist、OpenAI 早期 GPT-f/MiniF2F、DeepMind AlphaGeometry/AlphaProof 等发展。 [事实] 她认为 DeepMind 2024 年在 IMO 拿到28分是跨时代时刻。 [事实] 她把 Axiom 2025年12月普特南满分看作 DeepMind 开启序章后的一个阶段性尾声。 [推测] 她把 AI for Math 看成已有几十年定理证明传统与新一代 AI 系统的交汇。

[99:15] 种子轮融资

[事实] 她说融资过程很累，因为需要反复讲同样的事情、回答同样的问题。 [事实] 她最终种子轮融资6400万美元，估值约3.1亿美元，领投方包括 B Capital。 [事实] 她说自己 pitch 时很保守，会把商业模式不确定、技术风险等都讲出来。 [推测] 她不是典型夸张式募资者，但深度技术和团队愿景吸引了投资人。

[108:55] 年轻CEO与高压决策

[事实] 她认为年轻做 consumer 产品可能是加分，但做 deep tech 是减分，因为需要长期、高频、高风险决策。 [事实] 她用 zip lining 体验比喻创业：很多时候只能闭眼跳下去。 [事实] 她总结自己常常需要在执行与不执行之间选择更乐观、更行动导向的选项。 [推测] 她的 CEO 学习不是理论训练，而是在融资、招人、签约和取舍中被迫形成肌肉记忆。

[115:10] A轮融资与执行成果

[事实] A轮由 Melo 领投，融资至少2亿美元，估值约16亿美元。 [事实] 她说 A轮投资人看重团队六个月内从零搭基础设施、建系统、做工具，并在四个月拿下普特南满分。 [事实] 她还提到系统解决了一批研究问题，并在代码验证 benchmark 上有强表现。 [推测] A轮故事的核心不是单个模型指标，而是团队执行速度和系统能力。

[122:00] Axiom不是模型公司

[事实] 她说 Axiom 更像 deep tech 公司，不是单纯模型公司。 [事实] 她列举 Lean 数据少、Lean 语言脆弱、验证工具慢、需要自造十多个辅助工具等技术壁垒。 [事实] 她说他们没有沿用 DeepMind AlphaProof 的 Monte Carlo Tree Search，因为成本太高，需要找别的系统设计。 [推测] 她把公司护城河放在系统、工具链和工程化验证能力上。

[127:52] Shubo与Ken Ono加入

[事实] Shubo 后来决定加入，成为联合创始人；她说一个人做这件事会比较孤单。 [事实] Ken Ono 曾告诉她自己可能加入 OpenAI 或 DeepMind，她于是邀请他来 Axiom。 [事实] 她认为 Ken Ono 被 Axiom 更数学化的团队氛围和专注点吸引。 [推测] 这些关键人物加入，强化了 Axiom “数学公司”而非泛 AGI 部门的身份。

[136:20] 数学家在AI时代的角色

[事实] 她说 Ken Ono 是理论建造者，擅长连接不同领域、发现好问题。 [事实] 她认为 AI 进步后，人类数学家会在更高抽象层面推理，提出问题、选择方向、提供直觉。 [事实] 她希望 Axiom Prover 具备猜想能力，并与证明能力形成向上螺旋。 [推测] 她并不认为 AI 简单替代数学家，而是改变数学家工作的抽象层级。

[140:00] Putnam满分与Axiom命名

[事实] 2025年12月6日，团队拿到普特南试卷后，把题目变成形式化题目交给 Axiom Prover。 [事实] 当天下午他们一度已有8题，最终完成12题满分。 [事实] 她说 Axiom 这个名字呼应公理、形式化语言和从有限公理推导新结果的感觉。 [推测] Putnam 事件在节目中被讲成团队文化、系统能力和数学审美的共同展示。

[144:55] 从数学匮乏到数学丰富

[事实] 她认为 AI 会把社会从 math poor 推向 math rich，使数学供给爆炸。 [事实] 她设想数学家像资源分配者，决定哪些问题值得投入算力。 [事实] 她用 AlphaFold “fold everything”的故事类比：如果算力足够，可能应解决所有人类好奇的数学问题。 [推测] 这是她最激进的愿景之一：数学发现将指数级增长，并反过来服务科学和工程。

[151:00] Math is code，code is math

[事实] 她说数学和代码像孪生兄弟，数学证明可以变成计算机程序，代码也需要数学式验证。 [事实] 她认为 AI for Math 的 ChatGPT 时刻会同时涉及数学和代码。 [事实] 她介绍 Draft、Sketch、Proof 范式：先让 informal 模型列提纲，再转成 formal Lean，再填掉 sorry。 [推测] 她把形式化证明视为连接推理能力和产品落地的关键桥梁。

[158:00] 技术Aha Moments

[事实] 她提到用 subagents、learning from experience 和 skills 来替代昂贵的搜索，是团队的重要尝试。 [事实] 她说数学定理证明能力迁移到代码验证，是一个让团队惊讶的发现。 [事实] 她认为生成代码和生成证明的目标函数如果更接近，可能带来更好的 verified generation。 [推测] Axiom 的技术路线不是单点模型突破，而是系统级组合和迁移。

[161:25] AI for Math地图

[事实] 她说当前 AI for Math 大体是基于开源模型后训练，再放入包含多模型和工具调用的系统。 [事实] 她认为完整的 AI 数学家需要 prover、conjecturer、knowledge base 和 auto-formalization。 [事实] 她强调自动形式化被低估：把论文、定义、定理和证明转成 Lean，难度至少不低于证明本身。 [推测] 在她看来，AI for Math 的瓶颈不只是“会不会证”，还包括“能不能定义、拆解、转写和积累”。

[171:55] 形式化语言与Specification难题

[事实] 她把 Lean 类比为可运行、可报错、可验证的形式化语言。 [事实] 她说 coding 可以产出程序，数学可以验证性质；未来理想是写程序时同步证明程序确实满足目标。 [事实] 她指出 software verification 中，program、specification、verification condition 和 proof 都重要，而 Axiom 主要做 proof。 [推测] 她认为真正难点之一是 specification：人能否把需求精确表达成可验证命题。

[180:00] 第一市场：验证

[事实] 她认为验证是 Axiom 最好的第一市场，尤其是芯片、软件和复杂系统验证。 [事实] 她举亚马逊自动推理团队多年写26万行定理证明代码验证工程组件的例子。 [事实] 她说更广泛的未来是让普通编程也不再依赖有限 test cases，而是可证明正确。 [推测] 形式化验证的痛点更集中、付费能力更强，因此比大众数学产品更适合作为早期商业落地。

[187:30] 研究前沿与Benchmark

[事实] 她说团队已解决一些交换代数、代数几何、代数数论和组合概率意味的问题。 [事实] 下一步希望进入动力系统、概率、随机曲面等 Lean 基础建设较少的领域。 [事实] 她说研究级 benchmark 很缺，数学家出题很重要，但好题也很稀缺。 [推测] 系统能否跨领域处理 distribution shift，是衡量它是不是“AI数学家”的关键。

[193:00] ASI、递归自我改进与市场

[事实] 她不太喜欢 AGI 这个词，更愿意把目标理解为 specialized super intelligence。 [事实] 她把 Axiom 想象成从数学方向打到超人类任务边界，再扩散到代码验证、物理等扇形领域。 [事实] 她相信 recursive self-improvement 是很快能做出来的，而 Axiom 会是生态系统中的一环。 [推测] 她对通用智能的看法不是覆盖一切，而是从一个极深能力点向邻近领域扩展。

[202:35] 数学作为现实世界沙盒

[事实] 她说数学是现实世界的沙盒，因为它有清晰验证信号和结构化数据。 [事实] 她区分 AI for Math 和 AI for Science：后者常涉及实验室、现实反馈和更长迭代周期。 [事实] 她希望 Axiom 的 AI 数学家帮助 AI for Science 解决理论问题，但公司本身停留在数字世界。 [推测] 数学被她视为训练可靠推理和验证能力的低摩擦环境。

[207:10] 猜想、拉马努金与Ken Ono

[事实] 她说真正创造性猜想很难，目前机器猜想能力还很弱。 [事实] 她认为 Ken Ono 是高产猜想家，擅长连接不同视角，而拉马努金更像尖锐的直觉型天才。 [事实] 她提到“拉马努金式直觉”可能更像预训练产物，而 Axiom 当前主要做后训练。 [推测] 她承认现有形式化证明系统更偏验证型，距离真正天才式直觉仍有距离。

[214:20] 大厂、New Labs与竞争

[事实] 她说 OpenAI、DeepMind、Anthropic 等对 AI for Math 的切入点不同，有的做 informal，有的做 formal，有的用于提升推理。 [事实] 她认为大厂未必会亲自做 Axiom 正在做的所有事情，也可能与垂直创业公司合作。 [事实] 她说个人最大挑战是执行速度和学习速度之间的矛盾。 [推测] New Labs 的机会来自更高人才密度、更快试错和更强使命驱动。

[228:50] 自我奖励与终点

[事实] 她说现在更多从事情本身获得能量，团队则提供 grounded 的安全感。 [事实] 她最期待的是让顶尖推理能力成为默认状态，并且这种推理能自我验证。 [事实] 她希望 AI 能复现类似加罗瓦、拉马努金这样的数学能力，并让更多科学理论被发现。 [推测] 她的“终点”不是单个产品，而是推理能力基础设施的普及。

[233:30] 00后CEO与Bottom-up文化

[事实] 她说自己最快乐的状态不是 CEO，而是 research scientist intern，因为可以继续当学徒。 [事实] 她曾因随口发起 benchmark 小项目，让团队误以为这是 CEO 级高优先级任务，之后变得更 hands-off。 [事实] 她认为 Axiom 是技术人员作为主干的 bottom-up 文化，类似梦工厂。 [推测] 她的年轻和不以 CEO 身份自居，反而使团队更依赖自下而上的技术判断。

[240:00] AI会让数学无聊吗

[事实] 她喜欢高斯，也说如果和历史数学家共进晚餐，Erdos 会很有趣。 [事实] 她承认曾担心 AI 做完数学家能做的事会让数学变无聊。 [事实] 她后来认为人的元素、数学共同体、生日峰会、合作传统和新问题不会消失。 [推测] 她相信 AI 会改变数学文化，但不会磨灭人类的好奇心和智力社群。

[246:00] 看见上帝的面容与学徒身份

[事实] 她说自己小时候就相信数学家和科学家的意义之一，是探索基本真理。 [事实] 她在斯坦福教堂附近跑步时产生了强烈的 spiritual 感受，想到如果能让数学遗产成亿倍扩展，是否值得去做。 [事实] 她说墓志铭如果非要写，可以写“学徒”。 [推测] 她把创业视为继续学习和追问真理的一种形式，而不是身份成就本身。

[250:00] 人与事的冲突

[事实] 她承认 CEO 会遇到人与事情冲突的时刻，也经历过解雇实习生。 [事实] 她说遇到冲突时要收起乐观主义，谨慎做决定。 [事实] 她相信 authorship：人要承认自己参与书写了局面，不能简单把责任推给情境。 [推测] 这是她从理想主义走向组织管理现实的一段反思。

[252:30] 书、AI训练、新公理与中国AI

[事实] 她推荐初等数论、Davenport 的解析数论，也说自己喜欢《红楼梦》和一些企业家故事。 [事实] 她把训练 AI 和训练自己类比：看到模型刚好一点，就给它更难的题。 [事实] 她谈到 AI 可能用奇怪公理作弊，也说若新公理自然，数学共同体可能接受不同分支。 [事实] 她尊重中国 AI 玩家，特别提到豆包 Seed 在 AI for Math 上做得很好。 [推测] 她更希望行业保持科学交流、学术信任和纯真，而不是只被商业顾虑驱动。

[260:00] 论文、系统与语言集世界

[事实] 她提到 Christian Szegedy 白皮书、Transformer 做数学任务、Draft Sketch and Proof，以及 Gemini/DeepSeek/Seed/Hilbert 等 prover 工作。 [事实] 她说自己 bet system，不 bet model，并相信 recursive self-improvement 很快会出现。 [事实] 看到“语言集世界”这个名字时，她想到数学家几千年来一直在用自然语言写逻辑代码。 [推测] 节目最后把数学、语言、代码和世界模型重新扣回主题：语言能展开世界，形式化能验证世界。

播客点评/总结

这期的价值在于，它不是单纯介绍一位年轻创始人的传奇故事，而是把数学共同体、形式化证明、AI 系统设计和硅谷创业放在一起讨论。洪乐潼的表达里既有技术细节，也有很强的个人经验线索：从广州竞赛、MIT 挫败、牛津神经科学、斯坦福法学，到 Axiom 的融资和团队。

亮点是 AI for Math 的技术图景讲得比较完整：证明不是唯一核心，自动形式化、猜想、知识库、benchmark、Lean 工具链、代码验证和系统 orchestration 都被纳入其中。对想理解 AI 为什么会进入数学、以及数学为什么可能反过来改变代码验证和科学发现的人，这期信息量很高。

局限是访谈很长，话题跳跃也很大；部分技术名词依赖听众已有背景，例如 Lean、Mathlib、ATP/ITP、program synthesis、formal verification 等。[推测] 对非技术听众来说，最容易进入的线索可能不是术语，而是“如何把直觉变成可验证的证明”这一主线。

[推测] 这期适合三类听众：关心 AI 前沿和 New Labs 的人，关心数学与形式化证明的人，以及关心年轻 deep tech 创业者如何形成判断、招募团队和面对不确定性的人。