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

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

264分钟 ·2个月前

42574

135

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

Jump into the new world-and explore with us!😉

展开Show Notes

狂野时代的小熊

2026.4.20

好喜欢这期啊！好喜欢！

生而为猫奴

2026.4.20

感觉她的脑子转得好快啊！她的表达的速度跟不上她脑子转的速度，各种跳跃🥹

孙骏_fhJf:是的，而且我感觉有些回答她是嵌套的，像编程一样，她自己能再一层层回来，不都是发散的，她的大脑可以做长线程思考（做N行代数解题的训练结果？）

生而为猫奴:对对对，太会形容了🥹就是这种在一长段发言当中，看起来越跳越远，回头一听发现都一层层收回到主线

Dec_3

2026.4.21

我很喜欢这期，很有生活、人味的一起，听乐潼的描述能代入到她的经历中，很容易找到彼此的共通点。
让我想到之前罗永浩和李想的那期访谈，很精彩。

Vera超幸运

2026.4.20

终于有AI行业的女生采访了！

-竹木-

2026.4.21

2:04:04 2:04:03 哈哈哈哈GCC compiler和C runtime 二者合一这个类比不是很适合解释为什么Lean能检查证明。我来尝试科普下Lean。
- 作为一个编程语言，Lean最酷的特色是你可以在里面写证明，然后它自动会验证证明对不对。同时你也可以把它当普通的编程语言用它来写可以跑的代码。
- 自动验证证明的关键是“类型”（Types）。
- 类型在很多编程语言里面都至关重要，比如在Java里，int count = 10 意味着count是整数10，char grade = ‘A’意味着grade是字符“A”，一个输入count输出grade的函数它的类型就是 int -> char。这儿的整数int、字符char和函数int -> char 都是类型。
- 在Java里变量的类型都要程序员自己写明白，编译器会自动检查你给这个变量的值是不是你说的这个类型。（在另外一些语言(比如Rust和C++)，有时候你不需要自己写明白，后台（编译器）会自动推断。）
- Lean允许用户自己定义类型，而且可以定义的特别具体，不仅整数可以是一个类型，“大于4的整数”也可以是一个类型，“正好为5的整数”也可以是一个类型，”当收到一个为n的整数时长度为n的向量“也可以是一个类型，… 它允许你把想证明的定理写成一个类型，根据Curry-Howard同构（理论计算就里一个不是很复杂但特别美的观察），如果你能写出一段恰好是这个类型的的代码，这段代码就可以被翻译成这个定理的证明！所以编译器里自动检查类型的方法也可以用来检查一个定理是不是被正确地证明了。
- 我不知道嘉宾说的Lean finicky有各种限制是不是指它的type system带来的限制，但这正是Lean为什么能验证证明的关键
- Lean不是第一个这样检查证明的语言。除了Lean之外，资格更老的还有Rocq，Agda·。但Lean在设计的时候更加考虑数学家的需求，也更被数学家欢迎。
- Lean还有一个酷的地方是它对metaprogramming的支持，你可以不去碰它的底层就为它添加新的语法。

RayHu

2026.4.22

Share 一下听后 MEMO😄：

https://younavi.me/doc/6wGVLthN12iqqS_WVaIppf_jgCg

