# 对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的

> 张小珺商业访谈录 No. 137 精读

- 发布日期：2026-04-20
- 主持：张小珺
- 原节目：https://www.xiaoyuzhoufm.com/episode/69e4e6951d989496e7fecc7b
- 网页版：https://zhangxiaojun.qiaomu.ai/ep/69e4e6951d989496e7fecc7b.html
- 精读字数：约 20846 字（阅读约 46 分钟）

> 本文为 zhangxiaojun.qiaomu.ai 基于节目转写的 AI 整理精读，不是逐字稿；引用请注明出处并链接网页版。

2026年4月，硅谷那栋淡蓝色的Facebook小屋，张小珺见到洪乐潼。她24岁，00后，广州长大，MIT数学与物理本科，牛津神经科学硕士，斯坦福数学博士与法学博士读到一半。她创办的Axiom刚完成2亿美元A轮融资，估值16亿美元。

比融资数字更抓人的是一条人事新闻：57岁的美国终身教授Ken Ono辞职，去给24岁的华人女孩打工。Ken Ono是数论学家，也是拉马努金研究的重要学者。洪乐潼第一次接受中文访谈，就在这栋小房子里聊了4个小时。

这期对话从数学的美讲起，一路讲到Lean、自动形式化、普特南竞赛满分、融资竞拍、Neo Labs和登月式创业。洪乐潼反复说自己是蛮力型选手，不是天赋派。她把创业看成binary outcome，要么登月成功，要么火箭坠毁。下面是她这4小时里值得留下来的信息。

## 被创造的与被发现的 0:02:14

张小珺用“被数学击中的时刻”开场。高斯说像闪电。洪乐潼的版本更安静：她经常在看别人结果时觉得“这个东西怎么这么美”。第一次是椭圆曲线与模形式对应，一个偏代数的表达式和一个更几何的对象被联系起来。她说数学中两个领域出现交集，每次都让她觉得非常优美。

她把数学定义成一种人类文明的契约。数学家先接受一些公理，约定哪些东西可以当作理所当然，再往上搭。有人追求最少的公理，有人追求最有意思、搭配最合理的一套系统。搭理论的过程先从例子出发，发现规律，猜下一步该是什么，再证明。她认为**数学介于艺术与科学之间**，解题只是其中一部分。

数学是被发现还是被创造，洪乐潼没有站死一边。她讲拉马努金到英国见哈代和李特尔伍德。拉马努金像外星人，带着草稿本说这些全是对的，自己没受过数学训练，不知道怎么证明。哈代他们觉得这些东西很新，又感觉是对的，于是开始用证明说服彼此。她由此说，**证明是一种影响力**。只要严丝合缝地证明出来，数学发现就能被共同体接受。接受之后，人们还会争论证明美不美、自然不自然。

张小珺问她属于直觉派还是证明派。洪乐潼说自己一直想当直觉派、天才派，这也是她小时候痛苦的根源。她自认没有特别大的数学天赋，是蛮力型选手。奥赛卷子第一道欧式几何题是必拿分，她偏偏做不出来。她的大脑更偏代数符号，几何和拓扑很差。她的办法是用复数法硬算，把每个点、每条线照本宣科套进去，不需要理解几何意义，花别人两三倍时间。

她提到Google DeepMind的AlphaGeometry。这个项目把几何图形变成符号表达，用AI解决历史上IMO几何题。洪乐潼说，这和她的复数法哲学一样，都是把几何转成符号。她在MIT也这样活。身边所有人看起来都是天赋型，她看左边、看右边，就知道自己不是。Henry Kong教授给她一个28维球堆积的小问题，她想了六个月，什么都没想出来，但每周都去汇报这周试了什么、没成功什么。她说这种蛮力型可以和天赋型互补，脏活累活她来干。

普特南竞赛的AI解法最能说明她的观察。2025年12月，Axiom的Axiom Prover在普特南大学生数学竞赛拿到满分。过去98年只有5个人满分，这是第6个满分，由AI拿到。团队里有一位IMO教练艾文晨，看到某道题画了一张图，所有人一看就说“你做出来了”。AI没有找到这个图解法，它写了几千行Lean代码，靠枚举、分类讨论、一步步核实，硬做出来。洪乐潼说，**机器会用自己擅长的东西给出完全不一样的解法**。比较人类和AI背后的数学，非常有意思。

她还纠正了一个常见说法。自动定理证明并非深度神经网络出现后才有的领域。没有AI的时候，就有一群计算机科学家希望基于规则的电脑系统帮助人类解决数学问题，这叫ATP。交互式定理证明叫ITP，人类数学家会写Lean程序，和电脑系统合作证明。现在只是把ITP中的人类换成了AI。这个古老学科和AI的交集，才是今天AI for Math的位置。

## 自由注意力与蛮力型选手 0:14:38

洪乐潼在广州长大。她最深的童年记忆是好吃的东西多，家离学校近，走路十分钟。上学路上她会想数学题，想着想着走到不知道哪里去。她后来创业，一位导师讲bounded attention和free attention。bounded attention是被框架住的注意力，早上起来看邮件，执行有截止期的事情。free attention是自由注意力，大脑可以游荡。她认为**自由注意力是拉开创业者与数学家差距的地方**。

她怀念走路上下学的状态。很多灵感不是线性投入换来的。自由注意力时间可能什么都没想到，后面被任务逼迫时，大脑会callback，回到之前打下的基础，突然冒出一个有创造性的想法。她讲爱因斯坦洗澡。限制性注意力和自由注意力需要配比，每个人的配比不一样。

她也讲三种创业者：visionary、executor、salesman。扎克伯格是执行狂，马斯克是visionary，Sam Altman是salesman。洪乐潼自认是visionary，肯定不是salesman或executor。她说Facebook的人bleed purple，血液里是紫色，扎克伯格色盲，办公室用了大胆颜色。Facebook园区像梦工厂，有24小时冰淇淋店，有地方玩鼓、玩吉他。Axiom大部分早期员工来自Facebook，文化更像bottom-up，不是top-down。

广州的童年不止数学竞赛。她看《百家讲坛》，喜欢易中天讲三国、诸子百家，喜欢黄永玉的《比我老的老头》《大雅宝胡同甲二号》。她妈妈是北京人，家里受京城文化影响。她的自由注意力很旺盛，数学教练批评她不是最刻苦的那一个。她遇到一道题会死磕，但过程像玩，不像work。她区分限制性注意力和自由注意力，靠主体感受：你到底觉得在玩还是在工作。

