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

Overview

Shownote

Highlights

Transcript

Chapters

Pins

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

张小珺Jùn｜商业访谈录

Apr 20
张小珺Jùn｜商业访谈录

张小珺Jùn｜商业访谈录

Apr 20
OverviewShownoteHighlightsTranscriptChaptersPins

Shownote

2026 年，美国诞生了一系列的 Neo Labs（新型研究室）。Neo Labs 是近年兴起的一个新概念，专指由顶级 AI 研究者创立、以基础模型或新一代智能体系为目标、融资规模巨大、研究导向很强的一类新型 AI 实验室。我们 133 集的嘉宾，来自 AMI Labs 的谢赛宁是，今天我们邀请的是另外一位。 她是《商业访谈录》至今最年轻的一位嘉宾，是一位 00 后华人女孩，网络空间有人会叫她 “数学少女”—— 她的名字是洪乐潼 Carina，这是她第一次接受中文访谈。 她探索的方向是 AI for Math，所创办的公司 Axiom（公...

Highlights

本期节目聚焦一位 00 后华人女性创业者洪乐潼，她以数学为原点，闯入 AI 前沿阵地，创办专注 AI for Math 的公司 Axiom。这不是一场关于技术堆砌的讲述，而是一次对数学本质、人类直觉与机器推理边界的深度叩问。
00:11
57 岁美国终身教授辞职为洪乐潼打工
11:52
AI 在普特南竞赛中用几千行 Lean 代码获满分，是人类历史上第六个满分
14:39
自由注意力能区分普通创业者和有策略决策能力的创业者
42:19
失败不是例外，而是默认状态
59:54
本科时就打算读数学博士，因罗德小学期去了牛津，且因从小喜欢辩论，参与了 Oxford Union 的活动
1:06:50
AI 应能熟练运用数论工具，达到博士生水平
1:28:51
团队早期定下‘不招到 15 人不招数学家’的规则，因种子轮资金有限且需思想开放、敢于对抗的数学家
1:58:39
团队四个月获普特南满分，六个月实现自动形式化证明系统里程碑
2:17:24
AI 不会替代数学家，人类将在更高抽象层面进行逻辑推理，与 AI 协同实现猜想与证明的相互促进
2:19:54
团队在普特南竞赛当天实现 12 道题全对，人类与 AI 协同完成形式化建模与解题
2:46:20
将人类已有的数学转化为形式化内容虽难却获赞少
3:05:48
强大的 AI 虽会犯错，但可通过 Axiom Prover 转化为 Lean 进行密码学文章验证
3:16:16
AI for Math 既能带来超人类表现，又能保证百分百正确，是公司的 DNA
3:26:19
AI for Math 的核心目标是像天才数学家一样提出好问题、拥有好直觉，而猜想生成是其中最难也最具魅力的部分
4:00:48
数学家间的友谊、合作关系和文化社区等元素永远不会被磨灭

Chapters

AI for Math 的突破与创业奇迹
00:00
被创造的与被发现的
02:14
bounded vs free attention
14:38
对苦难上瘾
32:14
数论多美啊!
50:21
Verve Coffee
1:02:26
最不可能创业的创业者
1:16:23
没有人喜欢融资
1:38:33
小野肯的邮件
2:07:17
数学天书中的证明
2:19:51
Al for Math
2:24:38
把数学变成 Lean
3:03:50
数学家的直觉
3:09:59
登月要么成功，要么失败
3:26:18
与数学家共进晚餐
3:54:17

Transcript

洪乐潼: Hello，大家好。 张小珺: 我是张小珺。今天我们来到了美国硅谷，此刻正在扎克伯格最早的创业所在地 Facebook House。这是一栋外表为淡蓝色的可爱的小房子。而今天也将迎来商业访谈录最年轻的一位嘉宾，她是一位 00 后的华人女孩，名字叫洪乐潼。她的探索方向是 AI。format。所创办的公司 Axiom 刚刚完成了估值为 16 亿美元的 A 轮融资。而它引起了很多人的关注。这来自于这样一条新闻，57 岁的美国终身教授突然辞职，去给 24 岁的华人女孩打工。那接下来就是我对洪乐潼的访谈。 ...
小宇宙
Open in 小宇宙