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

264分钟 4.24万 2个月前

主播

节目简介

来源：小宇宙

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: [email protected]
Jump into the new world-and explore with us!😉

小宇宙热评

狂野时代的小熊

2个月前上海

好喜欢这期啊！好喜欢！

生而为猫奴

2个月前俄罗斯

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

Vera超幸运

2个月前美国

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

-竹木-

2个月前美国

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的支持，你可以不去碰它的底层就为它添加新的语法。