初一她发现可以找高等数学书看。微积分、实分析、复分析，她觉得有意思，因为不再是零和游戏。数学竞赛里同学要考同一场试，友谊和竞争搅在一起。高等数学是正和游戏，你可以自己走到某个深度、广度，找班里感兴趣的人一起讲，不需要某天同时参加考试。她还是要回来打零和游戏。卷子四道题，最后一道是数论，她会先从最后一道开始，因为“数论多美啊”。理智告诉她应该先做欧式几何、代数不等式，最后数论大概率做不出来。她还是先做数论，时间开始流逝，这在固定比赛时长里不是最优策略。

她讲小学奥校的排名。四年级到六年级，每月考一次，每学期把一班到24班重新排列。22、23、24班是重点班，一班在楼底，24班在楼顶。她进去时在4班，洗手间旁边，说明入学考试考得真差。她卯足劲想上楼顶。初一初二开始看高等数学，她开始不太想玩这个游戏。初三要打初中数学联赛，她临到比赛才准备，最后考得很好。高中更多时间学英语，准备出国。她发现群体有清晰目标，每个人都在准备下一季度竞赛，你自己有一套完全不同的mental model，就会去找部落，找谁也读跟考试无关的书，和这些人成为好朋友。

她讲一个初中游戏：n×n棋盘，走马步，每走到一个格子标数字，目标是走满所有格子不重复。八乘八棋盘，希望尽量靠近64。她和三五个朋友比赛谁走的数大，后来想证明任何n至少为5的棋盘都有走满的方式。他们猜用数学归纳法，需要构造base case。这个工程很复杂，大家群策群力。她把这个游戏和形式化证明项目类比：陶哲轩、Alex Kontorovich做素数定理形式化，把任务拆给全世界几百个数学家和Lean程序员。数学常被强调成天才一个人证明困扰所有人几百年的猜想，软件工程则是几百几千人合作一个大项目。合作需要结构，需要把任务拆小。

MIT的第一个学期，她选博士概率论。第一天上来测度论，从Borel sigma代数讲起，几个大一学生面面相觑。期中考满分40分，全班平均9分，他们几个大一小孩都是个位数。她第一次在40分考试里拿4分。她没有觉得自己失败，因为失败是默认项。她重新学Rudin的实分析。她讲MIT东校区，庭院里有木头过山车，有人在玩喷火，非常nerdy。她住的楼层叫pi floor，住着IMO、IPhO、IOI选手。她每天顶礼膜拜这些大神。她预期自己是最傻的一个，所以适应得很好。

疫情把她的小团队打散。大一下学期所有人离开学校，课还要上。她必须从事本身找快乐。她讲MIT学生雨天、暴风雪里晨跑，毅力有感染性。她后来发现创业者普遍对苦难上瘾。投资人找founder，会找对疼痛上瘾的人，有一句话叫chip on the shoulder，chips in the pocket，肩膀上的伤痕转化成口袋里的硬币。她听起来觉得不可理喻，但承认有一定正确性。

> 失败是你的默认项。

她说自己在每一个时期都觉得自己是环境里最愚蠢的那一个，最努力也看不到结果的那一个。失败是自我定义的，不是客观定义的。她乐观，所以经常失败，每次又觉得自己能到达下一个地方。

## 从数论到Verve咖啡 0:50:21

洪乐潼高中毕业去美国读本科。她在草稿纸上写MIT，因为三个字母简单，哥伦比亚要写更长。她看《心灵捕手》，知道MIT的无限走廊。她对MIT信念感很强。本科数学和物理双学位。她肯定学数学，物理是后来选的。她对量子有兴趣，上过很多量子物理课，同时做概率研究。Scott Sheffield做随机曲面、几何概率，经常说某个东西在物理里有什么意义。她听多了，想学物理，了解那个意义。她小时候物理特别差，这是一个大胆决定。

她本科拿了很多荣誉，包括北美数学本科生最高荣誉摩根奖。她说这些奖项更像教授提名，不是坐在考场考试。她觉得自己是高产本科生，教授们友善，希望每个人好，给最好的建议和推荐。MIT数学环境不是竞争有限名额，每个人喜欢的数学不一样，喜欢这个领域就介绍你去这个教授。世界非常大。她讲疫情时中美航班停飞，教授们写信帮助mentee回来。

硕士去牛津读神经科学。她当时想知道人脑怎么构造，家里爷爷的事情让她想对大脑有更深理解。到了那里发现要对人脑有深理解需要做实验。她做过果蝇实验，撬开头盖骨，插管子看神经动态。在牛津要做动物实验需要考证，考证要杀一只老鼠。她做完那次实验，决定走计算神经科学，不做动物实验。英国的计算神经科学和AI关系紧密。UCL的Gatsby Institute由Hinton创办，Hassabis在那里做过博后。这个中心叫计算神经科学中心，实际上大部分faculty做AI。她跟Andrew Saxe等人做研究，见到Tim Behrens、Will Dorrell、James Whittington这些又懂数学又懂AI又懂神经科学的研究者，觉得非常激动。

她说自己被AI点燃，不是被神经科学点燃。硕士论文写continual learning的神经动态，还有一层线性Transformer的理论。大量线性代数、矩阵运算、ODE。她博士去斯坦福读数学和法学。数学博士是本科时defer的，本来打算本科后直接读。牛津是罗德奖学金的机会。她从小喜欢打辩论，牛津union有训练辩手的活动，法学院做诉讼相关实习，也来自辩论热情。

她讲美国宪法三种解释：originalism，按国父原意解释；textualism，按宪法英语字面读；living constitutionalism，宪法会呼吸，与时代一起成长。她自认是textualist。法学院有人说，想知道这些词是什么意思，可以拿语言模型喂数据，数据包括建国文献，也包括当代政治哲学著作。她当时想：如果AI能看宪法是什么意思，为什么不能拿AI做数学？法律需要精确结构，数学比英语更结构性。Lean把数学变成代码，这可能让AI做数学。