RayHu:商业访谈录备忘：AI for Math与数学少女的探索之旅嘉宾背景信息姓名：洪乐潼（Carina Hong），00后华人创业者。身份：Axiom（公理）公司创始人兼CEO。公司概况：致力于AI for Math领域，近期完成2亿美元A轮融资，估值达16亿美元。学术经历：本科就读于MIT（数学与物理），硕士就读于牛津（计算神经科学），博士就读于斯坦福（数学与法学）。一、数学的本质：在艺术与科学之间搭建公理数学是契约与结构：数学并非简单的解题，而是一套文明体系。数学家们达成“契约”，在一套公理系统上不断向上搭建理论，它介于艺术与科学之间。发现还是创造？：数学发现的过程需要共识。证明不仅是逻辑的严丝合缝，更是一种影响力。只有当证明被接受，数学发现才真正成为文明的一部分。关于美感的直觉：洪乐潼认为数学最美的时刻在于跨领域的交集，例如代数表达式与几何物体的联系（如模形式椭圆曲线定理）。二、个人成长：从“蛮力型选手”到长期主义者拒绝零和游戏：在数学竞赛的压力下，她意识到自己并非“天赋型选手”，而是依靠勤勉的“蛮力型选手”。她通过学习高等数学来跳出竞赛的零和博弈，转向正和的知识探索。自由注意力（Free Attention）：区分平庸与卓越创业者的关键在于能否保护好“自由注意力”。这种非线性、发散性的思维状态是产生灵感和策略性决策的土壤。对苦难的上瘾：创业者往往是对苦难（Suffering）上瘾的人。洪乐潼在MIT学到的重要品质是毅力——在极端压力下保持内核的坚持。三、 AI for Math：人工智能在逻辑高地的突破大力出奇迹的AI：Axiom Prover在普特南数学竞赛中获得满分，展现了AI通过枚举、分类讨论等“蛮力”手段解决人类天才型创造力问题的可能性。形式化证明（Lean语言）：将数学语言代码化。Lean不仅是编程语言，更具备自我验证能力。它将数学逻辑从自然语言的松散中解放出来，实现严丝合缝的验证。核心技术三角： Proving（证明）：逻辑推导与验证。 Conjecturing（猜想）：提出有意义的数学问题，这是目前的难点。 Auto-formalization（自动形式化）：将人类浩如烟海的数学文献转化为机器可理解的代码，这是通往超级智能的桥梁。四、 Axiom的愿景：深科技（Deep Tech）的“SpaceX” 定位深科技而非单纯的模型公司：Axiom被视为深科技领域的SpaceX，具有极高的工程壁垒和长研发周期。首个商业落地：验证（Verification）：软件与芯片验证：目前传统验证手段耗时耗力。AI可以在编写程序的同时进行数学层面的验证，确保代码百分之百正确。 Math is Code, Code is Math：任何能定义的都能被证明，任何能表达的都能被执行。指数级增长的发现：AI将使数学从匮乏走向丰富，带来数学发现的爆炸式增长。人类数学家将转型为“资源分配者”，利用直觉决定算力的投入方向。五、启发洞察：好奇心驱动的未来递归式自我提升（Recursive Self-improvement）：当AI具备了自我验证和提出新猜想的能力，智能将进入加速循环。跨学科的连接力：法学的严谨、物理的逻辑与AI的算力在数学这一“现实世界的沙盒”中汇聚。学徒心态：洪乐潼将自己定义为“学徒”。她认为人类的好奇心是无法被压制的基本动力，即使AI解决了所有问题，人类依然会因为想要看懂证明而产生新的好奇。核心金句： “我们相信任何能定义的都能被证明，任何能表达的都能被执行。” “解决一个有意义的失败，比很多个肤浅的成功来得更有价值。”

JasonB2026:她连自己失败了以后去做神经科学都想好了，我觉得她不会成的

共3条回复

easymode

2026.4.22

太强了！00后的同学有如此的人生阅历和认知！嘉宾的知识面好广，数学物理法学计算机神经科学。稀里糊涂听完了🤣感慨一下普通人还是应该学工科

蓝色小鱼_S4gR

2026.4.28

果然是打过辩论的，思维能力太强了，对比一下小米那位，这期听着真的好舒服，而且她才二十多岁

HD497051s

2026.4.20

哈哈哈哈哈哈，小珺老师沉默最长的一期

姥姥王

2026.4.20

天才少女，听不太懂

椰椰阿梨璐

2026.4.28

26:46 这嘉宾表达能力实在太强了！连外行如我都听的津津有味。主持人的功力还要提升啊～

good_luck

2026.4.20

真不错这周又有的听了哈哈小珺辛苦

good_luck:3:15:34 他们想做科学家模型？听到这的感觉

__null__

2026.4.20

赞美所有lean community 的 contributors

-竹木-

2026.4.21

2:03:18 相比较而言Lean和program synthesis的关系不大，program synthesis 是在大语言模型出来前用逻辑方法研究代码生成的领域。Lean主要是dependent type theory的衍生物，当然和program verification也有很多渊源

LBeP:program synthesis 是来解决lean语料严重不足的一个思路。

-竹木-:嗯，lean的高质量语料严重不足，但不求高质量的话又很好生成一堆。之前alphaproof还是一个别的work说他们在mathlib的定理证明上随便加一两行证明就得到一个新的定理的证明，那些新生成的定理对数学家来说可能压根没用，但仍能够提升训练效果。你说的program synthesis扩充语料是指这个方法还是另外的方法？是另外的方法的话还挺想知道具体的

共3条回复