洪乐潼（2001年生，广州长大）描述了两种截然不同的"被数学击中"的体验：一种来自看别人的成果，一种来自自己解题的过程。
她最早的解题震撼来自罗斯夏令营（Ross Program）。每天必须做完全部题才能拿到下一天的题集，像"游戏打怪一样"。最终推导到二次互反律时，简洁的表述背后展现出极深的证明和极具创造力的解法。
洪乐潼的定义：数学是人类决定创造的一个文明体系。基于一些我们"愿意接受是理所当然的"公理，然后往上搭建。这个过程"有一点像艺术"——数学是介于艺术与科学之间的存在。先从例子出发，发现规律，猜测下一步"应该是怎样的"，再去证明它。
洪乐潼反复强调自己"不是天赋型选手"，而是"蛮力型选手"——无法做出欧式几何题的直觉解法，只能用复数法"大力出奇迹"，需要比别人多两到三倍的时间。
洪乐潼引述一个导师的框架：Bounded Attention（被框架住的注意力）是你每天必须执行的邮件、任务、deadline；Free Attention（自由注意力）是爱因斯坦洗澡时的灵感时刻。她认为：区分一个平均的创业者和一个有策略性决策力的创业者，关键在自由注意力。但两者需要配比，且"这个配比每个人不一样"。
洪乐潼的"蛮力做几何"和Google DeepMind的AlphaGeometry背后哲学一致——都是把几何图形变成符号表达式来解决，AI因此能解决81%的历史IMO几何题。这暗示了一个深刻的对称：蛮力型人类数学家与蛮力型AI数学家之间存在天然的互补关系。
洪乐潼在广州数学奥赛体系中（1班到24班按成绩排列，入学时在4班"洗手间旁边"）意识到自己"在拒绝被驯化成一个竞争力很强的人"。初中开始自学高等数学——微积分、复分析——从零和游戏转向正和游戏。关键发现：她的竞赛成绩反而因为发散性探索（高等数学）而提高，这与AI中的transfer learning（转移学习）现象高度一致。
MIT的经历塑造了洪乐潼的核心人格："失败是我的默认项"。
住在东校区Pi楼（圆周率楼），楼上全是IMO/IPhO/IOI选手。听从学长建议上博士概率论——第一天开讲测度论、Borel sigma代数，完全听不懂。期中考40分满分，全班平均分9分，她和几个大一学生都是个位数。
小团队的奖励机制被迫中断。必须学会从"事情本身的难度"中找到快乐——从人际驱动转向事物驱动。
本来要去桥水基金实习，被小野肯教授的暑期数学研究项目（REU）候补名单"捞上来"——因为疫情很多人放弃了。从此走上数论研究之路。
获得北美数学本科生最高荣誉摩根奖。但她强调"我并不觉得我是数学最好的那一个人"，且"谁拿到谁拿不到，随机性很大"。
洪乐潼的学术路线——数学(MIT) → 神经科学(牛津) → 法学(斯坦福) → 数学博士(斯坦福)——看似杂乱，实则每一步都在为AI for Math积累认知。
洪乐潼是Textualist。她在法学课上想到：如果已经到了能拿AI看宪法是什么意思的时代，"我为什么不能拿AI做数学？"——而这需要的不是英语，而是更结构性的呈现：Lean形式化语言。
从2020年起，Kenny Luo就在做Lean形式化证明——当时Mathlib还是空的，他是把本科代数、本科分析一行行打进去的5-7个学生之一。Kenny是Kevin Buzard的学生，现在也在Axiom。
Axiom的创始故事发生在Palo Alto的Verve咖啡馆——一个六人桌、周末有狗的地方。
洪乐潼抱着厚厚的法律书去咖啡馆做作业（"周末有狗，可以看狗喝抹茶"）。舒伯是Meta FAIR的Director，Facebook AI Research的元老，GPU经验20年，AI经验10年，曾在百度硅谷AI研究室与Dario Amodei（Anthropic创始人）共事。两人在同一张六人桌上认识——因为拉窗帘说上了话。
持续一年半只聊科学和历史。洪乐潼不知道舒伯在Meta，舒伯可能不知道她有数学研究背景。
洪乐潼某天晨跑后觉得"这件事真的要发生了"，找舒伯算需要多少张GPU卡、融多少钱。"两个人在Verve拿了张餐巾纸在那算。"
"他在Verve咖啡店说的——'好多好的人都走了，感觉这个地方不太像以前的地方。'然后问要不要一起做。"洪乐潼回忆自己"不太敢问"——因为舒伯是AI元老。
洪乐潼曾在同一家Verve咖啡馆遇到主要竞争对手的CEO Tudor，主动问"你们招人吗？"——想加入而不是自己创业。对方回复："我们只招计算机的PhD。"洪乐潼是数学PhD——于是决定自己做。这个细节揭示了Axiom和竞争对手之间DNA的根本差异。
A轮原本没打算融——2025年圣诞节时，已有投资人主动递出term sheet。1月5日被叫到外地做pitch，当晚收到offer。最终由Menlo Ventures领投（Anthropic最大机构投资人），Matt Krisiloff是从种子轮开始支持Axiom的partner。
小野肯（Ken Ono）教授加入Axiom的故事是整场访谈中最戏剧化的段落之一。
Ken Ono写信说他要来湾区，如果加入了OpenAI或DeepMind，希望洪乐潼有心理准备——因为可能存在战略竞争关系。洪乐潼的反应："你如果能加入OpenAI和DeepMind，那你为什么不来我这里？"
Ken Ono去了OpenAI，但没来Axiom实地看。洪乐潼以为"凉了"。结果在Zoom上定了——Ken觉得Axiom"更数学"，OpenAI做数学的同学不多。整个过程在对方offer即将expire的两三天内完成。
Ken的父亲是筹款为拉马努金在印度修雕像的数学家之一。拉马努金的遗孀给世界各地数学家写信众筹，Ken父亲回了信。Ken的办公室里至今还有拉马努金遗孀写给他父亲的那封信。Ken本科时绩点不好、高中没毕业——他的父亲用拉马努金的故事勉励他："任何时候开始也不算晚。"
洪乐潼详细解释了Lean形式化语言及其在AI for Math中的核心地位。
Lean是一种形式化证明语言——你可以把数学证明写成代码，跑完看到一个勾（证明正确）或报错（某行有问题）。它既是编程语言，又自带验证能力——"既是C语言，又是GCC compiler和C runtime两者合一"。这使它非常finicky（脆弱），但也非常强大。
| 挑战 | 问题 | Axiom的解法 |
|---|---|---|
| 数据稀缺 | 全世界Lean代码加起来tokens很少 | 用AI生成合成Lean数据（而非靠人手打） |
| 验证速度 | 社区原有的comparator慢100倍 | 自建verify proof系统，快100倍 |
| 搜索成本 | AlphaProof用蒙特卡洛树搜索太贵 | 用sub-agents + skill learning替代（类似Anthropic的方向） |
| 工具缺乏 | Lean没有好用的hammer（一斧头解决sorry） | 自建12-13个辅助工具 |
Axiom的证明树已从40个节点scale到4000个节点——更深更广的搜索。
2025年12月6日，成立仅四个月的Axiom在普特南大学生数学竞赛中取得满分120分——人类历史上98年来仅有5个满分，这是第六个，也是第一个由AI获得的。
Axiom发现了一个令所有人惊讶的现象：数学定理证明能力能转移到代码验证能力。在VerifyNot benchmark上，原本DeepSeek Prover达到11%，Axiom的系统达到98.93%。洪乐潼认为这是因为数学证明和代码验证在Lean中的目标函数"聚拢"了——都是形式化语言，而不是一个Python一个英语。
洪乐潼将AI for Math的核心科技拆解为四个组成部分，并明确了Axiom相对于竞争对手的差异化定位。
Christian Szegedy在Google开始用HOList做定理证明；ATPboost（波兰人Bartosz，现在Axiom）。
Ilya Sutskever带队做GPT-f、mini-f2f。Jesse Michael Han、Stan Polu等后来成为创业者。
一个实习生在Google DeepMind秘密开始AlphaGeometry项目。
IMO六道题做了五道，28分银牌——"跨世纪的时刻"。
四个月从零到满分。同时解决了交换代数、代数几何、代数数论、离散数学的多个研究问题。
Lean语言体现了这个数学-计算机的同构关系：代码即证明，证明即代码。这意味着Axiom的Prover可以同时做到两件事——生成数学证明和验证程序正确性。在Axiom的系统中，这不是两个目标函数拉扯（Python + 英语），而是统一的形式化空间。
洪乐潼提出一个精彩的观察：数学作为英语的子集，词汇的概率分布完全不同——比如代数几何中的"germ"，在英语中是"细菌"。如果让AI在英语中做数学，"这不是事情的全貌"。
洪乐潼详细阐述了Axiom的商业路线图：验证（Verification）是第一个市场，之后是AI for Science和最优化。
| 市场 | 应用场景 | 时间 |
|---|---|---|
| 验证（第一市场） | 芯片验证（替代基于SMT的Jasper）、代码验证（不需要test case） | 正在探索 |
| AI for Science | 为物理学家、生物学家解决理论问题 | 中期 |
| 最优化 | 覆盖所有edge case的搜索引擎级能力 | 远期 |
洪乐潼指出验证的难点不在证明本身，而在specification（定义/命题）——你如何把问题精确地写成形式化的命题？这和数学中猜想的困难是同构的。比如First Proof挑战的10道题，Axiom甚至无法参加——因为题目涉及的定义完全不在Mathlib里，"题目我都放不到Lean里面"。这解释了为什么猜想家（Conjecturer）是Axiom的长期战略重点。
这个贯穿整场访谈的哲学问题，在洪乐潼这里得到了层次丰富的回答。
国际数论学家看张益唐的证明时觉得和他们熟悉的学派"非常不一样"，但结果是正确的，于是接受了。James Maynard的2022年菲尔兹奖带来了另一套证明技巧。学生们继承、比较、简化——"这个过程是非常有意思的智力过程"。
洪乐潼被问到一个思想实验：如果Axiom的AI证明了重大猜想但使用了一个不属于现有数学的新公理？她的回答：
洪乐潼描绘了AI for Math成功后的世界图景——一个"数学的供给会爆炸"的社会。
洪乐潼引用了DeepMind纪录片中的一幕：AlphaFold成功后，有人建议做一个平台让结构生物学家提交要折叠的蛋白。Demis Hassabis问"有多少蛋白"，回答"2亿个"，Demis把笔扔在桌上说"Fold everything, that was a stupid idea"。洪乐潼的类比：如果算力无限，"我们要把所有人类能想到的数学问题全部解决"。
洪乐潼反复强调自己不是天赋型——用复数法暴力做几何、六个月做不出sphere packing问题但每周汇报、期中考40分只拿4分。但这恰恰是AI for Math创业者的最佳背景：她深刻理解AI作为"蛮力型数学家"的价值，因为她自己就是这样做数学的。AlphaGeometry的哲学和她的解题方式完全一致。这提示了一个反直觉的创始人筛选标准：在天才云集的领域里，"最愚蠢的那个人"可能最理解如何用工具增强人类。
洪乐潼的核心洞见：之前大家把"数学当语言做拐杖"——但数学应该变成Lean。语言模型的幻觉问题在数学领域有了精确解：形式化验证给出100%确定的对错信号。这不只是数学问题——芯片验证（替代SMT/Jasper）、代码验证（不需要test case）都是直接应用。Axiom在代码验证benchmark上从DeepSeek的11%跳到98.93%，证明了数学证明能力向代码验证的transfer learning是真实的。
证明可以验证对错，但定义（specification）没有对错之分。猜想家比证明家更难训练，因为"我不知道这个定义是对还是错"。这个问题同构于代码世界的specification问题：你能写出程序，但能精确定义你要解决什么问题吗？洪乐潼坦承Axiom无法参加First Proof挑战——"题目我都放不到Lean里"——因为涉及的定义不在Mathlib中。这是AI for Math和AI for Code共同面临的根本瓶颈。
Axiom的创始故事几乎全部发生在Palo Alto的Verve咖啡馆：洪乐潼在那里认识了舒伯（拉窗帘说上话），在那里和竞争对手的CEO偶遇（被拒绝后决定自己做），在餐巾纸上算融资，墙上还有她和舒伯的拍立得。这不是巧合——硅谷的创新密度来自物理空间的碰撞，而非线上网络。洪乐潼说她"没有办法开超过一小时的Zoom"，但和舒伯每次讨论四五个小时。
洪乐潼将New Lab的诞生归结为一个"基本作用力"——人类的好奇心。即使OpenAI/DeepMind开出1亿美元package，也"无法压制住青年研究者的好奇心"。她引用Peter Thiel的话："垄断导致创新，竞争导致平庸"——New Lab是被使命而非ego驱动的。假设AI解决了所有数学问题——"还会有数学家吗？"——答案是一定会有，因为"你不让我看那100万行Lean代码，我都会去看"。
洪乐潼对自己公司的判断极为清醒：结果一定是"极好或极坏"，没有中间态——"要么登月成功，要么火箭坠毁"。她的核心竞争策略是效率（"一个单位的创新需要多少单位资源"）和人才密度（30人 vs 竞争对手50-75人，但前30篇AI for Math论文的大部分作者都在Axiom）。如果失败了？"我可能会做跟神经科学相关的事情——brain-machine interface目前的实现都太不理想了。"
被问到墓志铭想写什么，洪乐潼的回答不是"数学家"也不是"CEO"——而是"学徒"。从数学到物理到神经科学到法学到AI，她的模式是在每个领域都做学徒。她说自己"最快乐的状态是research scientist intern——这个intern很重要，因为如果我说的话比较愚蠢，大家会觉得正常"。这个回答解释了为什么一个"最不可能创业的创业者"最终创建了一家追求"天书中的证明"的公司——因为学徒的驱动力不是控制，而是好奇。
| 数据点 | 具体内容 |
|---|---|
| Axiom团队规模 | 30人（竞争对手50-75人） |
| 种子轮 | 6400万美元，估值3亿美元（2025年1-7月） |
| A轮 | 2亿+美元，估值16亿美元（2026年1月） |
| 普特南成绩 | 满分120分（成立4个月后，2025年12月） |
| 代码验证分数 | 98.93%（vs DeepSeek Prover 11%） |
| 自建验证器速度 | 比社区版快100倍 |
| 证明树规模 | 从40节点scale到4000节点 |
| 自建工具数量 | 12-13个辅助Lean的生成和验证工具 |
| 团队IMO选手 | 5个IMO（含4个IMO金牌） |
| 领投方 | 种子轮B Capital（文艺复兴联创Howard Morgan）；A轮Menlo Ventures |
| 竞争对手 | 成立早2年，融资约为Axiom种子轮的5倍 |
| 洪乐潼年龄 | 24岁（2001年生） |
| 直觉能力预测 | 5-10年可能实现AI数学直觉 |
| 公司名字来源 | "Axiom"（公理）——源自《数学天书中的证明》 |
| 会议室命名 | 高斯、庞加莱、希尔伯特、Lovelace、图灵（因"polymath"原则选定） |