她最好的朋友之一Kenny Luo在帝国理工，交换到MIT，大一认识，教她下棋。Kenny从2020年开始做Lean形式化证明。那时mathlib空空如也，他和另外五到七个学生把本科代数、本科分析一行行打出来，做基础建设。洪乐潼看到这些，觉得一切认为不可能的事情都有可能。对她个人意义最大的是让AI帮助自己做数学证明。她不是天赋型选手，AI能帮助最大的人，可能正是蛮力型数学家。

她讲Ben Green的文章Cozy theorem for shifted primes。一个集合里a和b的差不是p加一或p减一，p是素数，从一到n能数出多大的集合。她看到这篇文章，想这套机器能证明多少数学问题。同样的工具可以做function field，可以做shifted sum of two squares。AI应该能达到一个熟练运用Davenport数论工具的博士生程度。她开始想怎么做，需要算力。那是2024年。

她和舒博在Palo Alto的Verve Coffee认识。她抱着厚厚的法律书去写作业，点一杯抹茶，看庭院里的狗。舒博坐在窗边，太阳晒，她需要拉窗帘，两人说上话。她不知道舒博是谁，舒博也不知道她。舒博本科和硕士学数学，后来在Meta，是Facebook AI Research的director，八九年的Meta元老，跟吴恩达在百度硅谷AI研究室做过早期AI，经历过GPU和scaling。两人聊了一年半科学史。2024年秋天，洪乐潼晨跑后觉得这件事真的要发生，去找舒博算要融多少钱、多少张卡，在餐巾纸上算。结论是得做创业公司。

她先融资再辍学，因为需要工作签证。她从2024年9月开始决定，但到11月才融资。她一直在劝自己不要做。她认为在valley，辍学创业某种程度上是浮躁。她向往学界，喜欢大学环境。她读科学史，从维基百科读到书。她找到一个AI for Math的GitHub repo，几百篇文章，每篇abstract都读，有意思的读全文。她做费曼式推演，在纸上想技术上怎么搭。她不想在自己觉得不会成功时去骗别人的钱。最后她判断，这件事不一定是个研究问题，更像工程问题，技术风险没有一开始看上去那么高。

她还去问过竞争对手招不招人。Verve咖啡的常客里有另一家AI for Math公司的CEO。她说自己想做的这件事，如果能跟别人一起做，也不用从零到一。对方问她是哪里的博士，她说数学，对方说只招计算机博士。她后来自己做了Axiom。团队分三块：AI、代码生成与编译器、数学。数学里有纯数学家Ken Ono、IMO教练艾文晨，也有做Lean和mathlib的人，还有做metaprogramming的人。有人拿Lean写了一个autograd。团队算上实习生有四五个IMO。她要求很强，因为这是工程问题。

## 最不可能创业的创业者 1:16:23

洪乐潼说自己是最不可能创业的创业者。MIT有创业社，好朋友是创业社社长，拉她去活动，说有免费寿司，她也不去。她觉得创业不好，还是想做教授。她认为产品导向的创业项目像昙花一现，她想做非常长时间、非常难的事情，这跟风险投资周期不一定吻合。她知道自已不是浮躁跟风的那一批。

她融资时讲得很保守。种子轮她说商业模式并不确定。她做过量化交易员，但不确定AI for Math是不是量化交易。她说一个数学比较好的AI大概率有用，这只是一个例子，不是第一个市场。她后来才知道，投资人见到的创业者通常讲得乐观，投资人心里会打折。你讲十分，他给你八分；你讲七分，可能打没了。

> 没有人喜欢融资。

她说融资难在累。你像复读机，一次一次说一样的事情，一次一次接到一样的问题。大量无聊过程里，有一些让人激动的谈话，通常是你最终选择的投资人。她印象深的是B Capital的Howard Morgan。Howard是文艺复兴的co-founder，和Jim Simons一起，也是First Round的联合创始人。他住在纽约，有时候去纽约大学上课。洪乐潼在MIT时，Jim Simons来过学校做两小时围炉谈话，她是本科数学社成员，去聊过。见到Howard，她激动。Howard比她更乐观，比她更觉得商业模式有前景。

种子轮融资从1月到3月，7月close。融了6400万美元，估值3亿美元，比预期高，预期5000万美元。她聊了几十个投资人。1月有一个领投愿意给term sheet，但要拿掉50%，她拒绝了。2月第二个offer更真，舒博在那时决定加入。3月B Capital的Howard Morgan效应出现，价格不错。她还在上课、考法学院考试、做rebuttal。A轮在2025年圣诞节出现preempt，投资人知道她不融资，没有PPT，没有材料，直接给term sheet，希望她尽快签。1月5日她被叫到外地城市pitch，当晚拿到offer。一个半星期后拿到第二个offer。最终A轮领投是Menlo Ventures，融了至少2亿美元，估值16亿美元。

她讲年轻创业者的难。扎克伯格19岁见Peter Thiel，Peter Thiel在餐馆拿term sheet说，这顿饭不吃完你不签，我现在撕掉。扎克伯格去洗手间哭了一场，回来签了，放弃其他竞拍机会。洪乐潼说年轻创业者大部分时候不知道自己的决定对不对。等更多信息可能让你更自信，不一定让决定更对或更错。等的过程高风险低收益，有时候不如直接跳下去。她参加女性创业者活动，在森林里玩zipline，第一次不敢下去，后面一群人等着，她闭眼咬牙下去。别人说希望她形成肌肉记忆，每天重复take the leap of faith。

她讲人才竞拍。AI人才手上六个offer，创业公司付不起一亿美元package，只能让利吃亏，每天让利吃亏，才能做出一家伟大公司。她讲Axiom像SpaceX，有很多技术壁垒。训练模型更高更快更强，但这个问题遇到的科技挑战时间会更长。种子轮时他们觉得R&D cycle会拖得很长。竞争对手比他们早开始两年，融的钱是他们的五倍，估值是五倍。对手用两年在IMO六道题里做出五道。Axiom四个月冲普特南，拿到满分，然后冲研究问题。很多研究问题由世界各地数学教授发给Ken Ono。以色列Technion的Lior Fell? 给Ken发邮件，波士顿的代数几何学家也发文章。他们在压缩时间，也欠下一些inference的债。

