137. 对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书的证明、直觉、被创造与被发现的
播客收听
问这期播客
会先在本集摘要、章节、转录和笔记里找答案。
本集要点
- 洪乐潼创办的Axiom聚焦AI for Math，已完成2亿美元A轮融资，估值16亿美元。
- 项目核心是将数学证明转化为Lean等证明助手可验证的形式，提升严谨性与自动化。
- 访谈强调数学是被发现而非被创造，并讨论数学家直觉与AI协作的可能性。
节目简介
00后华人创业者洪乐潼创立AI for Math公司Axiom，获2亿美元融资，探讨用Lean形式化数学及AI辅助证明。
章节
- 02:14
被创造的与被发现的
被创造的与被发现的
- 14:38
bounded vs free attention
bounded vs free attention
- 32:14
对苦难上瘾
对苦难上瘾
- 50:21
数论多美啊!
数论多美啊!
- 1:02:26
Verve Coffee
Verve Coffee
- 1:16:23
最不可能创业的创业者
最不可能创业的创业者
- 1:38:33
没有人喜欢融资
没有人喜欢融资
- 2:07:17
小野肯的邮件
小野肯的邮件
- 2:19:51
数学天书中的证明
数学天书中的证明
- 2:24:38
Al for Math
Al for Math
- 3:03:50
把数学变成Lean
把数学变成Lean
- 3:09:59
数学家的直觉
数学家的直觉
转录
被创造的与被发现的
bounded vs free attention
对苦难上瘾
数论多美啊!
Verve Coffee
最不可能创业的创业者
没有人喜欢融资
小野肯的邮件
数学天书中的证明
Al for Math
把数学变成Lean
数学家的直觉
登月要么成功，要么失败
与数学家共进晚餐
节目笔记
2026年，美国诞生了一系列的Neo Labs（新型研究室）。Neo Labs是近年兴起的一个新概念，专指由顶级AI研究者创立、以基础模型或新一代智能体系为目标、融资规模巨大、研究导向很强的一类新型AI实验室。我们133集的嘉宾，来自AMI Labs的谢赛宁是，今天我们邀请的是另外一位。
**她是《商业访谈录》至今最年轻的一位嘉宾，是一位00后华人女孩，网络空间有人会叫她“数学少女”——她的名字是洪乐潼Carina，这是她第一次接受中文访谈。**
她探索的方向是AI for Math，所创办的公司Axiom（公理）刚完成2亿美元的A轮融资，估值16亿美金。
而她引起很多人的关注，来自于这样一条新闻：57岁美国终身教授小野肯（Ken Ono）突然辞职，去给24岁的华人女孩打工。
**我们谈论了许多数学与美、被创造的与被发现的数学、数学天书中的证明与公理、最不可能的创业者的创业旅途，当然还有AI for Math。**
接下来，是我对洪乐潼的访谈。
**OUTLINE:**
00:02:14 被创造的与被发现的
00:14:38 bounded vs free attention
00:32:14 对苦难上瘾
00:50:21 数论多美啊!
01:02:26 Verve Coffee
01:16:23 最不可能创业的创业者
01:38:33 没有人喜欢融资
02:07:17 小野肯的邮件
02:19:51 数学天书中的证明
02:24:38 Al for Math
03:03:50 把数学变成Lean
03:09:59 数学家的直觉
03:26:18 登月要么成功，要么失败
03:54:17 与数学家共进晚餐
**LINKS：**
我们的播客在小宇宙、Apple Podcast、Spotify等全音频平台播出；
我们的视频播客在Bilibili、小红书、视频号、抖音等全视频平台播出；
如果你想服用文字版，请搜索我们工作室的公众号：语言即世界language is world。
**DISCLAIMER:**本内容不作为投资建议。
**CONTACT:**[xiaojunzhang@lisw.ai](mailto:xiaojunzhang@lisw.ai)
**Jump into the new world-and explore with us!**😉