137. 对洪乐潼的4小时访谈:AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的张小珺Jùn|商业访谈录

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

264分钟 ·
播放数7828
·
评论数57

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
好喜欢这期啊!好喜欢!
感觉她的脑子转得好快啊!她的表达的速度跟不上她脑子转的速度,各种跳跃🥹
good_luck
good_luck
1 天前
真不错 这周又有的听了 哈哈 小珺辛苦
终于有AI行业的女生采访了!
姥姥王
姥姥王
1 天前
天才少女,听不太懂
__null__
__null__
1 天前
赞美所有lean community 的 contributors
46:37 请教大拿,这句英文,怎么拼写?谢谢
兽斯:Chip on the shoulder, chips in the pocket. 应该就是小宇宙自带的文字字幕里的这一句
Ulysses-2024:感谢,苦难却是能刺激内腓肽。这也是顶级运动员的常态。
3条回复
好好好好好好,听的很嗨皮
Dec_3
Dec_3
6小时前
我很喜欢这期,很有生活、人味的一起,听乐潼的描述能代入到她的经历中,很容易找到彼此的共通点。
让我想到之前罗永浩和李想的那期访谈,很精彩。
04:20 嗯,开头就懵了😅
第一次前排!
薯条哲学家海鸥同学:加入播放列表,中午开学
薯条哲学家海鸥同学:1:13:39 是啊,感觉现在大家很少在咖啡馆聊天了(特别是陌生人间)
3条回复
前排。哈哈
hercules_jia:00:00 哇塞。被哈哈。感谢对留言的点赞
最后结束的音乐名字叫什么?
Alpha_C
Alpha_C
18小时前
挺好听,但没有ai背景我听不懂
越到后面越精彩
HD497051s
HD497051s
21小时前
哈哈哈哈哈哈,小珺老师沉默最长的一期
-竹木-
-竹木-
13小时前
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条回复
ChaNg1o
ChaNg1o
1 天前
卧槽,这期可以
cypr
cypr
5小时前
这期最好看视频,姑娘眼里有光
-竹木-
-竹木-
6小时前
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的支持,你可以不去碰它的底层就为它添加新的语法。