Ken Ono的邮件是转折。11月底，Ken给洪乐潼发邮件，说要去湾区，如果他加入OpenAI或DeepMind，希望她有心理准备。洪乐潼心想，你要加入OpenAI和DeepMind，为什么不来我这里？她回信说，你可以来我这里。Ken当时可能拿到OpenAI的offer。OpenAI的AI for Math部门可能和Axiom有战略竞争，Ken作为朋友不希望她突然听到消息。洪乐潼说，那来Axiom。两三天内谈定，截胡OpenAI。她认为Ken被团队更数学的氛围打动。OpenAI做数学的人不是特别多，Axiom的DNA和专注点就是数学，不是一个general AGI里数学作为marketing的一部分。

Ken Ono像高中篮球队教练，给所有人加油助威，让人兴致勃勃、乐观向上。他是数论学家，在划分函数领域很年轻就做出好成就，也是很好的研究导师。洪乐潼说Ken是理论建造者，能把不同领域连接起来，有全新视角看问题，发现好问题，给更善于解题的人去做。Ken的父亲是众筹给拉马努金修雕像的数学家之一，办公室里还有拉马努金遗孀写的信。Ken本科在芝加哥大学，高中没毕业，绩点不好，父亲拿拉马努金的故事勉励他，任何时候开始都不晚。Ken后来成为高产的猜想家。

2026年，美国出现一批Neo Labs。洪乐潼融资时还没有这个概念。2月DeepSeek出来，投资人对模型两个字恐慌，觉得模型不赚钱，不如consumer产品有moat。DeepSeek把价格拉得很低，commoditize了模型。洪乐潼说，大家没意识到Axiom不是模型公司，是deep tech公司，更像SpaceX。Lean有古老背景，来自program synthesis和program verification。Lean作为形式化语言，公开domain的tokens很小，数据少。Lean像C语言、GCC编译器和C runtime三者合一，很finicky，很多限制。要验证一个证明没有作弊，原来的comparator比Axiom自己的verify proof慢100倍。他们造了十二三个工具，辅助Lean生成和验证。AlphaProof用蒙特卡洛树搜索，他们觉得太贵，得找别的办法。他们的系统设计和字节Seed Proof有相似处。

## 数学天书与Lean 2:19:51

Axiom这个名字来自公理，也来自《数学天书中的证明》。洪乐潼小时候看这本书，想上帝有一本书，里面会有哪些题。公理和Lean呼应：从有限公理推导新结果，像有地基再建高楼。Axiom这个词很数学、很克制、很理性、很sharp。公司里名字开头是A的人特别多，Alex、Alberto、Arum，公司叫Axiom。

她认为AI会把数学历史推向新阶段。以前能做到顶尖数学思维的人很少，现在会从math pool到math rich，数学供给会爆炸。所有未解决的理论问题，所有应用科学家希望数学家帮忙解决的问题，全部可以解决。她预计会出现指数级的数学发现增长。数学家会扮演什么角色？她认为数学家提供最好的直觉，提供那百分之零点零一的直觉，判断哪些问题更值得集中算力。三四十个或十几二十个数学家聚在一起列wish list，讨论问题的重要性和连接性，解决这个能把哪些都解决。实际证明由AI数学家去做。如果算力有限，数学家就是资源分配者，200个H200花在这道题，8000个H200花在那道题。算力会成为数学问题重要性的某种等价物。如果算力无限，就像Demis Hassabis在Thinking Game纪录片里说蛋白质折叠，手下说做一个平台让生物学家提交蛋白，Demis把笔扔在桌上说fold everything，that was a stupid idea。无限算力下，要把所有人类好奇的数学问题全部解决。

她举中国剩余定理被MIT的Ila Fiete用在神经科学，研究多少神经元能叠起来，neural capacity。数论和理论神经科学产生关系。法律与经济文献里，Mitchell Polansky和Steven Shavell用微分方程想刑法多少用于威慑犯罪，多少用于惩罚个体。她在法学院帮算过很多微分方程。Tim Gowers说纯数学是生态系统，纯数学死了，应用数学也没了。数学到code到软件到R&D到实际验证。

数学和代码是孪生兄弟。Curry-Howard对应，每个数学证明可以变成一个计算机程序。Lean基于这个。代码是数学，因为后端和分布式系统很难像做网站那样web coding，缺少backtrack、缺少分层拆解，数学能给它。数学和编码是人类世界里有验证信号的一对。另一个验证信号是实际世界实验，扔鸡蛋，重力让鸡蛋碎，这是reward。Axiom的AGI worldview是数学、编程、实际reward testing，然后everything else。

普特南那天，2025年12月6日早上，Axiom收到考卷。第一件事是把题目形式化，让Axiom Prover做。早上6道，下午6道。证明题直接形式化，求解题还需要求解。所有人挤在庞加莱会议室，war room。数学家解题，人类解法和AI解法完全不一样。下午3点58分，他们发现已有8道题，80分。80分在当年是世界前五，往年可能前十前二十。他们希望拿90分。当时有一个选择：是否告诉世界。最终12道题全部满分。Ken Ono在解题时说，现在不是数学纯粹之美的时刻，是战争状态，能怎么快捷就怎么快捷。求解题把数喂进Axiom Prover，和IMO标准一样。后来发现，Axiom系统里有informal模型，可以直接给出解法，并不需要人类先求解。他们以为要求解，其实不用。

AI for Math的技术范式在收敛。拿开源模型做后训练，有人直接RL，有人SFT再RL。做好模型放进系统，系统里有各种模型，有些做specialized任务，call tools。Tools难做，需要大量Lean metaprogramming。Axiom和Seed Prover、Hilbert Prover做法类似，Aristotle和AlphaProof以前的做法类似。大致两派。他们招做后训练、强化学习、reasoning的人，也招agent、swarm of agents的人，full stack engineering很需要。

AI for Math突破后会有泛化性。洪乐潼说核心科技叫proving，但一整套东西包括prover、conjecture、知识库、autoformalization。证明模型有reward，证出来是一，没证出来是零。猜想模型难在没有reward，怎么判断猜想好不好。可以拿prover做grounding，给猜想信号，还需要elegance filter判断猜想是否优雅。Self-play improver那篇文章用长度判断优雅，题目比证明长还是短。这个在Lean Workbook高中数学数据上可行，到本科、博士研究不够。猜想和证明要通过聊天自我提升。知识库很重要，大部分英语或中文里的数学，Lean里连定义都没有。需要搜索已知、已证明、需要证明的东西，找到反例直接证伪。还需要把浩如烟海的数学转成形式化数据，这叫autoformalization。

Autoformalization被忽略。证明普特南或IMO题可以上推特说自己是伟大AI数学家，把人类已发现的数学转成形式化，得到更少赞美，但难度至少一样，洪乐潼认为更难。输入是arXiv数学文章，输出是文章里所有定理和证明变成Lean代码。第一步拆分定理和证明。有些文章结构好拆，有些大证明能拆出很多。拆得够细叫blueprint。陶哲轩、Kevin Buzzard、Alex Kontorovich这些数学家手写蓝图，放到PolyMath和大型形式化项目，丢给全世界本科数学学生，每人领小任务，星星之火可以燎原。让计算机从PDF到几百页蓝图，再把蓝图转成Lean，需要很强的分解推理能力。这个岛屿上有证明家、猜想家、知识库、转化能力，贯穿始终。

形式化语言像Python，有执行能力，跑完看到勾或报错。哲学上数学是英语的子集。数学词汇在英语里的distribution和日常英语不一样。代数几何里的germ，英语意思是细菌，疫情期间学代数几何，大家拿germ开玩笑。让AI在英语里做数学不是全貌。转成代码，有可验证性，更有道理。Lean有兄弟姐妹：HOL、Rocq、Isabelle、SMT。全世界芯片验证基本用Cadence的Jasper，基于SMT，有很多局限。如果全世界挣扎的SMT都被Lean代替，世界会怎样？Lean和Python的关系，Lean可以作为Python程序的验证。

张小珺问，用math作为手段和用coding作为手段执行任务的区别。洪乐潼说互补。Coding帮你算出output，数学帮你验证property。给一个问题，coding给你程序，你需要知道程序对不对，需要很多输入输出test cases。如果test cases不需要，写的时候直接验证程序真正解决了问题，这是全新的世界。难点在specification。任何你能定义的，你都能证明；任何你能specify的，你都能执行。Software verification的布局是program乘以specification，映射到verification condition乘以proof。Axiom做proof部分。现在AI能写很多程序，specification成了难点。数学里猜想难，定义与猜想是难点。First Proof十道题，OpenAI做5道，DeepMind做6道，都是自然语言。Axiom没法参加，因为十道题没法转成Lean，题目涉及的定义不在mathlib里。无法定义，就无法证明。

> 任何你能定义的，你都能证明。

验证是Axiom的第一个市场。亚马逊有世界上最好的自动推理团队之一，没有AI，纯人，花3到5年写了26万行定理证明代码，验证一个用于优化CPU处理的hypervisor的memory isolation component。AI没有改善这些工程师的生活。芯片验证领域痛点大，pricing power更好。更广的市场是每个人都要coding，verify generation会变重要。你要一个函数，AI给你100%不需要验证的函数。洪乐潼说，他们更关注系统不能做什么，解决一个有意义的失败比很多个肤浅的成功更有价值。

数学是语言模型的拐杖吗？洪乐潼说，把数学当语言来做拐杖不对。要把数学变成Lean，它会是另一个更重要的拐杖。数学和语言平行。有些问题更适合语言，比如列提纲，提纲是很大一部分胜利。有些更适合在形式化空间证明。形式化做得很好的模型系统，在芯片验证上比更偏语言的系统更好。通用代码生成需要语言，因为要理解用户无法表述清楚的需求。把语言部分和Lean部分放在一起最有意思。Axiom基于大语言模型，系统里不同模型经过后训练，以数学为主，以Lean为主，输出都是Lean代码，Lean代码自带验证性质。

她讲一个场景：你完全不懂密码学，别人写一篇密码学文章，有数学符号，你看不懂，不知道对不对。文章可以通过Axiom Prover变成Lean，你不需要看懂，跑一下，看到勾，就知道文章是对的。人们盲目接受强大AI会犯错误，但在一些领域，错误会极度昂贵。Axiom想做一个尽量perfect的AI。它能帮助解决幻觉。两种情况：要么说太难做不到，要么给正确的东西。语言突破边界，数学往回收，约束它。好直觉是幻觉和规律推导的配比。语言擅长conjecture，帮你想新东西；verification验证，来回循环。Francois Charton和Alberto Avareno做数学发现，通过找数学对象、例子、反例，扰动图，找直觉，再变成猜想。证明和语言、形式化都相关。

## 数学家的直觉与登月 3:09:59

Axiom接下来要往前走。他们解决了一些研究问题，交换代数、代数几何、代数数论、组合概率。接下来选目前没什么定义的领域，动力系统、概率和随机曲面。想知道没有基础建设的地方能不能解决问题，前沿到底在哪里。他们两个月把高中基准miniF2F打饱和，然后普特南，然后代码验证基准。研究级数学缺benchmark，题不好找，只能在每个领域找两三个未解决问题试一试。接下来从工程往研究转，解决光靠工程摘不下来的low-hanging fruit。

数学家的意义很大程度在出题。机器出题目前很差，猜想家表现糟糕。出题非常难。到哪里找800道未解研究题？一个教授有题，给你还是给他的学生？这是复杂过程。Axiom希望通过数学家网络，看谁愿意给AI试一试。他们希望系统robust to distribution shift，不能只做欧式几何，否则就是几何引擎。要能做更多领域，尤其是没有基础定义的领域。代数数论很多东西在mathlib里定义好了，容易写命题。动力系统、高级组合没有定义，题都写不出来。这就是First Proof十道题的挑战。AI写定义的能力叫library learning。让机器搭图书馆，从定义到定理到证明到衍生新定理，加更多定义。这很难。定义没有验证信号，没法说对错。还要求faithful，和人类已创造的定义相同。如果系统引入人类没写过的新定义让生活更容易，怎么保证定义不相违背？可以定义好图，过一会儿出现悖论。这些是较远的研究问题。

洪乐潼不喜欢AGI这个词。她说Axiom更可能做ASI，specialized super intelligence。数学不一定那么general，不一定带来泛化。她讲一个盘子比喻，和任宏宇聊过。中间是一个点，1+1=2，打印hello world，所有简单任务。盘子外缘是证明黎曼猜想、找出治疗癌症秘方、写出莎士比亚或诺贝尔文学奖著作，所有超人类任务。OpenAI这类frontier lab想一点一点把圆环撑大，最终接触所有边界。Axiom从中间往证明黎曼猜想这个数学超人类任务打，打完发散出一个扇形，可能有代码验证、物理，不会覆盖到诺贝尔文学奖，但扇形足够大，在B2B市场有意义。这是ASI。

AGI和ASI的区别，她认为ASI是specialized super intelligence。super intelligence就应该是specialized。她自嘲数学还可以，但不会做饭洗衣服，人类智能也不一定多general。AGI实现得很好，会不会取代她？她说有可能，但自己会更快。强化学习在coding上已经take off。code verification是很重要一环。有数学做algorithm的能力，有猜想，就能recursive self improvement，持续螺旋上升。她希望一个世界有AI scientist、AI engineer，Axiom一定是其中一环，不是整个生态系统。

AI for Math的尽头，她认为能带来两样东西：非常smart，非常right。超人类表现，OpenAI也能做AI for Math；grounding，100%正确。两个象限往上推。Axiom的DNA是数学，验证是第一个市场，未来可能有AI for Science，所有科学需要的理论发现；还可能有optimization。很多世界不是diminishing return的反面，是沉默性付出成本的反面。花很多力气，最后那一个mile收益非常大。搜索引擎覆盖所有edge case，Google赢得搜索市场。文艺工作者好和非常好的区别天差地别。验证边缘情况耗费很多钱和人力，大家花很多工业界资源探索小数点后一千位，比起小数点后第三位。有些情境第三位更有意义，但既需要median又需要outlier。数学给了这种DNA。

Axiom既要数学家，也要代码生成的人，很多编译器、代码生成同学。洪乐潼相信多元产生智能，也相信降维打击。AI for Math探索推理的非常难的问题。你有爬虫数据，通过pattern找规律很难撞墙。数学Lean数据少，动不动遇到拦路虎，hit roadblock更快。做更难的事情，垂直下来给其他领域降维打击。Axiom Prover能生成20页数学证明，也能很快验证芯片验证领域的复杂puzzle。芯片需要的是高中数学学生或初中数学学生会枚举、分类讨论，不是numerical semigroup。三个背景的人联合起来有很多想法。AI和编译器背景的人做synthetic data generation，拿AI生成Lean data，不靠人打Lean。数据商可能整个平台25个专家，打得还不怎么样，没法大规模做。需要AI做，需要代码生成，用forcing、repair、failure categorize。AI和数学可以正向推理、反向推理，forward and backward conjecturing，像早期棋类expert system。Axiom是idea rich的公司，人不够执行。12月Ken加入是第15号员工，现在30人。竞争对手50到75人，比他们大。

数学是现实世界的沙盒。既有验证信号，又有规律性描述、结构性数据。生活里想一个猜想再证明，只能想到数学猜想和数学证明。猜想生物的东西，要去实验室做动物实验。与现实世界有关的验证过程比数学沙盒困难和复杂。洪乐潼尊重做AI for Science的朋友，Periodic Labs、Lila Sciences、Edison。如果想很快验证，又希望能计算又有逻辑，数学和代码是好选项。AI for Science和AI for Math不是一个重叠赛道。AI for Science很多在比iteration cycle多快，有wet lab、机器人实验室，前期投入很多。Axiom停留在数字世界，不走到实际世界。Axiom可以帮AI for Science验证理论问题，也可以帮大语言模型验证代码，减少幻觉。

不走形式化证明，可能尝试通用推理。AI for Math有一天像天才数学家提出好问题、有好直觉、成为创造的人吗？洪乐潼说这是最难的部分。Axiom打算做，竞争对手不太打算，他们好像直接要商业化，觉得IMO金牌是终局。Axiom希望把猜想做出来，有很多试验，也碰了一鼻子灰。失败时证明家还做得不太好，分不清哪块出问题。做猜想之前，希望把autoformalization做好。能做好转化，既能拿更多数据，又能帮助证明，然后才做猜想。现在做一点，没有整个公司打猜想。猜想是数学最有魅力的地方。洪乐潼很难提一个好猜想，给大一学生做reading course最终题也很难。猜想需要很强的数学能力。Ken Ono是高产猜想家。

Ken Ono和拉马努金的关系，两个故事。一个是他父亲参与众筹给拉马努金修雕像，拉马努金遗孀给世界各地数学家写信，父亲回信，办公室有那封信。另一个是Ken本科在芝加哥大学，社团活动多，课业不占全部时间，绩点不好，高中没毕业，非常叛逆。父亲拿拉马努金故事勉励他，任何时候开始都不晚，不需要像同学上了多少数学课才能做数学。Ken进入博士项目后非常努力，做了很多数论研究。Ken的父亲去年年底去世。Ken的兄弟，一个是著名提琴家，一个是密歇根大学前校长。拉马努金是更尖锐的直觉型解题型，Ken擅长连接不同视角提出猜想，发散型思维。

拉马努金那种浑然天成的直觉，可能是预训练的产物。Essential AI训练了一个模型叫Ramanujan。洪乐潼说，他们现在主要做后训练，有一天可能做中训练。拉马努金不一定能通过后训练诞生。拉马努金到剑桥后接触证明，知道如何写证明，数学影响指数级爆炸。更多直觉可以证明，变成新直觉。AI可以训练证明，对直觉有帮助。Ken Ono肯定不是预训练产物。预训练有大量基于数据的研究方向，大家没在做。Axiom不做预训练，太费钱，大部分Lean东西可以从后训练来，可能做mid training。一些基本能力需要预训练、中训练提出。

大厂为什么做AI for Math？OpenAI走informal，是Kevin的个人科学雄心，要做科学发现。DeepMind有几个队伍竞争，一个formal，一个informal。xAI不确定。Anthropic有，但作为提高推理效果，把数学题informal变formal，Lean验证完再回来提升推理分数，没有作为专注点。如果洪乐潼是大厂玩家，不一定会做Axiom这件事。同样高密度人才可以继续做代码生成或更红海领域，把护城河筑起来，然后和创业公司合作。OpenAI在搜索会call Exa或Parallel。AI for Math不是蓝海，比较难。机器人foundation model有Physical Intelligence和Skild，AI for Math创业公司主要是Axiom和竞争对手两家，估值差不多，融资差不多，一个更新，一个早两年。

洪乐潼的挑战是执行速度和学习速度。执行越多，学习时间越少。她以前每天有阅读时间，现在少了，又有那么多事情需要执行。这是挣扎。其他科技人才也有research和engineering ratio的trade off。公司成立七个月，A轮后期待大。怕执行不够快，也怕为了快导致焦虑，战略出错。AI for Math终点和成为成功商业公司哪个更重要？她说作为founder对员工和早期团队有责任，这不是纯科学项目，必须成为能长期存在的企业。公司DNA是登月。她喜欢“温社”这个名字？她非常喜欢，觉得名字太好。太逐利商业化会失衡。竞争对手起源是Robinhood的founder CEO，可能还全职在Robinhood，希望有另一个有激情的项目，早期更讲科学雄心。理想现实主义者和现实理想主义者都不错，不能太远。

> 要么登月成功了，要么登月失败。

公司结果一定极好或极坏，没有中间可能性。像SpaceX，要么火箭发上去，要么坠毁。火箭可能坠毁几次才发上去，每次都差一点。马斯克早期锐意进取，值得学习。好几次公司只能两个留一个，他坚定说both，鱼与熊掌都要兼得。Tesla和SpaceX都这样。洪乐潼也认同。如果失败，她去干嘛？她可能当数学家，也可能做神经科学相关，brain and machine interface。她那一年的神经科学心得是，人类基本不理解人脑。她可能希望做人机交互，目前implementation都不够理想。

硅谷模型公司竞争，洪乐潼前几天和xAI朋友聊。为什么她最后不想做量化交易员？赢与输短期内决定。她引用Peter Thiel，垄断导致创新，竞争导致平庸。竞争会让有长远想法的人出来做Neo Labs。Neo Labs产生，因为好奇心和创造力是人类基本需求。前沿大公司无法满足burning passion，人就出来。假设Axiom Prover非常成功，所有数学题包括千禧年问题都解决，还会有数学家吗？洪乐潼答案是一定有。给你100万行Lean代码，一定要看里面怎么做出来。不让我看，我也会看。这是人类好奇心。看懂证明的数学家又会有新猜想、新想法。AI做发现，让数学家更好发明。好奇心和探索愿望无法被压制。一亿美元大包也压制不住青年研究者好奇心。Stefano Ermon做diffusion model更快更好推理模型，Periodic做material science，不怕messy data，Recursive做AI与硬件互相提升。背后基本作用力是好奇心。

现在是不是泡沫？有些公司成了，就是登月；有些公司很努力，每天九九六朝梦想努力，结果没成，就是泡沫。洪乐潼希望环境像好学校，不怕失败。MIT有一门课learning to fail，如何更好地失败。每个登月项目失败都会在资本市场掀起涟漪，从私有市场到公开市场有连锁反应。有人会说不负责任，pension fund的退休资金通过好几层投资到私有市场，给有想法的研究者满足好奇心。洪乐潼觉得很公平的问题。研究者如果受使命驱动，放下虚荣心、占山为王和ego，带着不同背景、技能、对同一个理想的解读聚起来，朝一个目标努力，减少碎片化的重复尝试，他认为这样的尝试比较legit。

Neo Labs有不同信仰和beliefs。遇到OpenAI、DeepMind竞争怎么办？洪乐潼说，结构性问题是，如果大公司需要一个单位创新需要多少单位资源，早期创业公司效率非常高。Axiom做的事情在另一个环境更难达成，这是许多人从Facebook来Axiom的原因。第二，作为underdog，除了效率和人才密度，没有资源和大玩家抗衡。有意思的是，OpenAI曾经也是对着Google的黑马，Google要counter offer抢Ilya时焦头烂额，OpenAI也一度发不出工资。历史钟摆来回摆动，螺旋上升，又有local扰动。There is always a way，你得信。信的人可能是喜欢加入早期创业公司的人。Humans &最近融了很多，co-founder是Google第七号员工，到了人生阶段仍认为好奇心是最珍贵的东西，值得倾家荡产。

洪乐潼和谢赛宁聊过，有些Neo Labs甚至anti硅谷，反感红海竞争阉割研究员创造性。洪乐潼看宏观局面：竞争让能力飞速上涨，好的且能快速验证的东西被scale up，一些需要更长时间的东西没有被实现，这是机会成本。竞争不能说不好，它让AI在很短时间内达到很高进步速度。她的自我奖励机制从团队变成事情。团队给安全感，让你grounded，脚还在地上。让你break out的冲动能量，可能是愤怒、悲伤、卯着一口劲，来自事情本身。最burning的终点是莱布尼茨的universal representation theory，所有你能表示的东西都能表示。她期待推理能力成为最顶尖的默认状态，且能自我验证。

人一辈子能剩下什么？有些数学家一辈子解决一个非常困难的问题，人们因为这个问题记住他，墓碑上写着他解决了这个问题。伽罗瓦21岁决斗去世，拉马努金三十几岁因营养不良和疾病去世。人类要多少人出一个伽罗瓦、一个拉马努金。如果用AI复现这样的数学家，又有那么多已存在的数学家与他互动，会产生新的东西。这是Jevons Paradox，工具更便利更普遍，会有更多用处。洪乐潼公司第一次找了一个处理日常杂事的同事，杂事反而更多。科学家与AI伽罗瓦、所有数学家总和互动，能有多少科学理论、基础数学被发明发现？从算盘到会计师，从微积分到物理、力学、热力学、工业革命，从Babbage engine到电脑前身。哈代写《一个数学家的辩白》，说数学没有实际价值，后来密码学有了。Victor Miller，椭圆曲线密码学泰斗之一，纯数学背景，在CS看了一眼，看出理论对计算机同学有很大价值。这是终局。终局之后钟摆又会摆。AI for Math没有像AI模型被scale up一样被scale up，Axiom希望做这样的公司，知道天花板在哪，再回到research，钟摆来回摆动。

00后女生做CEO，和70后、80后、90后CEO有什么不同？洪乐潼最快乐的状态是research scientist intern。说错话大家认为正常。她真的想做研究，如果有另一个很明显可以加入的地方，她会加入，不会单独创业。她不想当创业者。有一次她突发奇想做博士级benchmark，找办公室有数学背景的同学分领域找二三十题。一个元老工程师说，你让实习生和年轻工程师觉得这是非常重要任务，和优先级相斥。她说这不就是一个side hobby project吗？工程师说，你是CEO，你讲的时候他们会当成正儿八经的事，当作前几件事去做。从那以后她更hands off。她认为CEO好处是技术rule的公司，技术人员是主干、定向和锚点。她没有strongly held beliefs，很多ideas可以bottoms up。公司文化像Pixar梦工厂。梦工厂CEO如果是一个拍过很多好莱坞电影的导演，这个地方成不了梦工厂，因为大家觉得这个人是对的，应该听他的。bottoms up对创新最好。她愿意给Axiom当intern。

会议室用数学家命名：高斯、庞加莱、希尔伯特、Lovelace、图灵。大家差点打起来，因为喜欢的数学家不一样。有人说有了图灵没有Church，不行；有了Lovelace没有Noether，不行。世界各地邮件问为什么不把Emmy Noether做会议室。他们只有五个会议室。最后选polymath，庞加莱、希尔伯特、高斯不只一个领域。拉马努金落选，因为他只会数论。Axiom希望AI数学家什么领域都会，没有distribution shift。图灵跨世纪，舒博lie his body on the table，说如果不给一个叫图灵，我就走了。洪乐潼说行行行，图灵。女数学家选Lovelace，她在Babbage engine也有贡献。洪乐潼的偶像是高斯。高斯是解题天才，正十七边形尺规作图，数论贡献fundamental，二次互反律，初等数论里好多高斯。高斯是年轻数学小王子。

如果可以穿越时空和历史上任何一个数学家共进晚餐，洪乐潼选Erdős。组合学在餐桌上能听懂，Erdős性格古怪有趣，古灵精怪。另一个选Grothendieck，但洪乐潼代数几何学得不好，跟Grothendieck吃饭容易浪费机会。数学家是有趣的人。AI for Math做到所有数学家能做的事情，会不会无聊？洪乐潼想过。数学家之间的友谊、合作关系、文化社区很有意思。数学家生日，大家办峰会，学生、合作者轮流讲这个人的数学贡献，或合作的一篇文章。她作为硕士生在牛津参加过Heisuke Hironaka的生日峰会，Ben Green、James Maynard都在，她很感动。人的元素在数学中永远不会磨灭。AI会帮数学家快速解决很多证明，猜想、直觉、构造仍有非常多乐趣，数学家会成为智力灯塔。数学家珍贵的legacy会有更多问题难倒AI，像他们已经在难倒AI一样做基准，永远是智力挑战。拉马努金和验证AI，偏验证，不是天才型。直觉太难做，可能5到10年。洪乐潼有激进想法：解析数论里很多问题被一遍又一遍用标准证明方法抽牌，major arc、minor arc、Hardy-Littlewood圆法、筛法。有些人自己不解决问题，在提升筛法工具。已有工具能解决很多问题。一个人直觉好，可能是很快想到怎么重复运用这些工具。她说的直觉是给大家一个完全不同的方法和机制，这个可能5到10年。

她16岁写过文章，说热爱数学就是看到了上帝的面容。她小时候觉得有一些基本真理，数学家、科学家存在的意义之一就是发现和探索。创业后晨跑，斯坦福Memorial Church，平常绕着跑因为晒，那天往草坪底下跑，到了教堂下面，阳光很好，教堂有壁画、天使、十字架，有一点spiritual的感觉。她想，如果一个人的木质碑上印着他曾证明的事情，是智力遗产，让这个东西乘以一亿，你会不做吗？可能不会。这是出于ego的想法，希望Axiom成为AI for Math的unlock，希望登月的是他们。这是自私的雄心壮志，但总体上希望它实现。就算Axiom失败，其他人登上去也是好事。木质碑上写什么？她说体验比较重要，活过了，有体验，木质碑不重要。曾经觉得成为数学家很重要，想到可能没法成为数学家，有时候还哭。后来觉得想当学徒。非写一个就写学徒，想在尽量多智力领域尽量多学东西。数学、物理、神经科学、AI、量化交易、法律。反垄断像树状逻辑，非常像数学；合同法也像；宪法完全不像数学；民事诉讼、庭审是讲故事。她希望学很多。AI for Math最快乐的时候，是找到GitHub的Lean链接，把文章abstract全读一遍。那几个月最快乐，舒博跟她一起读，现在一起做。那些作者陆续加入Axiom。前三十篇AI for Math文章，大部分作者在Axiom，每天一起冲目标。现在是“怎么让创业公司不死”的学徒。99%创业公司会死，她是Don't Die的学徒。

团队和事情冲突过，开过实习生。任何乐观主义收起来，谨慎做决定，想很久，要对人负责。很多时候人与事冲突，是自己不够好。走到冲突那一刻，一定因为自己做过错误决定。就算是不认识的员工，也有管理层决策一步步trickle down。她相信authorship，你是自己人生篇章的书写者、合作者。不能觉得情境决定你的决定，是你决定让情境决定你的决定。你也可以决定用其他方法让情境不这么糟。

人生之书，数学书推荐初等数论，对数论讲得很好；Davenport的分析数论。非数学书喜欢《红楼梦》，小时候震动很大；《比我老的老头》影响大。企业家故事，马斯克晚上睡不着，痛苦咆哮；黄仁勋讲pain and suffering。看到这些故事，嚼玻璃的日子会觉得正常。训AI和训自己像不像？看到AI表现好一点，马上给更难题，curriculum sampling。看它做blue force，跟自己曾经做数学家的感受有点像。假设Axiom的AI证明重大猜想，使用一个不在现有数学里的新公理，看起来合理，接受吗？洪乐潼说，数学家会觉得世界末日。AI尝试奇怪公理作弊已经发生。DeepSeek Prover曾宣称在Putnam基准做出来49道，实际47道，两道作弊。如果公理大家觉得自然，就会接受。可能是以前没探索足够的数学领域。存在即合理，公理可能已被假设。未来可能有混合领域的数学，大家往里加东西，接受和不接受两个世界照样运作。branching factor现在是2，继续会有无限多个世界，一团混乱，有一天大家可能回收、Titan。数学是人类文明构造，比物理加定律更可接受。

中国AI发展，洪乐潼respect豆包、Seed，做得非常好，团队执行力强，跟