00后华人女孩洪乐潼创办AI数学公司Axium获2亿美金A轮融资

00后华人女孩洪乐潼创办AI数学公司Axium获2亿美元A轮融资 通过形式化语言Lean将数学转化为代码并构建Subagents系统，人工智能能以硬核逻辑和几千行代码的蛮力消除幻觉、实现超人类纯数学猜想的自我演进。 访谈回顾了洪乐潼从数学竞赛营、MIT、牛津到斯坦福法学院的多学科交叉背景，以及她在Palo Alto咖啡馆与联创舒博萌发创业想法、完成巨额融资并打造独角兽公司Axiom的历程。公司利用形式化Lean语言和自研Prover系统，在普特南数学竞赛中斩获满分，并攻克了Falcon等纯数学猜想。她强调Axiom是数学界的SpaceX，核心是通过工程化手段加速自动形式化，推动人类从“数学匮乏”走向无限算力驱动的“数学富裕”时代。 00后华人女孩洪乐潼创办的 AI for Math 公司 Axiom 完成由 Melo Ventures 领投的 A 轮融资，累计融资金额超 2 亿美元，估值达 16 亿美元，吸引了 57 岁美国终身教授小野肯（Ken Ono）辞职加盟。 (2:14) 洪乐潼自谦为“蛮力型选手”，幼时用复数法强拆几何题的解题思路，在多年后与 DeepMind AlphaGeometry 项目将几何图形转化为符号表达式的哲学产生共鸣。 (24:38) Axiom 团队研发的 Action Prover AI 在第 98 届普特南大学生数学竞赛中斩获满分，成为该赛事历史第 6 个满分获得者，通过数千行 Lean 代码进行枚举与分类讨论完成逻辑强拆通关。 (126:06) 在法学院期间，作为坚定文本主义者的洪乐潼受大模型分析宪法文本启发，萌生出将结构化数学通过 Lean 形式化语言转变为代码，并利用 AI 推进自动定理证明的创业想法。 (62:50) Axiom 放弃了昂贵的蒙特卡洛树搜索（MCTS），自研 Subagents 架构将推理链节点树扩展 100 倍，并以周期一致性校验法攻克自然语言论文到 Lean 代码的“自动形式化”难题，未来瞄准芯片与软件形式化验证的商业化落地。 (183:50)

Axium（Axien）创始人洪乐童认为，数学本质上是结构化的代码，通过引入 Lean 等形式化语言与强化学习，AI 能够突破传统概率模型的逻辑与幻觉瓶颈，并在纯数学探索及软硬件代码验证领域引发指数级供给爆发。 Math is Code：形式化语言重构证明系统 洪乐童指出，依据“库里-霍华德通道”，每个形式化数学证明在底层都可以映射为一段计算机程序，数学家数千年来其实一直在用自然语言写代码。针对大模型推理中的幻觉问题，她主张“把数学变成 Lean”，将形式化验证作为强化学习的刚性奖励信号。与盲目依赖概率性大模型不同，Axium 采用“Draft-Sketch-Proof”三步法，先用非形式化模型拟定思路，再翻译为 Lean 语言并挂起未证断言，最后调用工具链补全证明。该系统要么因问题过难而拒绝输出，要么输出百分之百严密的正确结果。 算力替代传统直觉：从符号蛮力到普特南满分 洪乐童将自己与公司技术路径归类为“蛮力型”，类比 DeepMind AlphaGeometry 将几何图形转化为符号表达式来解题（解决历史上 81% 的 IMO 几何题）。Axium 的 Action Prover AI 在 2025 年 12 月的普特南大学生数学竞赛中斩获 12 道题满分（120分），成为该赛事 98 年历史上除 5 位人类满分外的第六个满分获得者。解题过程中，AI 并未展现出人类教练般的“一图流”几何直觉，而是生成数千行 Lean 代码，依靠符号分类讨论与穷举完成严密论证，表明机器可以通过强大的符号与逻辑计算开辟全新的解题逻辑。 工程架构创新与昂贵 MCTS 的替代 为解决形式化语言环境下的工程效率瓶颈，Axium 自研了 12 至 13 个辅助工具，将 Lean 的证明验证速度提升至社区工具的 100 倍。同时，团队评估 AlphaProof 所采用的蒙特卡洛树搜索（MCTS）在推理扩展上成本过于高昂，转而采用 Subagents（子智能体）架构，结合路径轨迹作为经验开展强化学习，成功将推理链证明树的节点规模从 40 个扩展至 4000 个。此外，团队利用周期一致性校验法攻坚从学术论文到代码的“自动形式化”难题，将英语解构为 Lean 再反向翻译比对，以弥补互联网级 Lean 数据集匮乏的短板。 商业落地切入验证，战略押注专精超智能 在战略定位上，洪乐童主张追求领域专精超智能（ASI）而非全能型 AGI。她以餐馆盘子为喻：OpenAI 等机构试图从中心向外覆盖全圆环，而 Axium 则是从中心精准切向高难度数学与代码验证，形成覆盖物理、半导体等学科的扇形。在商业变现路径上，公司首选具备极高定价权的高价值验证场景，例如芯片硬件与内存隔离组件的性质验证，以此替代传统耗费数年手写数十万行代码的人工形式化流程。公司估值在完成由 Melo Ventures 等支持的融资后达到 16 亿美元。 洪乐童认为数学家未来不会失业，而是转型为提出高维猜想和分配算力的探索者，但 AI 能否在动力系统或随机曲面等缺乏先验设施的深水区自主构建忠实、非琐碎的“猜想与新定义”，仍是该路径面临的核心未解难题。

洪乐潼: 确实在每一个时期都觉得是自己是那个环境里面最愚蠢的那一个，最怎么要努力都看不到结果的那一个 洪乐潼: 大部分我知道的就是Founder，就是创业公司的创始人，他们都对苦难上瘾 洪乐潼: 没有人喜欢融资……他不是说难结果难，他就是累，你是一个复读机一次一次的说一样的事情 洪乐潼: 证明其实某种创意上它是影响力 洪乐潼: 你给我一道题，我三个月我做不出来我继续想。 洪乐潼: 我觉得我是Visionary，我反正肯定不是Salesman或者是Executor。 洪乐潼: 每一次你在执行与不执行、做和不做中，选择那个乐观的选项，你就能够有一天走到那个终点。 投资人: 我希望你能形成这种肌肉记忆，这就是你每一天需要去重复的、麻木的这样的一种 take the leap of faith（纵身一跃的信念）。 洪乐潼: 大家都是成年人，自己做一些有趣的选择，然后一起去承担选择的风险。 [224:38] 小野肯: 现在不是讨论数学纯粹之美的时刻，不要去精确地搞这些东西，现在是战争状态！ 洪乐潼: 在推特上说你证明了普特南或 IMO 题会赢得无数赞美，但做自动形式化这种默默无闻的‘翻译’工作却少有人喝彩，可它的工程难度实际上更大。 [206:18] 洪乐潼: 要么登月成功了，要么登月失败了，没有中间状态。 洪乐潼: 其实你要非写一个什么，就写‘学徒’。就是我想去在尽量多的一些智力领域上，能尽量多的去学一些东西。 洪乐潼: Authorship 就是作者，你是你自己人生篇章的书写者和作者。所以你不能觉得是一个情境决定了你的决定，是你决定让这个情境决定你的决定的。 洪乐潼: 这感觉像是两只鲸鱼，又找到了彼此的聊天频率。有些鲸鱼它的频率跟别的鲸鱼不一样，如果你遇到一个人，你们以前都是学数学的，现在都对 AI for Math 有一些理解，同时又有一些新的见解，聊起来就特别有意思。

[0:00] 大家好,我是小俊今天我们来到了美国硅谷此刻正在扎克伯格最早的创业所在的Facebook House这是一栋外表为带蓝色的可爱的小房子而今天也将迎来上一访谈录最年轻的一位嘉宾他是一位女嘉宾的女嘉宾00后的华人女孩名字叫洪乐童她的探索方向是AFOMAP所创办的公司Oxin刚刚完成了估值为16亿美元的A轮融资而她引起了很多人的关注则来自于这样一条新闻57岁的美国终身教授突然辞职去给24岁的华人女孩打工那接下来就是我对洪乐童的访谈因为我确实在每一个时期都觉得是自己是那个环境里面最愚蠢的那一个最怎么要努力都看不到结果的那一个在你的心目中AI format它在整个AI的大地图上它应该画在哪个地方我觉得大部分我知道的就是Founder就是创业公司的创始人他们都对就是苦难上瘾我听下来我会有一个问题因为现在coding也很火对那用math作为手段和用coding作为手段去执行任务的区别会是什么呢没有人喜欢荣泽没有人喜欢荣泽他不是说难结果难他就是累你是一个复读机一次一次的说一样的事情你一次一次的接到一样的问题真的我就能我可以把它录下来然后我就给你们大家发对吧你们反正问题也是一样的但是呢就是从这一些大量的比较无聊的这个过程中有一些让人很激动的谈话通常这一些谈话是你最终选择的选择的投资人比如我印象特别深刻的我们最后的领头方B Capital我跟Howard Morgan就是有一个对话哈喽乐童还是先给观众朋友们打个招呼并且做一个简单的自我介绍好哈喽小俊谢谢你邀请我我是洪乐童Axium的创始人和CEO对我想我们的聊天可以从一个故事开始就很多数学家在说自己被数学打动的那个时刻都叫做被数学击中的时刻比如说高斯就说像闪电一样你自己有过这样的时刻吗我就是自己解题的过程中这个稍微就是低频率一些但是我经常在看别人结果的时候有一种哇这个东西怎么这么美的一个感受我印象中特别深其中一个例子就是说第一次看到这个模型式椭圆曲线定理就是说每一个这种模型式它都对应着一个椭圆曲线相当于是把一个比较代数性的一些一个表达式和一个更几何性的一种几何物体就是联系起来然后我觉得就是数学中这种两个领域然后它们相当于中间有一个交集的这样的一个例子还是每一次我都是觉得非常非常非常优美的然后我印象中就是还有另外的比如说概率然后物理那里面又有一堆的可以就是让我觉得非常就是有意思的结果然后我自己解题的话还是就是小的时候可能见的不太多就是觉得数学还能还能这么玩就是当时从初等数论的时候一直推推到这个二字互反律我当时在美国的一个叫罗斯三零然后他每一天就给你每一天给你一个题集然后你要把它全部做完还挺多题呢全部做完才能拿第二天的题集像游戏打怪一样然后如果你做不完所有的题他就不给你下一个题集然后你就看你隔壁的那个同学已经就比你就是多了三个题集有更多有意思的可能是正确的东西但是由于你的证明能力还没有跟上你一直到不了然后到最后到二次互反律的时候就是他给你呈现了很多的证明我在这个过程中一定是觉得有被数学击中的时刻然后就是觉得非常表达非常简洁的东西他后面的这个证明可以很深然后也可以有很创造力的一些解法我有一个问题他可能会很好回答也可能会很不好回答就是有一天我跟AI在谈论数学的时候他提到数学是一种结构的语言所以我想知道从你的视角来定义数学到底是什么对啊这个确实不太好回答我觉得数学它有一点像是说是人类我们决定说去创造一个文明的体系然后在这个文明的体系里面由于一些就是我们愿意去说是呃我们认为是是对的一些功夫 [4:59] 然后往上去搭建就是我们他其实某种程度上是数学家他有一个契约就是说哪一些东西我们是愿意接受是理所当然的然后在这些东西上面最少的理所当然或者说不一定是最少看你从哪一个角度去看有一些人他会去从Compression压缩这里去看那希望是最少的公里有一些人是去希望能找最有意思的或者说就是搭配最合理的一套公里系统然后往上再搭建然后往上搭建的这个过程中其实我觉得这个过程是很多人觉得数学是解题就是我有一道题然后我把它做出来但就是往上搭理论的这个过程其实很有意思一般是先从一些数学的一些例子出发一些它就是比如说是一个序列或者说是一个集合然后你去发现一些规律然后这个时候你觉得很自然而然的下面的一个题应该是怎么样的然后再去证明它所以这个过程其实有一点点像艺术我觉得数学是一个介于艺术与科学之间的一个存在所以数学到底是一个被发现的过程还是一个被创造的过程这是一个千古的难题的辩论点你是哪一派我觉得如果一些数学家他们有一套比较相似的训练背景或者说他们在同一个领域里面他们阅读了同样的一批代表作他们会有一个某种程度上比较大的一个默契去说我们认为这个很自然而然的它应该是是什么样的然后如果说出现了一个比如说最有意思的就是当拉玛努金他从印度来到了英国他遇到了这个哈代和Littlewood他们就是Hardy Littlewood他们两个人就是一直就他们两个写paper他们写了很多很多的文章然后拉马努金来到这里就是像一个外星人一样他说嘿这是我的这个草稿本上面这些东西全都是对的我从来没有接受过数学的这个训练我不知道怎么去证明它然后哈代和Littlewood就会觉得这些东西看起来很有意思他们很新然后他们和我们之前做的东西又感觉是又感觉这个东西是对的但是所以他们就开始用证明所以某种程度上证明是一个与原来的这一群数学家所不太一样的一些人他们可以用证明来说服他们证明其实某种程度上它是影响力就是我只要能够去把这个东西严丝合缝的逻辑证明出来我这个数学的发现就是可以被接受的然后在他被接受的这个情况下当然了但是又会说你这个证明是美还是不美是自然还是不自然这个我们之前看到很多国际的数论学家去看张艺堂先生的这个的数论证明他们就觉得这个证明是和他们熟悉的一些学派非常不一样的一种证明方式但是在就是非常著名的那一个那个结果就是速数的这个固定的这个差这个他们觉得是正确的所以他们又接受了这件事情于是就是又开始去互相的去去学习和整理他们的证明方式比如说James Maynard2022年的菲尔兹奖他有另外的他的一套的证明的这个技巧然后他的学生们去继承他的证明的技巧然后他和这个张艺唐先生的这些就可以进行大家可以进行比较也可以进行简化这个过程其实是非常非常有意思的一个一个智力过程你是哪一派呀是那种直觉派天才派还是证明派我一直就是非常希望能当直觉派天才派然后这其实是我很小就是痛苦的一个根源就是我一直发现我自己没有什么特别大的数学天赋就我是一个蛮例行选手对我是蛮例行选手就是你给我我小时候在打数学奥赛的时候我记得他们说就是每个卷子的第一道题几何题欧式几何题欧式几何题是必拿的分你如果不拿欧式几何题你连这个三等奖你都拿不到然后我就一直做不出来欧式几何题我倒是可能能做代数不等式我的大脑可能更偏代数的符号的表达然后几何和拓谱实在是差所以我一般就是去把每一个点然后每一条线就用这个复述法就是大力出奇迹我最后我不需要去理解这个几何题它背后的几何意义我就把它完全是就是照本宣科的去拿一个套非常复杂的复述法去把它就是解决出来我可能会需要比别人多两到三倍的时间导致我可能其他题目的时间分配不均但是这是我做这个几何题的唯一方式其实最有意思的是2021年开始就是Google DeepMind他们从他们很秘密的开始一个这个Alpha Geometry的这个项目就是说如果我们这个拿AI去证明欧式几何体非常困难感到困难能否把它变成符号表达它这个不是复述法跟我说的这个人类我这个人类做的方式是不一样但它这个背后的哲学是一样的我把几何的图形变成这个 [9:59] 符号表达式于是这就是他们就能够通过这个东西去解决好像81%的就是AI就是AI能够解决81%历史上IMO的几何题就这是一个很有意思这是一个我不是天赋型选手的这个解释解释一我有一个解释二就是我在MIC的时候我身边所有人他们都是天赋型选手所以你只要就是看看左边看看右边你就知道自己不是天赋型选手但是呢我不放弃我是打不死的小强就是你给我也道题我三个月我做不出来我继续想我记得当时Henry Kohn教授他给了我一道sphere packing让我去想一些关于28位的这个sphere packing的一些小的问题这个东西当然不可能就是期待一个本科生完全解决然后我六个月我什么都没有想出来但是我每一周我就去说我这是我试过的我没有成功然后我又试了一周我又没有成功所以但这种蛮例行其实某种程度上会和一些天赋型选手存在一个互补就是说他们可能有一些脏活累活不愿意干的我可以把它去干完所以你的这个过程有点类似于AI的过程AI是这种蛮例行玄奏AI是直觉派吗现在AI里面它也分了这个比较天赋型聪明型的AI和这个比较蛮例行的AI比如说我们现在这个我们公司的这个AI系统它里面就是它是一个系统所以它中间有很多的模型它有一些模型就是能够很很快的去认定这个题目应该是被一二三四五六七步这么大概证明出来然后就是偏形式化见到了很多另这种形式化语言的AI他就会说反正我就是一个tactic一个tactic的tactic是另里面的一个步骤或者说是策略它能够让你就是从把你的一个很复杂的问题一步一步的去把它解决它更是这种严丝合缝就是小步小步走然后不是之前刚才讲的那一个能够列提纲的AI所以其实AI这系统里面两种就是类型的AI数学家它也能相辅相成某种情况下其实最有意思的是当看到一道题就是我们发现在我们最近我们公司在这个普特南大学生数学竞赛中就是这个Action Prover AI拿了满分然后是人类历史上有五个满分过去的98年1927年开始第一次普特南数学竞赛然后这是第六个满分是一个AI拿到的然后我们就有看这个AI的解法有一道题我印象特别深刻我们队伍中有这么一个同学他叫做Avan Chen他是美国就是IMO数学竞赛队的教练所以他是非常天赋型的一个选手他看到这道题他画了一个图然后我们所有人当时在那个会议室一看到这个图我们就说那你是把它做出来了就一个图的一个解法这个AI果然就没有找到这个一个图的解法我们看到了就是几千行的这个Lin代码它是就是硬生生的把它某种类似美举类似分类讨论然后就是一步一步一步核实去把它就是干出来的所以就是这是一个大力出奇迹的AI它可以看到这个机器它会去就算是一道很明显可以去做创造力解法的一道题目它可以去通过它自己擅长的东西去给出一个完全不一样的解法其实我觉得去比较人类与AI就是得到的这个证明解法背后的数学是一个非常有意思的过程所以数学不是人类的特权对吧现在感觉上这个自动定理证明这个领域发展的很好其实这个领域它不能够叫是AI的胜利它在没有AI没有这个神助神经网络的时候就有一群电脑计算机科学家他们就是去希望能够使得基于规则的电脑系统能够去帮助人类去解决能够解决的数学问题然后这就叫做自动定理证明ATP然后ITP就是交互性定理证明互动性定理证明就是毕竟有一些ATP无法解决的就是过去会有一些人类他们是数学家他们也会去写这种LIN这种特定的这种程序编程语言他们就会去与这个电脑系统一起去合作证明这件事情现在其实我们只是把这个ITP中的这个人类换成了一个AI而已他这个古老的这个学科其实某种程度上是ATP与AI的这样的一个交集我相信很多人都还是会对你很好奇你虽然一直在说你不是天赋型选手你是一个蛮力型选手但是你的过往的背景非常的强所以还是想聊聊你自己你在广州长大广州是一座非常有烟火气的城市所以你的小说的成长环境是什么样的广州是一个非常非常 [14:59] 烟火气的城市其中我最深刻的一个童年记忆就是确实有很多好吃的就是感觉到了后面长大就是留学感觉就是食物上比较溃疤尤其是和家乡的美食比起来我爸爸妈妈我们是在广州我在广州出生长大然后我们住在就是离学校很近所以就是每天可以走路去上学然后有些时候上学的时候就也会想想数学题然后也走到不知道哪里去就是这种说是就是想数学的同学们经常犯的这样的这个习惯我也有走路到需要多远就十分钟然后就是有时候会会开始游荡因为就是就是有时候脑子会想想别的事情其实我觉得这是一个非常快乐的一个状态后面就是我最近创业我有一个这个导师他讲到一个概念就叫做Bounded Attention和Free AttentionBounded Attention的意思是说被框架注的注意力然后Free Attention是说自由注意力比如说我们每一天早上起来我们看到很多邮件然后我们会有很多我必须要执行的事情因为我不执行这些事情可能说有一个期限性你必须要把它执行掉这个时候你的大脑是在一个被框架注的注意力的这样的一个情况下对然后很多很成功的企业家他们是非常有纪律性的执行家他们就是每一天日复一日的去肯胖复利他的这个执行这个很好然后所以我一开始就是创业的时候非常希望我每一天能做多少事情做多少事情但是就是后面这一个自由注意力其实是能够区分一个平均的一个创业者和一个很很好的一个很有策略性和决策性的一个创业者的一个区别其实是在自由注意力这里或者说一个数学家自由注意力这里是可以把人与人之间的这个差距拉开的点所以当你所有的时间自愿的去由于说我要做一个像就是像军训一样我每一天就是要干掉多少活你可能会使得你这个自由注意力这一块反而是欠血了你丧失了很多的机会成本所以我就是特别有时候怀念小时候就是走路上学的时候就是有很多这种自由注意力某种程度上就是人家说爱因斯坦的洗澡事件这个过程中其实能够有很多很有意思的一些就是大脑能到一些很有意思的地方去这可能是灵感和直觉来到你的大脑里的时候对但是这个事情是它不是一个线性的不是说你投入多少自由注意力的时间其实也有可能自由注意力的时间你什么都没有想到然后在后面的你可能在被逼迫做一些任务的时候在中间你会就是有一个callback就是回到了你其实自由注意力给你大脑里面打下的这样的一个基础你反而会在那一刻可能你大脑也不想做那些无聊的事情他就说我想到了这样的一个比较有创造性的一个想法所以自由注意力和帮力的tension和限制性的注意力它应该是结合的它有配比吗不知道我觉得大家的配比不一样人家说有三种创业者第一种叫visionary就是有前瞻性的野心家第二种叫做executor就是执行他就是能够其实扎克伯格我们在这个Facebook小屋今天特别特别有意思的一个场地扎克伯格他就是一个执行狂就是他是一个执行执行执行执行执行的一个人然后你可以看到他每隔一段时间会有一些行动去弥补可能前瞻性的决策落后所以他是一个非常就是执行的执行派的一个企业家然后第三种就是销售派就是他是能够销售派其实并不是一个负面的词就是他有非常好的沟通能力他有非常强的与不同的这个受众沟通能力然后他能够去影响别人引领别人然后把一个队伍就是这么建起来我一直从来不觉得我是销售派这个是肯定肯定不是的然后我也不是一个多好的知性派其实我也我可能就是也不能叫做前瞻性这个前瞻性是说是对的我就是想做一些事情然后我想做一些事情会极度乐观然后我极度乐观的情况下就算是往下就是跌一点它好像也还行也还达成了一个KPI所以你觉得你是第一种Victionary我觉得我是Victionary我反正肯定不是Salesman或者是Executor你刚才说扎克伯格是属于第二类他是第二类对你觉得像其他的一些企业家呢在美国这边一些知名的企业家知名的企业家马斯克是visionary这个是绝对的然后Sam Elman是Salesman然后我觉得一定要互补就是比如说扎克伯格他身边全是梦想家看Shrap [19:59] 这个CTO梦想家他也有其他很好的执行的其他执行的人就是我觉得光互补也不行你要有一些是你的同类然后有一些是互补桑德伯格做了很长时间的很好的执行家稳健的去把零到三千人的情况下这个文化都把持的很好其实我觉得Facebook非常强的一个点是就是每一个Facebook的人他们都bleed purple就是他们的血液里面就是紫色就是Facebook的这个颜色它们紫色紫色代表什么紫色就是Facebook的办公室有很多很疯狂的颜色其中有一个很明显的是紫色其实这个是因为扎克伯格他是colorblind他是有一些颜色光谱无法区分所以说他的那个就是办公室有非常大胆的大胆的颜色和其实去看那个Facebook的这个园区像是一个梦工厂他有24小时的这个雪糕店就是冰淇淋店然后有地方让大家去玩鼓 玩吉他 玩乐队我们公司大部分的人其实之前都是在Facebook的所以你会了解他们对 他们有一个非常强的一个叫做Bottoms off的culture就是由下往上 而不是上行下行它不是top downwnTop Down非常Google然后Bottoms of非常的Facebook所以我们公司其实某种程度上并没有一个定义文化的机会我们某种程度上沿袭了我们大部分的早期创始员工他们本来的文化好的 关于Facebook我们后面还会聊到我们先回来你在广州那个城市是怎么长大的对 就是打打数学竞赛然后我看看百家讲坛我是非常喜欢这个百家讲坛对我非常喜欢就是所有的就是中国的这个文学与历史我喜欢就是看那些历史故事我当时记得就是一中天讲三国然后珠子百家然后就是还是非常快乐的一段时间我特别喜欢文学就是黄永玉他有一本书叫大雅宝胡同讲二号然后比我老的老头就是那本书的书名然后其中讲到了这个中国的这个文艺界就是画家然后作家然后他们各种各样的画家版画家雕塑家然后他们都住在这样的一个北京的一个胡同里面我妈妈她是她是北京的北京人所以说我们家某种程度上我们虽然住在广州然后又有受很多这种精神文化的这个影响对所以我发现你小时候自由注意力是很旺盛的很旺盛的自由注意力因为你并没有把所有的时间都集中在数学上我对我也被数学教练小时候就批评说不是最刻苦的那一个OK但是我如果遇到一道题这个题就是要跟这道题去死磕就某种程度上你如果看我花了多少时间在那道题上你会说这个小孩很刻苦但这个过程中像玩一样它不像work就我觉得区分说是这个框住了的这种限制性注意力和自由注意力的这个其实是一个主体感知就是你到底觉得你是在玩还是在工作然后我觉得我小时候大部分的事情都感觉是像玩然后就是那些学校的作业就是一般课间就写完然后我放学之后就所有的时间我就是可以做一些其他的事情后来大概是初一的时候发现了一个事情我可以去找一些更高等的数学书看小时候是意识到说我一直要做数学竞赛所以我要比如说三年级做五年级的数学竞赛提及一直做数学竞赛更高级的但是到初中的时候就开始我为什么不去学学高等数学呢所以就是开始看就是微积分啊就是识分析副分析哇然后就觉得非常有意思因为它不像是一个零和游戏了就是做数学竞赛的时候总觉得其实比如说在这个广东省的这种奥数这种这个训练环境下比较痛苦的一点就是你的同学们他们要跟你考同一场试所以对于一个一个小孩来说这种友谊的这种概念也比较复杂就是竞争它就是特别存在但是你如果是看高等数学这个它没有它不是一个零和游戏它是一个正和游戏你可以自己就是到你想到的这个深度广度然后你可以找一些你们班里就是对这个比较感兴趣的同学们一块去讲然后你们不需要某一天同时去参加某一个考试所以那但是你还是要回来打这场零和游戏对我还是要打这个银河游戏然后这个就是银河游戏上就非常吃亏了有些时候看到一个卷子吧就是四道题最后一道你就发现是数论数论多美啊你可能刚最近看了这个高等数学里面去学了更多就是数论的这种高级的这个概念然后你就一趟 [24:59] 卷子你如果你的理智会告诉你你要在这个零和游戏中取得高分你应该先把第一道欧式几何题把它做出来接着你做第二道代数不等事然后最后这道数论题大概率你是做不出来的你要是做出来你就进省对了然后所以你不应该拿到这个卷子的第一课先从最后这道题开始但是我当时由于我就是课外的这种非常浓厚的兴趣加上我非常的喜欢数论我长大也是就是做数论我觉得我非常非常的爱数论于是我就会先从这道题开始然后一般来说这个时间就开始流逝然后在一个固定的一个比赛时长中这是一个不是最优的策略你是一个竞争力很强的人吗因为你刚才也提到就是在打比赛的过程中这是一场联合游戏也会影响一些友谊你是一个竞争力很强的人吗我觉得我在拒绝被驯化成为一个竞争力很强的人你在拒绝对我在拒绝被驯化成为一个你出众的时候意识到的我意识到的对我当时你你很难不意识到你你小学数学奥数奥连皮克学校的时候我记得四年级到六年级对吧每每一个月考一次试然后每一个学期之后他把你呃一班到24班全部重新排列嗯呃就是说你如果22 三二十四班是重点班然后就是一班在这个楼底24班在楼顶然后你每学期之后就是把你这个同学们就是换换教室24班的下去了下到19班了不是重点班你楼梯也往下走你这个心情肯定也不是特别好你一班在哪一班在楼底啊我当时进去的时候我是四班然后我记得就是就在这个洗手间旁边这个感觉就是说明这个我入学考试考的是真差对不是天赋型选手就某足了就是想上这个22 23 24的那个楼顶听说楼顶这个风景也好对吧就一个四年级的一个小朋友他肯定是会有这种就是争强好胜心就是在一个比较大家就会有这种压力的感受然后我后面是觉得就是这个不好玩我不想玩后面是什么时候初中吧出一串就我开始看这个高等数学书的时候我就开始不太想玩这个游戏了那你做出了什么样的改变呢在你不想玩这个游戏之后就客观条件上你还是要去参加那些考试你还是要去排名你还是要去竞赛我不是那么在意了就是我一直不到初三我没有就是初三要打初中数学联赛了然后我就是开始初一到初我临到零初中数学联赛我才开始准备初中数学联赛最后好像好像也考得非常好这个初中数学联赛就是反正我当时还特别就是惊讶我觉得我肯定是要考杂但是初中数学联赛考得挺好然后到高中的时候就是更多的时间就是当时还学英语对高中的时候又又更多的去学英语毕竟当时也打算是要出国所以就是更多的时间花在这一些这一些事情上面然后我其实觉得做出来的改变改变其实就是我发现一个有意思的事情就是你在一个群体里面你如果发现大家有一个很清晰定义的一个目标然后每个人都往这个目标也就是当时的不管是下一个季度的什么数学竞赛开始准备的时候然后你自己有一套完全不一样的这个Mental Model 世界的这个模型你就会开始找这个群体里面的一个Tribe一个部落你会希望能够去建立一个小的一个部落然后去找看谁跟你一样想读这个跟这个考试没有关系的书然后你就会和这些人成为很好的朋友我记得我初中的时候有一个游戏我到现在其实我们也在有时候显得无聊也在玩就是你有一个N乘N的一个格子你有一个棋盘比如说八乘八的一个棋盘然后你可以从这个任何的一个格子开始去走马步骑就是你只能去走这个跳马就是二乘三就是的这个每一步你只能这么走然后你连续的这样去走然后你每走到一个格子你就标一二三四就这么开始标最后你的目标是说我能够走满每一个格子不重复或者说你走满每一个格子你希望走到一个更高的一个数比如说八成八的话你希望尽量靠近六十四你不要在五十你就停了你希望至少到个五十九就是这个游戏我当时我记得我初中就和好几个好朋友们一块玩然后我们就特别希望我们一个一开始开始比看谁的数更大后面我们就希望能够去证明说任何N至少是五的一个棋盘你永远有一种能够走满整个棋盘的方式我们希望拿就是我们当时猜测应该能拿数学归纳法去证明如果你要去拿数学归纳法去证明你就需要在N比较小的情况下去构造一些比较有代表性的一些base case基础情况于是这个是一个非常复杂的工程让我们所有的这一些对这个 [29:59] 游戏比较感兴趣的同学在华夫我们就开始去构造然后非常难构造所以就是群策群力一起构造让我有一点想到我们等会我们应该会聊到的就是形式化证明比如说陶哲轩老师还有就是Alex Kontorovich他们做这个素数素数定理的这个证明然后他们就是把它也是分了很多项不同的项目让全世界的几百个数学家和Lin的这个编程这个编程编程的同学一起去把这个事情搭起来有点像就是数学其实某种程度上大家强调说这一个人他是一个天才他一个人证明了一个困扰其他所有人几百年的一个猜想然后他是一个多么厉害的数学家他有一种个体性的一个强调就是说这一个人他非常厉害但数学如果你去看软件工程师他们几百个人几千个人去做一个一个project一个大的一个项目它是合作性的合作性就需要一个比较好的一个结构和把它就是把这个任务去分散分散成不同的小任务这个过程其实我觉得是很有意思的然后某种程度上在玩这个马步骑的时候我们当时就是我反正一个人肯定是不可能把所有的这个这个这个例子找出来的我需要我的这些同学们这个小部落的这个帮助多少人啊这个小部落一般是三到五个人三到五个人对对对都是数学很好的人我们当时是那个数学班就我们整个班都是数学很好的人然后就是上课就不听课了就是就是传纸条那个纸条上就画着这个格子就是说这个你看我又找出来这样的一个就是N等于比如说9的时候已经被我kill掉了就是非常快乐的一段时间在这个这么快乐的时候你的成绩是什么样的就我反正要不到大考我也不太我还还行吧我反正也到了那个反正你的最终的目标就是你初中好像我们是90个人你要进到一个2527个人的一个数学组高中这个数学组所以我也进去了我记得我们当时是7个女同学好像初中然后到这个高中好像就是25 27个34个女同学反正就是那也进去了但是这就很奇怪因为你说你不是天赋型你是蛮例型可是你实际上花的时间没有那么多对这就是一个很有意思的一个点就是我认为你在学这些高等数学的时候某种程度上你的竞赛的这个数学也在得到这个前一默化的提升就这是这其实是很有意思的就是我们等会儿应该可以讲到就是我们发现最近有一个AI的一个发现就是说我感觉我像是这真的是我每天在想的事情我不是在打印广就是一个数学非常好的一个模型它在编码能力上也非常好就是它会有这种东西叫做transfer learning就是转移技能的转移我觉得肯定有这么一定的程度反正我当时我记得那个考试嘛就是从初中考到高中的那一个考试我是觉得我肯定要完了然后我的爸爸妈妈说你应该没事你就去那里坐一坐你看一下就是结果怎么样反正觉得应该你能考好然后结果我觉得我应该是拿了满分那一次然后我觉得我连几何题我做出来了我十几个十几个大的考试中没有做出来过一次几何题所以那次也可能是运气比较好这个很神奇就是从学习上对于你来说突飞母精是来自于你其实变得更发散了而不是更聚焦了你不是更努力的去做题了而是变得你可能兴趣还会更广泛了你更像玩去做这件事情了对对我当时是这么觉得的但是这个事情到后面我在大学的时候在MIT的时候就觉得还是要学会聚焦就我觉得可能就是数学好这件事情它没有公式然后我一直也不是数学最好的那一批就是每一次大家可能说你以前打数学竞赛然后可能现在在计算机的这些同学里面我有一定的这个数学背景但是我在麻省理工的时候我身边的每一个人他都比我聪明每一个我是整个数学系里面最愚蠢的是你自己这么觉得但是别人也觉得自己才是最纯的一个我觉得他们应该是意识到他们是很聪明的他们意识到自己是天赋型选手的为什么呢为什么你会有这种感觉你觉得自己没有他们聪明就是你的背景在别人看来就已经是天才型的选手了对但是我当时我的同学们比如说任秋雨张生桶高继扬就是这些人每一个人都是在这个我小时候看着他们的新闻长大的我看着他们的新闻长大看到他们去了北大树苑看到他们转学到了MIT见到了真人我每一天就是在就是顶礼膜拜这些大神就是我当时在MIT的时候这一种这其实是一个非常有意思的一个点其实甚至是有一些其他的小国的这个IMO的选手比如说我有一个好朋友他是这个比利时的这个IMO来到MIT看到美国的 [34:59] 我和中国的IMO们然后也知道大家的IMO分数他也会有一个心理落差我这个其实没有落差我的期待就是我是最傻的一个所以我其实就是适应的也很好我反正我就觉得我每天很幸运我能和这些人一起说话一起上课一起做作业我觉得还挺好所以你对你预期没有那么高我预期没有那么高我觉得我当时觉得我来到MIT吧我可能以后就去做这个量化金融了因为我可能反正你说这个数学博士为什么他会要我而不要其他每一个人都是IMO金牌呢他肯定我觉得我肯定也考不上数学博士所以我那我就反正我记得我大一的暑假我就是本来是要去桥水桥水基金去实习因为当时就我想着我要做金融嘛那我肯定秋天就是校招的时候开始打一去递典礼然后我记得去还是挺高兴的就是能当时去桥水然后当时疫情来了疫情来了的话就桥水就变成从一个就是线下的变成一个网上的这个实习了然后同时当时就有另外的一个机会就是我当时被Professor Ken O'Neill小野肯老师我们就是他现在也在加入了你们在Axium对他是当然他是一个就是神级教授他有一个就是REUREU的意思是Research Experience for Undergraduate是在美国是一个名词就是给本科生的暑期数学研究项目这这些项目他们竞争非常的激烈他们是美国的这个自然科学委员会他们去去赞助的所以他们的这个经费有限经费有限就是能去录取的同学们也有限然后我当时就被小野肯教授扔到了这个waitless后补名单上然后他给我发了一个邮件他说我在后补名单上的名次比较靠前然后我当时感到非常的激动因为当时我身边的朋友们我刚才讲的这一些大神们他们都已经被录取了他们在同一天已经收到了录取函我看到了一个邮件说我在居然能够到这个后补名单上我居然还能够在后补名单上名字比较靠前然后我当时就觉得我可能还是想去做数学研究因为我觉得我如果这个暑假不去下一个暑假可能就不要我了我可能连这个后补名单上我也上不去了所以我就最后居然被捞上来了因为可能疫情吧可能好多同学他们就暑假不想在一个数学下令营他可能还是想比如说就是在家里可能隔离之类的所以拒绝他的人那一年比较多我就被捞上去了我被捞上去之后我就没有去敲水我最后是结束了大学结束的时候那个暑假去了敲水你们家里有刻意的引导你在数学上的发展吗我觉得有我觉得我妈妈她有一个这个危机意识她小时候数学特别不好然后她是吗你们家大人有数学基因吗没有就是彻底没有他数学特别不好他数学就是他其他可能都好他就是数学不好他就觉得说你要不就是先就是学一学数学因为可能到后面你数学会是你学科里面比较落后的一个他是觉得你可以就是笨鸟先飞一下你的青少年时期获得了特别多荣誉这个非常的长我就不念了我们到时候可以给大家打出来小朋友时候的事情了对只是小朋友时候的事情那这些对你来说是轻而易举获得的吗我们刚在聊天他们好像都不是你当时的目标对不对他可能考试前两三个月成为了我的目标对我觉得我还是比较喜欢去做一些有创造性的事情比如说我记得当时大部分的时间确实花在了就是对于数学自己的探索上然后你说这些目标它其实跟这个也有很大的关系对它反正都是数学它只是类型不一样你可能说准备奥赛我也有准备奥赛的时候我准备奥赛就是在好像是很短的一段时间里面就刷了75套卷子然后就是当时它其实是一个纸的杂志然后就一页一页的每一天就是做一夜然后做完把它撕掉然后就是75套卷子75套卷子做完之后没选上去打那个比赛就是我觉得我的这个所以一直对荣誉这个事情我的感受非常复杂因为我确实在每一个时期都觉得是自己是那个环境里面最愚蠢的那一个最怎么要努力都看不到结果的那一个然后最绝望某种程度上就是对他不是一个在舒适区持续的不在舒适区是一个非常我觉得是对人很有就是塑造的一个体验就是失败是你的默认性你是在持续的不在舒适区对自己的要求比较高你就会觉得什么都是失败但是你又很乐观对就你没有因为失败很痛苦没有 [39:59] 就是你我觉得是可能是因为你很乐观所以你经常失败你每一次就很乐观觉得自己能够到达一个一个去希望能够去成成成就一件一件事情然后失败某种程度上就是自我定义的并不是说客观定义的可能客观看来不是不是失败你能描述一下你的一个失败的体验内心的体验他是一个外界的什么事情触犯你内在的体验对呃就是麻省理工的第一个学期他有一个叫做成绩保护成绩保护就是所有的这些新生的同学们他们都可以就是上任何你想上的课然后你不需要去担心你的成绩不是一个A因为这个GPA变得非常的重要我身边有两类同学我当时住在这个麻省理工的一个很有特色的一个宿舍楼我们这个宿舍叫做东校区东校区的这个如果你走到东校区的这个庭院里面会看到那种木头座的过山车两个树之间有绳索然后有一群人在玩喷火这是一个非常麻省理工精神的一个黑客的一种非常nerdy的这样的一个文化大家就是我反正我当时住在这里感觉非常有意思然后我在整个东校区的这种环境下我在西边楼的三楼这个3west这个叫floor piefloor pie就是因为它是三楼所以大家叫把它叫做派楼就是圆周绿楼然后这个楼上住的全是IMO就是这个楼上不是IMO就是IPHO物理的或者是IOI就是信息奥赛遥远住在这个楼上就是这是美国的一个奥赛选手然后这个台湾的这个余红勋住在这个楼上就是我们整个楼每一个人都是我的偶像然后所以他们就给了我一个建议就是说你就是去上最难的课然后你就是去上你可能都没有这个预备知识的这个课然后我就真的去上了这个课因为我身边的当时玩的比较好的同学可能都非常的有这个乐观精神他们可能也从这样的学长学姐这里听到了一样的建议所以我们有好几个这个大一的这个小朋友去上了这个博士概率论博士概率论我们想概率论嘛这个我们知道概率论是什么我们就开始在想一些可能让我们算一些可能比较复杂的不会算的概率不对第一天开始上上来测度论测度论从这个从Borel Sigma Algebra开始讲起从这个测度论背后的代数一个叫Boreau的一个代数开始讲起我们就面面相去我们完全不知道这个发生了什么然后这其实我觉得是一个很有意思的一个体验因为它不是一个竞赛环境下我自己一个人考杂了的这种失败就是有好几个这个同学们大家一块去感叹一个事情很难然后在一个在解题小组里面我们一块去尝试就是群策群力去把这个题集MIT特别倡导合作去把这个题集做出来然后这个过程我觉得特别特别有意思所以你这次就是你的不舒适感是来自于你选了一个更难的东西对这个考试好像是满分试卷是40分然后这个期中考整个班的平均分就连带着我不知道是混进来了多少我们这种吃了雄心豹子胆要上这个课的本科生平均分好像只有九分就是平均分只有九分然后我们的分数都是五以下的各位数我们这几个大一的小孩所以我们肯定是拖这个平均分后腿的这个主力军那你的失败体验来自于哪里来自于你我从来没有在一个考试上看到自己一个40分的考试我能拿4分但是你知道这是因为我选择了更难的事情我觉得它也不会触发你自己觉得自己很失败的这个机制对对我什么失败都不会触发我自己觉得很失败的机制就是我把这个失败当做是我的这个default默认想所以我就开始说那我要学分析这个课我学不好的原因就是因为我的分析的底子不好于是我就开始很认真的去重新把我可能十四十五岁学过的Rudin的实分析我又再学一遍那你的自我奖励的机制是什么呀你在追求什么呢你在那个时候这是你自己选择的一些选项我自我奖励的机制其实这是一个很好问题其实它有很多重机制我觉得我有我在就是年纪比较小的时候这种社区感或者说我有这个朋友或者说我有战友们这个大家有这种同志的这种友情一块去做某一件难事情MIT他特别倡导就是攀登就是登山队这个会给我很大的一个奖励的感受就是我们没有放弃就是我们期中考完了之后我们大家一块 [44:59] 就要么就一块drop the class就是都都把这个这个这个课给退了要么就一块继续继续做反正就是也有这个保护机制了第一学期然后我们大家就决定一起继续上这个课就这个事情我年纪比较小的时候这种奖励的这种感受其实来源于这个社区或者说是小团队小团队然后我不知道是为什么反正近几年是不来源于人了近几年来源于就是可能这个非常难的这个事情本身就是近几年可能可能我觉得是年龄小的时候承受能力虽然说仍然说是就是经历了很多失败的你自己感觉到麻木对吧仍然没有这种失败的感受但是在近几年可能真的是对这个东西完全没有负面的感受所以就是这个难的事情本身我有种对 pain and suffering这个黄仁勋老师讲的这个有更多的这种suffering反而对这些事情有点上瘾为什么我觉得大部分我知道的就是founder就是创业公司的创始人他们都对就是苦难上瘾就是对苦难上瘾对就对其实这是一个不一定很健康甚至有一个有意思的我听一些风险投资人他们说他们找这个founders就要找这种对疼痛上瘾的founders我听起来这个感觉非常的不可理喻他们有一句话叫做chip on the shoulderchips in the pocket就是说我感觉我的肩膀上有一些重量可能是我以前的一些伤痕这个chip就是在这个肩膀上的这个chip能够转化成口袋里的chipschips就是硬币就是钱就是可能说某种程度上对于疼痛的上瘾从这一些当然从这一些风险投资人的角度上来说能够转化成一个小创业公司的成功这是一个我觉得比较激进的一个理论但是某种程度上他有他有一定的一定的正确性在里面嗯你从小团队的这种奖励机制到这种事情的奖励机制这个分析限运化在哪疫情马上理工就你没你没有团队了就是MIT毕业了以后就是不是不是我我大一的时候下学期就疫情隔离了OK所以等会你零几年我是我零一年对我零一年然后还没有到二十五二十四对然后我二十四特别好一个书你可以玩二十四点对然后就是对对对当时就是就是大一下学期所有人就就赶走了呀就不在学校就是off campus了然后所以就没有小团队了那课还得上对吧那你必须要去学会从这个事情男的事情本身里面去找快乐的感受所以我当时觉得就是学习曲线是非常陡的他对我MIT对我是性格真的是有很大的一个塑造我觉得就是每一个我遇到的在麻省理工的同学他们都特别能吃苦他们会在雨天暴风雪里面去跑就是我前一段时间我上周末还去了波士顿一趟就看到又是一个下雪天那个暴雪风暴红色警报他们还在跑步这是一个非常有毅力的一个学校然后这种毅力它是非常有感染性的它让我终身可能无法达到MIT希望我们能达到的那种毅力的程度但我会希望往那个方向努力就是什么难做做什么什么痛苦做什么什么长期主义做什么然后对还有一个我觉得就是刚才讲到小团体这件事情就是呃他也就是训练了就是说在压力来临的时候其实对任何的人际关系都会有一个比较大的挑战就是可能说是呃有一些呃一对一的这些人际关系也可能是一个团体的这个人际关系呃保持自己任性和就是自己的内心的这种坚持和能够去影响或者说是不一定说是影响吧去促进一个团队他们都有这种感受其实我觉得这是一个非常困难的一个技能然后这种技能我记得当时就是巴菲特 查理汪格他们就有在一个访谈中讲到说如果你看到这样的一个人一定要把他就是招进你的这个组织里他的他的信号是什么他标志是什么标志是一个自己内核很坚持很技术派的一个人同时能够有领导力但是领导力这是一个非常满的一个词就是leadership在美国的语境下我觉得和中文的语境下他有一点 [49:59] 一定的区别我还是觉得就是你千万如果你想就是领导力里面领导两个词你就没有办法有领导力就是一定就是服务型跟随型就是最好的领导力可能是服务最好的领导力就是别人就是整个团队在登山的时候你不是前面那个拿着喇叭的那个你是就是后面递水的那个你刚才说不想打零鹤游戏那你觉得你当时打的是一场什么游戏当时就是如果我去学高等数学的话我就可以就是有种就是你感觉有耗入烟海的不是你已经知道的这一些数学的这些概念他其实这是一个很有意思的点就是我在数学的竞赛中我是有一个就是syllabus就是有一个考试要领可能说每一年就是都是这些考点然后在高等数学里面我只要去新引入一个定义新引入一个概念我可以基于这个概念与以前的这些概念去发散出新的这种定理和问题然后这个某种程度上开始像搭积木其实有一篇就是AI for math的一篇文章叫做Lego Prover就是说像乐高积木一样就是你可以往上搭一个自己的小宇宙这个过程是非常快乐的这个过程是不受竞争所限的它不受竞争你就是在跟就是你可以在历史上的这一些站在巨人的肩膀上去探索一些事情对你为什么高中毕业去美国读本科而没有去比如说清华北大这样我是非常确定我希望能够出国我挺喜欢麻省理工的就我可能也确实看了一些电影我在草稿纸上写MIT我可能不一定是想出国我可能想来MIT为什么那个段子是真的什么这是真的我真的在草稿纸上写这个MIT对如果说我想去另外一个学校比如想去哥伦比亚大学Columbia可能要写的比较长MIT多简单就三个字母是在数学草稿纸上写的对对对就是数学就是你必须要一张白纸必须要一个铅笔不然反正也什么也做不出来就是有一些数学家就是他对这个纸质和这个笔他也有一些挑剔我是这样的人然后如果你有一句非常好的铅笔然后你有一个白纸的话你就开始想画画然后你可能就是我还画很多图形我经常我直到现在我们AXIUM的这个办公室上白板上如果你看到那种素描的那种立体立体几何图形就是我画的就是我喜欢Doodle所以我就是我Doodle的一部分我就会写MIT我对MIT信念感特别强我非常想去那里我看了比如说从这个就是Goodwill Hunting这个电影对吧里面讲的就是这个MIT那个非常标志性的这个大拱廊就是Infinite Corridor叫无限走廊这些事情对于一个小孩子来说我觉得是有很多的理想主义在里面的这个是怎么中到你脑子里的MIT这个字我怀疑就是看电影就是MIT他可能就是在这个pop culture流行文化中他成为了一个哦不还有很多很多的这个数学家物理学家他们是他们是MIT的尤其是还有很多宇航员他们是MIT的那你为什么本科学的是数学和物理啊双学位对肯定我要学数学这个我是知道我第一天他们还讲说怎么样去探索你去学哪个专业我肯定知道我要学数学后面在物理和计算机里面想了一下后来还是就是选物理就是某种程度上当时对量子比较有兴趣然后当时上了很多就是量子物理的一些课然后同时就是我做就是数学概率那边的一些研究比如说Professor Scott Sheffield他的随机曲面的那一些几何概率的这一些研究有很多东西他动不动就说这个东西在物理里面有一个意义这个东西在物理里面有一个意义然后我听他讲的比较多了我就想我也想学一下物理来了解一下这个到底在物理里面有什么意义我初高中我就是我想说物理特别长所以这是一个大胆的决定OK你大学又拿了很多的这种荣誉这个是怎么做到的就是你面对你觉得你自己是里面最蠢的然后最笨的一个然后你也不是很想竞争但是你还是从结果来说对他刚才不是竞赛的那有点像是这种我大学的这些荣誉像是就是可能一个教授他提名你然后你自己也不用他不是说你要去一个考试去坐在那里多少分钟他就是你可能你做你自己的事情然后学校可能会希望提名你去一些去拿一些奖项所以就是和我学校为什么比较欣赏你或者professor为什么比较欣赏你我觉得可能就是是一个比较高产的本科生对然后我觉得他们也很有鼓励性的意味对可能说看我可能平常就是学术学学的比较比较辛苦比较累 [54:59] 也就是特别怕我就是可能说就是不走数学了可能也有一些鼓励性的一些意味真的吗我觉得是的我觉得就是这个数学环境尤其我感受到MIT的数学环境教授们都是非常nice非常友善的人然后他们都非常希望每一个人好给每一个人最好的建议最好的推荐就是没有说你们这些MIT的数学的同学们是去竞争有限的名额的就是其实某种程度上每一个人有自己喜欢的数学你们喜欢的数学和别人喜欢的数学不太一样你们就是如果你喜欢这个领域的我就介绍你去这个教授这个世界非常大就他变成了一个无限的游戏了在大学期间他没有那么的竞赛和竞争了我的教授们他们是非常非常好的人就是我印象中当时有说当时就是疫情就是中美之间也就是停飞了就是没有航班后来就是赶紧就是有狂班的时候就想飞然后那个时候要写一些信啊给这个就是就是说这个人可以回来我们的教授都是非常好的他们对每一个他们的这个呃呃他们的这个辅导的同学都都非常的好非常的照顾比如说这个北美数学本科生最高荣誉摩根奖那是怎么拿到的摩根奖我觉得就是有我的教授他去提名我然后有另外的一些教授包括Professor Kano他们有写推荐信然后接下来其实就是评审委员会的评审委员会的这个决定了30年摩根奖的历史每年说虽然有一个人拿到然后有大概两三个人就是亚军和继军这些亚军和继军和拿到的这个人的数学水平没有什么差别然后可能还有很多没有被recognize到的同学他们都非常的好就是在我们的当时的那一个圈子里面我并不觉得我是数学最好的那一个人就我觉得某种程度上就是但有那么一波大家觉得就是可能研究还做得不错的本科同学其实谁拿到谁拿不到就是这个事情的随机性是很大了的对理解了你在本科期间在数学上有哪些新的探索感觉你喜欢什么对我当时喜欢还是喜欢数论当时可能有就是一个抉择就是哪一个哪种味道的数论是做更代数数论还是做更解析数论这个中间有一些想就是决定我印象中当时还是做了很多的就是模型式对然后做了一些椭圆曲线这一些的工作是在Professor Ono的这个我多于一半的文章其实Professor Ono然后和Io在他的就是这个夏令营的里面的合作者我们一块去写的对然后硕士去了牛津硕士去了牛津为什么学了神经科学没有继续研制数学的路寻找但是也竟动不动往数学系跑就是数学系也离我们那个学院也比较不太远对就就走十分钟然后神经科学那边是我其实当时出了一件事情就我可能非常想知道就是人脑是怎么样的一个构造就是当时家里有一些事情就是我可能想对我当时爷爷有一些对我当时想对大脑有更深的理解对然后到了那里发现你如果要对人脑有深的理解你需要做实验我之前做过果蝇的实验果蝇的实验是非常简单的你就是把他这个头盖骨一翘然后你就拿一个管子进去然后你就看他的这个neurodynamic就是果蝇这是一只小果蝇但是到牛肩的时候你要考一个就是license一个证你才能去做很多的动物实验就考这个证的时候需要你去杀一只老鼠我当时就是我做完了那一次实验之后我当时就是我要走计算神经科学我不要去做动物实验在英国就是其实计算神经科学和AI他们的这个关系非常的紧密在有一个UCL的Gatsby Institute里面他是原来的Deep Mind的的Miss Hasabis在那里做了他的Postdoc过后的工作然后在这个之前Jeffrey Hinton其实是就是是AI教父吧他是founded了这个Gatsby Institute这个Gatsby Institute他叫做Gatsby中心他叫做计算神经科学中心Computation and Neuroscience但他实际上其实就是大部分都是AI的Faculty然后我跟就是Andrew Sachs教授然后包括Andrew Sachs他的一个collaborator其实就在斯坦福叫先生跟Gooley我们当时有做一些研究然后还有Tim Behrens然后Will DorrellJames Whittington就是有很多非常杰出的又懂数学又懂AI又懂一些神经科学的研究者然后我当时是一个硕士的一个同学当时我反正我记得我见到他们中的任何一个人我当时就觉得非常的激动我就觉得我感觉这个人好像能带我做做研究然后觉得这是个非常好的机会 [59:59] 所以你是被AI点燃你不是被神经科学点燃了最后我最后是我的那个快乐来自于来自于AI不来自于神经科学当时还就是要写那个硕士论文就是这一些我刚才讲的这些研究员们他们要一起来协助我把它写成一个更神经科学的一个毕业论文因为就全是AI后来怎么写的写了个啥就是有其实有找到说比如有一篇其实就是continual learning的一篇去看这个neurodynamics然后另外的一篇是就是去看一个假设一个one layer linear transformer这个理论机器学习能做的事情非常有限在这样的情况下你也找不出你也没有办法做exact neurodynamic你就可以去但当然我印象中非常大量的线紧代数非常大量的矩阵运算就是在出现在前面那一篇大量的这种就是ODE对其实都是非常基础的数学应用在这一些可以有有有AI与认知科学背景的背景的这些项目上那你博士为什么又去读了数学和法学在Stanford我博士这个数学我是本来本科的时候就是defer了所以就是本来就知道自己要回去读所以我当时是本来打算可能本科之后直接去读数学博士没有去经过这个牛津这一层为什么牛津去了呢因为罗德小学金我觉得是一个非常好的一个机会对我有另外一层就我从小喜欢打辩论所以我觉得在就是牛津的这个有这个Oxford Union他有一些训练你去成为一个更好变手的一些活动然后包括是后面到法学院去做就是latigation诉讼相关的我不是并购那一边的我是诉讼那一边的就是暑假实习之类的其实都是由于这个辩论的这个很小的时候开始辩论的热情所以你其实整个的发展非常的综合能这么说对吗但我差了也是实在是差就是综合一般意味着是没有短板就是我还是有很多很多短板你差的是什么短板是什么我很多事情我都就是做得不太好比如说我印象之后当时地理是非常糟糕我到现在没有任何的方向感我觉得我是一个比较spiky又就是不太好的就是不太会的东西也非常spiky的一个人我是一个hberians的一个人那经过了数学物理神经科学AI包括法学这多重学科你站在这个交叉路口你看到了什么呢就在你可能站在博士的那个时候对当时看到了就是几件事情第一件事情就是我当时对宪法非常感兴趣然后我当时就是宪法里面它分几种宪法去诠释美国宪法的这个方式比如说originalism原典主义就是说所有宪法现在我们看到的是基于国父们就是建国的那一些人他们的原旨原意应该来这样诠释宪法这是第一种然后第二种就是叫做textualism就是说宪法写的这个英语字是什么你就把它读成什么你不要去想他们原来可能想的是什么你就是去一字一句的去解读去看到一个定义特别像一个数学家可能会去做的一个诠释第三个叫living constitutionalism或者叫policy consideration就是说这个宪法它会呼吸它会与时代一起成长原来的宪法是这样写的我们应该把它看到21世纪去怎么样去解读它就是然后在我在法学院就当时对这些东西非常感兴趣我是一个非常我是一个textualist就是我是一个按照它是什么样就是什么样的这样这是我的我的司法哲学judicial philosophy然后当时他们就有人说如果你想去了解这个到底是什么意思因为我们不知道这些词是什么意思可以去拿一个就是LM去给他一些就是一些data让他这些data可以包括什么在里面也值得商圈可以包括这些建国文献也可以就是包括现在的一些一些一些一些新的当代的一些一些政治与哲学的一些一些一些一些著作然后我当时就有一个想法就是如果我们已经到了一个能拿AI去看这个宪法是什么意思的这样的一个时代了我为什么不能拿AI做数学我当时就在课上我在想这件事情我就觉得AI应该可以做数学然后我就想到一件事情就我最好的一个朋友之一就是他叫Kenny Law他是帝国理工Empire College他交换到MIT我们大一就认识然后我们一块上了很多的课我们是非常好的朋友然后他还教会我怎么下这个 [64:59] 象棋他是象棋的大师然后他就是告诉我从2020年开始告诉我他在做LIN他在做形式化证明他是最开始LIN里面什么都没有的就是Mathlib是一个空空如也的一个Library他把他里面所有的本科的代数本科的分析去把他一行行的把他打出来做基础的这个建设的那五到七个学生之一是Kevin Bowser的学生所以他就当时我就在想一件事情就是说AI如果能去做法律是去看比较structure的东西就是这个东西到底是什么意思而是研究的是比较specification这一块而不是比如说让你去拿AI去判一个这个人到底有没有杀了另外一个人一个普通的trial court一个case而是去看这个constitutional law比较就是precisely defined比较严谨的去定义的这个那我需要数学不是英语而是一个更结构性的一种一种呈现而这个另这个形式化语言他就把数学变成了一个代码所以他就可能能够去我当然就有一些这样的一个想法然后当时同时和舒博我们在这个一个叫做Verve的一个咖啡店我们一开始认识了然后接下来就是在Palo Alto在Palo Alto对就是Verve咖啡现在墙上还有我们两个当时就是照了一张拍立德相片他当时说你买了一共买了一千杯咖啡你就可以照一张拍立德我和舒博在那一定买过一千杯咖啡对我们给这个咖啡店就是带来了非常多的这个应收我们现在整个拜登室的每一个人他们每一天都在这个咖啡店然后然后我们当时也一直在聊这件事情就是乔哲星老师有很多的不管是播客还是就是写的播客要讲这个形式化证明然后我身边的就是Kenny他我知道他有多对这个Lin进行狂热他现在也在AXM前职所以就是好多好朋友们大家现在就是慢慢的聚到了一起就是希望能做能做这件事情我当时看到的一个事情就是一切我们认为的不可能都有可能然后如果是这样的话对我个人意义最大的就是让AI能够帮助我进行一些数学证明尤其我不是天赋型选手我有些时候真的是花某种程度上你说AI能够帮助我进行一些数学证明尤其我不是天赋型选手我有些时候真的是花某种程度上你说AI能够帮助最大的是谁是那些蛮例行数学家就我就我可能真的就是我要每举多少个可能性我要经历多少天去验证一个非常可能是一个standard argument一个标准的一种一种一种一种一种证明方式我要按照那个比对我记得当时就有一个事情就是Ben Green老师有一篇文章叫Sharcozy Theorem for Shifted Primes他讲的就是说我有一个集合我要保证这个里面的集合的A和B两个元素中间的这个差值就是A-B它不是P加1或P-EP是一个素数然后我能够就是从1到N中数出多少个这样的一个多大的一个集合然后我当时就我看到那篇文章我想这个东西能够被证明多少的数学问题就同样的这一套machinery就是Ben Green老师的这一套发明或者是发现你可以把它去做function field你可以把它去做当然说做shifted sum of two squares没有特别大的意义可以做x方加y方加减一这个没有特别大的不知道有没有特别大的e反正就是这一套的东西是工具是可以用来做很多的事情的AI应该把它完全解决AI应该能够达到一个一个很熟练运用所有DAVINPORT里面数论的工具技巧的一个博士生的程度我当时觉得这一件事这个事情一定能做然后我就开始想怎么能做这件事情就要算力就要我要想我有多少的这是哪一年20242024年就是你跟舒博平凡的进入咖啡出入咖啡馆那一年就是2024年2023年9月份到2025年的12月份去年12月份不2024年的12月份OK就差不多因为我当时还在我第一年其实我大部分的时间就是我在作为一个法学生的时候I had a lot of fun就是我每一天就是感觉特别的神奇我从来没有任何的就是作业是让我去阅读的阅读这30页这就是你的作业我的本科是一个工程学校一个MIT是一个理工科学校我不是一个文理我没有接受过一个liberal arts的education哦 [69:59] 所以我就非常非常希望能够多读点书然后我可以我还想练练英文写作我当时觉得我都可以去所以我那一年但是第一次吧可能科学数学它不在你的生活之中就有点想念然后我想念的时候我就跑到咖啡馆去我坐校巴当时没有钱当时是特别一穷二白打不起Uber然后从斯坦福做八分钟的一个你要走二十分钟你走20分钟到这个大草坪你到了大草坪你就可以做一个就是校巴做校巴8到9分钟你就到了这个火车站这火车站穿越一个隧道里面有一些流浪汉住在这个隧道里面你就可以到这一个Verv的咖啡馆舒佛就在那里你就可以去跟他聊这个科技与科学他那当时已经在Meta上班了他一直都在他是在Meta是89年的一个Meta的一个元老他是Meta的Facebook AI Research的Director就是他当时跟他当时跟田园栋老师差不多时候进去的就是可能还比田园栋老师早一些那你们怎么成为朋友了我也不知道他是谁他也不知道我是谁那你怎么认识的呢我们就在这个咖啡馆的这个桌子就是我一开始当那写作业我一开始当那就是我有30页的阅读每堂课有30页的阅读我就抱着这个这么大的这个法律书我就抱着这三个法律书我就我就我就去去其实其实挺就是非常不不不不不明智的一个选择你有那么厚的书你抱着他们去做小巴但当时就是喜欢那你为什么一定要去那里去做作业在Palo Alto downtown就是我可能我们这个法学院的图书馆就是一般周一到周五待的有点闷我说实话就是它有地台然后有点密不透风就环境你周末你就是想放松一件心情对然后我记得这个Verve咖啡馆的一个点它那个庭院有很多狗然后它只有周末有狗就是它周中的时候那些狗的主人可能没有时间带他们遛狗我当时一开始去那里的motivation就我可以读书我可以喝这个我会点一杯抹茶然后我就可以看狗这是我的一个我的快乐就是读法律案例做笔记看狗喝抹茶然后时间一多就总是我和发现我然后就有这么一个每一次看的感觉非常面熟的一个人然后我们一开始聊起来了是在里面还是外面因为它有一天一个区域外面一个区域在里面你们可能共同坐在一个长桌上对一个六个人的桌子然后唯一的一个六人人桌子这个六个人桌子里面其他人也永远都在那里哦对成了一个常客对谁开始先聊天的应该是一个就是没人打算聊天好像是他坐在窗边然后那个太阳特别晒然后我需要那个窗帘拉起来这么说上话然后呢然后接着就我就说我就我就我就非常谢谢你就是拉这个窗帘然后他就说我经常看到你然后我就说是我也经常看到你然后一个团话就开始了然后那怎么聊到数学的呢发现他有他学过数学他的本科是数学他的硕士也是数学然后他后面他好像还读了两个数学的硕士我印象记得不是特别轻反正就是然后我的那个就是他就很好奇我就是他觉得我应该是个法律学生因为我有这个书然后我们就聊这个我当时可能我不知道我在看哪一块呢我反正就讲这个案例是非常的离奇然后就反正两个人就开始做朋友吧就是我觉得还是感觉这个21世纪就是有很多事情就是在互联网上大家不太到一个咖啡店咖啡馆去聊天了嗯但我们聊了多久我们聊了就是我们一两年我们是朋友我们不知道对方在哪但他不知道你是Stanford的学生他知道我是Stanford的学生但他不知道他可能知道我是法学院数学但他不知道我他可能不知道我有一个数学研究背景就是他可能他好像听说过摩根奖他听说摩根奖可能是因为有很多摩根奖的同学转入了AI比如说Levon Alpert在AnthropicGreg YoungXAI的co-founder就是Morgan Price就是 like a thing in AI然后他不知道我也不是一个什么人物他不知道也没关系但是我是真不知道他是一个这么厉害的一个AI人你知道他在埋他吗他现在就是厉害你知道他在埋他吗我当时不知道我一直不知道他在埋他后来你们是怎么开始决定要创业的呢就是在你们这种漫无目的的认识漫无目的的认识和聊天对之后我有一天你们这种谈话持续了多久持续了一年半聊什么呢这一年半聊科学历史对然后就有一天我印象是秋天2024年的秋天那个时候我刚开始那个数学的PhD但我当时很多的时间其实在给XTX去做一些工作就是XTX是一个 [74:59] 一个量化金融的一个我暑假就是后半端在那里然后我当时就觉得我在那里就是觉得天哪这个AI更有意思就是你XX有卡呀对吧它有卡所以你能做的事情就比你在盖茨比做的事情多很多所以就当时觉得AI很有意思然后回来然后我就我有一天我就跟我是去跑步我就是晨跑然后跑完之后我不知道为什么我就觉得好像这个事情真的要真的要发生然后我就去找舒伯我说这个事情大概如果我想融资要融多少钱呢然后我们两个人在那算我们算就是多少张卡然后也在WARF就在WARF就拿了张那个餐巾纸在那算然后我们就说好像这个事情还是得做一个创业公司就是没有可能在学姐去做那我那一个学期在做XDS我疯狂的往CS的那里跑有一个CS斯坦福CS我觉得最好的一门课是一个叫做就是first year PhD seminar每一个教授为了就是招新的学生他们就会去讲他的这个research highlight你每一周去就一个学分你每周三下午去下午五点然后你可以认识你所有其他的一些计算机系的同学们我就坐在后排厅我是个数学系的然后完了之后你就可以知道我的天哪就是有这么多就是做机器人的他们在做什么做这个computer vision的在做什么反正就是非常it's an intellectual feast你是在哪一刻决定辍学要创业的其实我大概知道就我开始融资的时候我就知道我总有一天要辍学就是你先开始融资才辍学的你是先开始融资再辍学我就先开始融资再辍学因为这个我不能辍学因为我辍学了我没有身份我要拿到我的这个身份工作签证我才能够辍学所以我拿到我的工作签证我就辍学了因为就是一般来说投资人也期待你辍学就是你很难说是同事就是硅谷这个一般拿到融资就是开始要甚至有些时候辍学是融资的closing conditionOK为什么不是Shubo当CEO是你当CEO舒博当时其实还在一开始大部分的时间他还在卖了他没有他到后年他不是定义的加入你的因为我们当时谁都不知道这个事情能否得到这个投资人的支持这个事情是想不明白所以从哪个月份决定的我从9月份就决定了但我不到11月我没有融资因为我一直在劝自己不要做这件事情为什么我不太喜欢就是当然我觉得中国语境下的创业者是一种就是气质但美国语境下现在就整个Valley都是Founder就是创业者某种程度上辍学创业他就是浮躁我其实觉得如果我是一个本科生我绝对不会去辍学然后去Y Combinator就我某种程度上我觉得我是最不可能创业的一个创业者我非常的喜欢向往学节我非常的希望能够去做更多的数学的一些探索我非常喜欢在大学的一个环境所以我就两个月是在劝退自己然后但是每一天早上还在跑步然后跑步的时候想事情想的非常清楚到后面确定是非常非常确定然后到我非常确定的时候马上就感恩节了从感恩节到圣诞节的时候没有微信上班所以你要么就是那个时候到感恩节融完只有十天要么你就来年再融所以我当时就来年再融那两个月最后你是怎么经过了怎么样的COT然后决定一定要做我当时去读了这个科学史读了科学史读了科学史真的读了科学史全创业读科学史就是多少个先是从维基百科开始读科学史后面要找书读科学史然后有一个叫AI for math一个GitHub repo这个GitHub repo里面大概有几百篇文章每篇文章的after我都读过然后有意思的after我就会把整篇文章看完然后我就做了多少次费慢的过程在纸上去想如果说我这个东西要搭起来应该技术上怎么做我不可能说我自己觉得这个事情不会成功然后去骗别人的钱这个事情我觉得做不到所以我当时就到了一个程度我发现我觉得它不一定是一个研究问题它是一个工程问题它这个东西的科技的风险就没有我一开始看上去的那么高然后在这样的一个情况下我觉得是负责任的去做这个创业开始融资所以你是在自我验证这个过程对 我觉得就是某种程度上你如果去吸引一些风险投资你需要自己一定要对这件事情比较确定比较了解不然我觉得不太负责任但你质疑自己的点可能是说会不会我这是一种浮躁 [79:59] 那种跟风一个是不是因为AI已经火了一个是不是浮躁跟风这个我倒知道我特别我特别反对做一个AI founder所以我知道我绝对不是浮躁跟风反对做一个AI founder是为什么就是我我从因为我在MIT然后在MIT就是有创业社然后我的好朋友们一起去打那个Jane Street的那个就是量化金融比赛黑客客客房的这些同学们他们是创业社的社长我当时就两个队友他们两个就是这个创业社的社长叫我去活动说有这个free sushi免费的寿司我也不去我觉得创业不好它不是一件好事情我觉得还是要做教授有点无证业是不是对然后我觉得就是我总觉得比如说一个以非常产品为导向的这样的一个创业项目感觉像是昙花一现我当时也有这样的一个感受然后我希望做的事情是非常长时间的非常难的所以我觉得一般和一个创业的一个这种风险投资的一个周期可能不一定吻合所以我知道我不是福道跟风的那一批然后我当时还有在在想就是我有没有什么别的办法能够做这个AI for数学然后我当时还尝试去我要不加入一下别的做AI for数学的公司然后就在这个Werb的咖啡馆这个我们现在的主要的竞争者这个公司的CEOTudor他也是常客你说我有一天还就见到了Tudor然后我就说你们招人吗然后我当时真的是想就是我是想做这件事情要是我能跟别人一块做我也不用自己去从零到一就感觉太复杂了就是然后这是主要的质疑点其实不是一个感性的我是不是浮躁我是不是跟风就是我到底会不会这个东西然后我就我就去研究这个AI for math真的当时就是看paper然后这个过程也非常的快乐就是非常非常的快乐非常快速的去学习一些主要的一些idea从比如说2018年一篇文章叫ATP boost在没有AI的情况下去做这个形式化的这个定理证明然后我看到Bartos一个波兰人是这个作者我们现在Bartos也就在Axian然后我当时有另外的一篇文章叫Pattern Boost就是是从很多的数据中去找里面的这个Pattern找这个规律的一个去从很多的图中去构造新的图去为数学家去找例子和反例的Pattern Boost我当时看François Chartrand是这个作者现在François Chartrand也在Axien然后我当时看另外一篇AI for Math的文章叫Into Int然后这个是拿这个一种translative的翻译的一种方法从问题能够翻译到解法问题能够翻译到解法如果看到了很多这样的例子下一次来到一个问题的时候是否能够直接翻译成解法也是做数学发现而不是数学证明这一个文献里面的Alberto Alferino他现在也在AXIAN就是所有这个美丽的过程就是我所有这当时我作为一个学徒去看这些巨人的肩膀这些文章他们现在都聚起来了都在AXIAN这是一个非常非常我觉得神奇做创业者我觉得其实这是最高兴的一个过程你又形成了你那个小团体对你去问竞争对手能不能加入你们公司有没有机会他怎么说他说你是什么的PhD我说我是数学的PhD他说我们只着急是一个计算机的PhD哦 为什么?AI for Math?对 为什么呢?我不知道他当时就是这么说的哦 但是你们团队很多是Math的我们团队呃 这么说我们团队有三块呃 我们团队有非常多AI的人就是强化学习Agent 就是Applied AI的这一些人我们有很多的做代码生成的人就是programming language然后很多是compiler编译器的人比如说LM compiler那个主要团队在我们这然后他们很多其他的工作compiler arena就是所有的这一些compiler就是深度学习去帮助compiler就是代码生成的这样的一群人然后他们当时也是Yang Lecun那个Code World Model32个Billion的那个模型的后面的里面的一部分团队然后都在我们这儿然后有一群是数学这数学里面比较tricky数学里面有纯数学家像Kano小野肯教授像Evan Chen我说的这个IMO的这一个教练然后也有做Lin的做Lin这个语言的里面其实就像Python里有Pytorch它是一个图书馆和Python它是下面的真正的那个编程Lin里面也有Mathlib是一个数学图书馆和Lin这个作为一个编程语言两拨人所以我们也都有我们又有这个做Mathlib像Kenny Law还有他的朋友张居健就这样的一些非常好的好的同学们然后我们又有就是做Meta ProgrammingMeta Programming叫原编程就是去把Lin当作 [84:59] 一个编程语言来使用去创造出里面另更多的工具更多的抽象层这样的就是相当于你可以拿python去写一个autograd一个著名的一个coding的这个编程的一个面试题你可以拿python写一个autograd我们来了一个同学他拿链写了一个autograd对所以就是这里面又有很多块所以并不全是数学的人我们很多的就是招ML的同学他们很多背景我们我们队伍里面就是当然说算上实习上四个M五个M所以说五个M然后就是他们会有很多数学的prior就是context就是他们理解这个数学过程是怎么样的但我们要求非常强的again这是一个工程问题有趣24年9月你刚刚萌生的想法但是在努力劝退自己11月决定要创业了然后要等那个这个圣诞假才能融资等了圣诞假圣诞假你干什么了吗圣诞假干了很多事和书狗一起再来读文章为什么是你们两个一起他已经说我要加入了吗他当时没有他当时就是在MEDA就是他当时他圣诞假闲着也是闲着我们两个人就是找像是一个reading group又是Gberg吗他当时在旅游他圣诞假感恩节他都在就是在不在一个地方我们在zoom哦你们还定期要开会我们发现我们就是讨论我们阅读的心得我们发现我们能够是很好的联创团队的时刻是我们发现我们两个都非常讨厌Zoom我没有办法跟人开Zoom的会超过一个小时他没有办法跟人开Zoom的会超过45分钟我们Zoom了四五个小时每次的这是我们发现一件事情我们思考的方式特别的又相似又互补所以我们就非常享受每一次我们的一些技术的探索他现在是他是一个他当然你看他20年的GPU经历10年的AI经历他是当时Cuda第一批就是开发者然后当时20152016年2014 15 16年和乌恩达他们这个百度这个硅谷AI研究室他加入了百度他当时是2015 16这是他进入AI的他的第一部的AI是乌恩达说你懂GPU你懂点数学反正这就是AI来吧然后当时有Dariel就是Anthoropic的founder他们当时有那么一群小团队都在百度都在百度是美国就在美国就在硅谷当时百度是他们后来叫百度Mafia像PayPalMafia一样这些人后面是做了多少重要的工作多少个早期的OpenAI多少个比如说Dariel就直接是Anthoropic的这个founder然后非常好的一个他们当时就是scaling works我们就是做这个deep speechdeep voice就是把大量的这些speech voice的data去扔进去scaling works他们当时办公室有一个就是一个理念叫我们绝对不招一个语言学家他们当时是做的deep speech和deep voice他们需要语言学家吧按道理他们不招一个语言学家有一点像我们当时我们现在公司这个做编译器的这个团队他们当时1617年拿就是机器学习要去革命这个Compiler Co-Generation代码生成他们就说刚时就很多就是编译器的这些专家说你不可能做到的他们就说我们不需要你们我们照样能做到就拿AI进入一个领域去革命这个领领域,某种程度上是我们这整一个,现在30个人了,但当时就是早期这个创始团队的一个DNA,我希望能够拿AI去给数学,去做一些革命性的一些改变,你看他们说,他们不招一个语言学家,要用AI去革语言学的命,那你们是不是不应该招一个数学家,我们以为是这样的,我们我们以为是这样的我们当时定了一个事情就我们不招到第15个人的时候不要招到一个数学家为什么是15个随便说了一个数我们当时觉得我们钱也不是我们的种子轮大家可能看起来数额很多对于我们要做的事情来说大家的普遍的想法是我们underraise了我们是raise的不够我们的种子轮所以我们当时觉得人的这个人头是限制的到20个人我们可能就没有办法再招人了所以当时觉得那只能说那就那就每15比1这样的一个数学家的比例去走但是他那句话的逻辑是我不需要语言学家语言学家背景可能对于这个团队是负分对我们现在的想法就是我们招数学家需要他非常的思想开放早期的时候其实有一个 [89:59] 叫做Frontier Mass的一个Benchmark与这个Benchmark相关的一些同学当时有希望就是我们有互相都希望能够一起合作让他们加入Axion但当时就发现一件事情就是一些数学家背景的同学他对Scaling这件事情他有一定的一定的犹豫他对或者说不是犹豫他就不愿意他不喜欢Scaling这种哲学他觉得说我数学是一个公义我是个手艺像日本师傅捏寿司你怎么能就是给我一个当时我们说我们要做internet scale dataset有同学就是接了我们的offer之后就是不来了就说我不要我不要做internet scale dataset我们觉得又是要scaling又是要更好的sample efficiency就是当然说sample efficiency这个效率是一个非常样本效率是一个非常也是一个非常满的非常非常多意思的一个词了但是我就拿Percy梁教授的这个话就是他是做惩罚我们觉得来的数学家我们现在希望他是跟我们对着干就是是他们做adversarial的就是与我们相对抗的去做Benchmark基准级的创造就我希望你能够感觉我们的系统哪弱然后去就是当然是做越来越难的这一些基准级所以某种程度上就是Ken就是小野肯他加入之后我们的这个基准级的这个集结是我们的第一号任务我们继续把那个实验线来捋一下我们刚刚说走了就是当时已经说到了圣诞假期然后你们有一个reading group音乐开始容资OK你们读了多少文章你解决读了好多而且当时我记得圣诞节我们有一个叫圣诞大礼包杨凯玉老师他们写的一篇文章Gabriel Proyesha他们一篇文章叫做形式化formal theorem proving形式化定理证明AI的下一个前沿是一个survey papersurvey paper就是它不是一个研究论文它是一篇介绍其他所有研究论文的研究论文它就是把这里面领域的捋了一遍然后我当时我记得我那篇文章还我记得它第五部分是有这个目标就是说我应该一个好的AI数学家能够做到什么样的事情在这几个项线上他能够有什么样的就是能力这是一个我们就把它做成了我们自己的表格然后这个之前就是从从第一行到最后一行我们我记得我当时就是就是每一个提到的就是直接和间接提到的这个文章不管是引用力的还是就是只是提到的一种逻辑我就是比我已经有的阅读笔记我想我还有哪些没读到的然后还真有一半没读到的所以那个AI for Math那个GitHub整理的也不是很全然后就是所有的这一些当时就感觉就是我原来知道的像是一二三四五个很好的做法现在这篇文章给我连成了一个面了就是他让我理解这个这个Big Picture了我就是更更我觉得我的理解反正是当时有很显著的深刻所以这个谢谢谢谢杨凯宇老师这篇文章对对对然后到这个假期结束Shubo决定加入你吗他还没决定加入我们他到了就是后面再决定加入了我们他是觉得跟你一起讨论很有乐趣对他当时因为他是一个元老他是一个AI的一个元老我们我当时都没有敢问他要不要加入我们就是我我想着就是那他为什么开始你们是怎么开始这个阅读的呢就是硅谷这个文化就是很多就是AI的这个元老他可以做你的天使投资人或者他可以去做你的advisor就是他会他会事情特别流通就是硅谷是一个非常有魅力的一个地方就是学界工业界老师同学就是年长的研究者经历丰富的研究者和就是刚进入这个这个工业界的研究者他们就是汇集非常的流通非常的就是非常多的互动就是大家是谁不重要做什么事比较重要比如说Sugo他另外的跟他指导过的创业公司也有很多比如说Pika对吧这个文景他们也是其实Demi他是当时进入这个就是Facebook的时候舒博还是面试哦面试官OK所以他也跟MistroMistro那整个funding team本来在拉嘛就是是舒博他们同一个org下面另外的隔壁的那一个team就是大家都包括其实Mistro这个队和我们队伍的这个François另外一个其实我和舒博说加入之后第三个 [94:59] 加入的这一个人关系也很密切就是他们也是很多年的朋友然后你们说这种Twitter的关系吗没有Twitter就是我就是两个人有不同的背景看这个事情的角度不一样所以我们就聊了很多比较哲学性的一些研究的一些想法我们当然就是觉得自己读的读的足够多的时候就想就是有哪些可以做新的事情然后就是做新的事情的话又其实可能连接到哪一个古老的AI的其他的领域的一个做法比如我们当时看到的一些我们想做的事情就在James Doe的那个AI for Science那里他们有做比如说James Doe这个实验室一直有做其实可以对AI和数学很相关的东西然后包括比如说我们当时想做怎么样去做一个conjecture怎么样去做好的猜想当时斯坦福的这个计算机器就有同学在以希望能够造一个AIAI科学家这一个愿景去做怎么样去能够去提出好的机器学习的猜想就所有的这些东西都混在一起比如说我们现在做的一些事情跟当时早期做棋棋的这个expert system专家系统这些都有关系所以就非常有意思就是所有的这些东西没有人去尝试把它聚焦起来在一个工业界盈利性的公司也就有更多的充足的资金和算力的情况下去把这一些从2022年开始有一个爆发一个想法的爆发去把它验证下来就没有人去做这件事情我觉得非常可惜这是有结构性原因的就是2016年的时候Christian Zagady还有这个吴玉淮他们在Google开始做比如说Hole List这些后世一个就是定理证明语言2016年很早期Christian Zagady大概在201819年一直在改动的修改自己写的一个他写的一个白皮书就是这个未来非常长的一个白皮书然后在2020年我想说20192020OpenAI一列带着人做了这些事情一列带了他们去做这个GPTFMini F2F当时OpenAI还有跟Jesse Michael Hahn然后Stamp Lou这些后面都成为了其他的好的公司的创业者当时他们有做在Openizer这件事情2021年有一个实习生开始一个人去在Google DeepMind做这个Alpha Geometry他们发现哇这个做的是真好所有的资源进来scale up做成Alpha Proof然后做了你看2021到2024这是三年的一个耕耘2024一炮而同的这个Alpha Proof拿了28分差1分金牌的银牌这个对我来说是一个是IMO被解决的那一个时刻它就是那两道组合体解决不出来2025年反正也是就一道组合体大家都没解决出来2024年的这个DeepMind真的是Kudos to them这是一个跨世纪的一个时刻就是AI在数学奥赛上达到了达到了好的胜利这是2024年我们在2025年12月做的这个普特南的这个满分是这一个他们开启的这一个序章的一个尾声而已然后我们其实马上希望做的就是研究数学所以就是这是这个整个AI数学的这个发展的这个历史Shubo作为你的第一个员工对是什么时候决定的联创吧对他是二月份吧二月份你融资融好了吗我当时有了不错的就是这事能做起来的只要想做就是已经有了不是最终的价格但是不错的价格估值就是你出去融资验证了一下对其实很快就是一月份一月七号好笑因为一月头是这个GMN就是数学家大会我当时到这个我记得是应该是西雅图西雅图就是那一年2025年居然美国数学学会说我们今年的主题是AI for数学这个就是由于数学是一个相对比较保守的一个学科比较这是一个非常让人就是雀跃的事情所以很多人都去了还有一些计算机学家我当时和DeepMind的Adam Wagner就聊了很多我们发现我们都是曾经在某一个英国的学院上过学还挺有意思的然后这个Albert John也是在这个学院上过学的挺有意思的然后所以我回来了回来之后好像就是第三天就有就开始就有offer了然后就开始不停的微信们开始开始去竞拍哦去竞拍对怎么竞拍的或者就是比如说你给了我一个offer然后过一周有另外一个人给了我一个offer然后他们会尝试去把上一家的这个价格 [99:59] 就是超过它所以最后从第一开始的那一个offer到最后的offer翻了三倍的股市翻了三倍对你是怎么去pitchJVC的这对你来说难吗这是一个非常融资的融资之门怎么打开的因为你是第一次没有人喜欢融资没有人喜欢融资如果说有一天有一个公司能把当然我觉得这个很难因为毕竟这不是一个技能的问题就如果有一个很好的AI融资源我希望能够让他去融资你要付他多少薪水我可以给他percentage这个真的我可以给我觉得融资是很难的一个过程他不是说难结果难他就是累你是一个复读机你一次一次的说一样的事情你一次一次的接到一样的问题真的我就能我可以把它录下来然后我就给你们大家发对吧你们反正问题也是一样的这个但是呢就是从这一些大量的比较无聊的这个过程中有一些让人很激动的谈话通常这一些谈话是你最终选择的选择的投资人比如我印象特别深刻的我们最后的领头方B Capital我跟Howard Morgan就是有一个对话我当时在赶这个Rebuttal Deadline就是有一篇就是文章的这个然后我当时跟他在Zoom上对话然后就是我发现Howard简直就是一个他比你更乐观他比你更觉得你的商业模式有前景他告诉你这些是你的商业模式他是文艺复兴的co-founder和Jim Simons一起然后他也是另外一个硅谷老牌的一个VC叫first round的联合创始人所以他即使他是一个数学家他住在纽约他现在有时候还去纽约大学上上课然后当时我就觉得Howard Morgan是一个非常让我感到就是跟他聊天我很激动我当时在MIT的时候Jim Simons先生还在的时候有来我们MIT网上有一个两小时的一个维路谈话我当时是本科的那个数学社就是我们那个活动我就跟他去去聊然后所以今天见到不是今天就那一天见到Howard然后他还在那个硅谷的那个TV show里面就是出现过对然后然后他就给我介绍了另外一个一个人然后这个人其实是Jim Simmons的这个表哥表哥或者表兄弟反正反正还挺有意思他们俩长得还一模一样就是有一些有意思的谈话你可以见到很多不同视角的人然后你可以我其实觉得我不是一个特别厉害的Foundraiser就我不是我一般就是这个事情是什么我就讲然后我一般还把很多就是风险啊什么的我全讲出来是什么你讲的风险我当时种子论我就说这个我们商业模式并不是非常的确定的这个我自己做过这个量化交易员我不知道我们这个东西是不是量化交易我觉得可能不是吧对我听说这个还是有差别的跟量化它的效果到现在不如量化好了对对对我当时就说我虽然我自己在量化中做了一些数学我觉得你就是作为一个商业模式来说它一定不是一个最终的商业模式我拿这个的举一个例子是说一个数学比较好的AI大部分大概率上是有用的就这只是一个例子这不是我们具体要想的第一个市场我们具体要想的第一个市场我也不知道是什么我们现在是个种子轮目前的还是希望把这个东西科技给做出来当时反正是这样的一个就我讲的都特别保守然后我后来才知道投资人们一般来说他们见到的创业者们讲的比较毕竟是一个pitch他讲的都是比较乐观的然后所以他有一个打折他比如说你可能讲说感觉这个东西是十分他心里就给你讲一个buffer他有一个conversion rate我如果当时讲的是一个七分他就给我打折就可能打没了所以就我后面才知道的事情但是他们都跟你say yes你有被拒绝吗有被拒绝拒绝都还是yes没有人想拒绝我们他们就不告就没有人回你的消息了因为他们其实在希望做的一件事情是说如果有别的人要领投你了就是他不太确定他不想拒绝他拒绝你你可能以后不理他了他就拖着你拖着你完了之后看这个人给了你那我也给你就是它是一个这样的一个群体groupthink的一个过程所以他们后来都跟了吗挺多的就是那一轮其实挺多挺oversubscribe的所以你核心是需要找到一个领头方愿意say yes我们当时有好几个领头方的金牌的一个offer几个的金牌三个你是怎么让他们金牌的 [104:59] 我没让他们近看我其实这是几月份这是一月份到二月份到三月份嗯对差不多一个月一个一个月一个对零头发因为就是价格从一倍到两倍到三倍就持续你都在聊你聊的多少个人嗯我不知道大概几十个几十个我觉得呃这有一点就是可能说以前做数学一个职业习惯就是总觉得希望有一个很optimal的一个 outcome就总觉得说希望能够把这个这个轮座的这个结构好一些对然后也不太知道怎么融资对后面就学会了一些道理后面就后面的融资就胜利的多一月份有一个领头说我愿意然后你没有听你为什么没有直接接那个offer然后还在继续聊因为他要再录掉我50%哦我不可能让他带露销我50%你当时say了yessay了no吗我当时说了no但是一月份你就确定你这个事情有戏所以Shubo答应加入了是二月份的那个更真一点的一个offer就是然后那个时候他加入的就第二个offerOK但是他还不是最终的offer你还在聊我最终对我还在聊你聊到了三月份我当时二月份那个我是想接了的于是我后面我就跟所有人说嗨这个这个我是想跟他们走的就是你可以加入我这一轮但我可能不会去看其他的其他的offer了然后到三月为什么又变了呢我觉得就是这个Hawrard Morgan的效应这个完全就是我作为一个就是我对文艺复兴有非常大的一个这种崇拜然后而且价格也确实很不错就是二月你已经觉得有一个不错的offer但是你还在聊然后聊到了三月份是那个B Capital他是怎么offer里的他的一个风格就是你每一天都会接到他的电话他就是他非常看好你我当时在那个做rebuttal我没有时间就这个为什么这个过程中拖了很长是因为我还在上课我还在考我法学院的考试我还在那个我还在上我的数学课虽然说就是我去的也少一些但是就是我还在我有事情我当时还有XT就我当时非常的忙二月份不就应该准备辍学了吗嗯二月份已经有offer我有这个offer然后当时我就开始我还没incorporate呢我去找这个律师去去我去就是建立一个公司有很多很多当时什么都不知道没有人完全什么都不知道什么都不知道我没有任何的这个孵化项目我也没有我真的什么都不知道就是到最后是说他们说我要给你写这个term sheet了我这个你这个公司我写什么我说我还没有一个公司就是哦所以下月份开始成立公司二月份其实其实一二月份你问我还在做一件什么事情我在招团队就是我大量的时间比如说就是在吸引一些我非常渴望能够得到的AI for math的人才嗯Suber肯定是第一个对吧对但Suber其实它像它是占有的然后去去我们两个再去找一些找一些同学们对所以你是几月份辍学的我是夏天辍学的夏天辍学那三月到六月在什么那个时候我的那个就是我的工作签证下来了所以我可以我可以辍学了对三月六月在干什么就是你签了一个一个term sheet之后你要做很多的这个法律的due diligence然后他才能把这个钱汇到你要找这个办公室然后你又去找人当时有很多很多的AI人才在流动同时AI人才市场的这个价格非常的高我们这个创业公司无法去支付一个100个million each这种package所以我们当时花了很多的时间与精力在希望能建一个好团队对那一轮融资是三亿美金的估值对融合多少钱融了64个million就是6400万美元是比预期低的吗是比预期高的预期是50个million是比预期高的对你觉得作为一个华人女性在硅谷好融资吗这个身份会给你带来任何加分减分吗我觉得我倒没觉得华人女性我觉得就首先我比较年轻这应该是一个减分年轻做product是加分年轻做deep tech是减分我没有我确实不像说是我们团队里面的除了我之外的所有人我没有一个带带带带一个tech队伍的经理我没有这个track record这是这肯定是减分然后我觉得华人女性这个没有什么我我我没有什么加减分这不是一个加减分 [109:59] 年轻是一个减分我有时候我有时候倒是觉得说我有时候觉得就是年轻这个事情吧做产品的话一定是加分的但是做产品性比如说consumer比如说facebook这种对其实我觉得就是真正应该加减分吗年轻就是我觉得作为一个创业者来说你被要求的是长期进行重复的就是非常非常重要的决策而你的每一个决策给到你的时间是非常短的所以如果你没有一个很好的一个我是一个一个word model一个一个一个就是第一性原则的一个一个体系的话你这一些决策容易不太不太最最最最直化所以我觉得还是我还是希望说我如果再来一次我希望我能够再再再多多多几年再就我觉得太早了嗯没准备好对我觉得我当时听一些Zuckerberg 19岁他19岁开始他跟谁他融资跟谁聊他跟Peter Thiel聊Peter Thiel跟他在一个餐馆见面手上拿了一张term sheet说这是我的term sheet然后Zuckerberg说好的谢谢你我什么时候就是什么时候给你答复他说我们这餐饭不吃完你不签我这东西我现在撕掉这是一个19岁的一个创业者没有见过这一种大风大浪的事情他这个故事就是他就去了洗手间他去洗手间哭了一场回来签了这上面肯定有他不喜欢的Terms他放弃了他去其他竞拍的机会我觉得就是年轻创业者真的还是挺就是当然创业者这个事情就难就是年轻创业者这个事情就是你大部分时候你并不知道你自己的这一个决定它到底是对还是不对的你可能等一会儿有更多的信息会能够让你对你自己的决定感到更加的自信但并不一定让你决定更对或者更错而你去等这个更多的信息这个过程中是一个高风险低收益的一个过程所以就是有些时候你还不如就直接跳下去就是我记得我们有一个有一个投资人他拉我们一群女性的一个创业者去一个活动找了一个那个森林然后在那个森林里就是Zip Lining就是你抓上那个东西你就晃过去就是一个树一个树中有个绳索你知道自己拴在这个绳索上我当时我第一次我人生从来没有做过这个Zip Lining我就不敢下去然后呢但是就特别尴尬因为我是第一个人后面有一群就是女性创业者他们都玩过这个好像他们以前可能去年就有这个活动然后呢他们就有点等得及然后我就只能就是一闭眼一咬牙我就下去这个过程后面他们跟我说我希望你能形成这种肌肉记忆就这就是你每一天需要去重复的麻木的这样的一种take the leap of faith所以我觉得这是我希望可能说我希望我如果说就是再来一次还是这个年龄的话我希望我以前就是能够把阅读再再抓紧一点我可能希望能读三倍的书我可能我所有所有所有我学过的东西都不够用这是一个非常有挑战性的一个一个事情其实就是因为这种高压快速决定的的这样的一个一个一个nature不管怎么样你在那一刻你得跳对你有遇到你要绳栓的不紧巴就完了对你有经历像小渣那样跟Peter Thiel那样的时刻吗然后自己在微真间去哭一场回来歉了我有一些我倒没哭但我有一些各种各样的感受到比较艰难的可能我现在做的这个决定我以后会后悔但是我也得做这个决定的时刻比如说就是大部分的人才的早期大部分的人才的情况就是人在手上有六个offer你得精排对我成了那个但我又我没有人家有leverage你做不了Peter Thiel对吗嗯那你是决定出还是不出你肯定得出呀你你你就这个这个事情为什么他痛苦就是你其实只有跳一个选择你你只要bias toward action每一次你在执行与不执行做和不做中 [114:59] 选择那个乐观的选项你就能够有一天走到那个终点这其实是一个但是对这其实是一个我的一个感受就是有些时候其实没有办法去想有几次这样的情况很经常很经常对硅谷的AI人才的价格已经非常高了对但也不单是全是人才的这些就是有很多很多类似的时刻除了人还有什么除了人还有什么我们又有一轮融资在这一轮融资中也有很多的一些故事或者说是就是很多很多的情况下我觉得就是要让利吃亏每一天的让利吃亏让利吃亏这样才能够做到一个一个一家一家伟大的一个公司让力吃亏对就是让力吃亏种子轮是25年的1月到3月几月close对7月close下一天close然后与此同时你出学了当然等那个签证等了对对对然后第二轮就是A轮是25年底开始的吗不A轮没想融A轮在圣诞节的时候我们已经有的一个投资人说我们要preemptpreempt的意思是我知道你现在不融资我知道你没有PPT我知道你什么材料都没有我要给你一张一张term sheet然后我希望你能够直接现在像Peter Sill希望你能够尽快地把它签掉这样你就不用再去融资我省掉你这样的一个这是他们的这种就是first mover advantage有这样一个感知1月5号我被交到了一个外地的一个城市然后我给了一个pitch然后我拿到了当天晚上拿到了这个offer然后接下来的一个星期之后还是一个半星期之后拿到了另外的一个offer我们最终签了那一个offer这是我们的A轮所以是从7月15号到1月15号这个差不多是六个月为什么选了第二个是一个很好的问题其实主要的原因是我觉得后面我们也让第一个让他也投进来所以并没有一个特别大的一个取舍我反正也能够得到很多非常长期以来支持我们的投资人的支持余帮主最终有一个Bose的一个解法领头方是谁领头方是Melo为什么你觉得他跟你可能更气候对,Melo的这一个partner Matt Cranning是一个从我们种子文开始对我们提供非常多帮助的一个投资人,然后他也是本来是,他是一个电气工程的PhD和物理的本科,然后他是一个非常technical,非常有一点nerdy,非常有意思的一个operator,他非常的就是founder spirit,然后同时Melo又是Anthropic的最大的institutional investor,然后我们是Melo Ventures在这个Ventures这一部分继Enthrope之后第二大的AI投资他们为什么愿意为什么愿意我觉得他们其实种子伦可能就想投但我们当然种子伦就是认识的时候比较晚就是已经差不多就定下来了对然后我觉得我们在六个月里面这个团队执行的快转这个团队在这个六个月的执行中持续表现没有失误而且他们在从零从什么都没有就是第一个月搭所有的infrastructure然后完了之后开始去串模型搭系统然后去做这些决定就是deterministic确定性的tooling而不是用令这个变成语言去写所有的这个东西是一个非常我觉得是spectaculously executed的一个非常完美的呈现的一个工程项目然后在四个月的时候拿到了普特兰的满分然后在六个月的时候去做出了许多研究问题没有许多一批三四个研究问题的解决然后是没有人类干预的第一个自动形式化证明系统达到这样的一个里程碑然后又发现了一些在代码证明中的一些神奇的transfer learning就是原来这样的一个AI数学家能够在代码的验证中达到一个非常好的一个表现在一个Varina benchmark中DeepSea Prover达到了11%当然这是老板的DeepSea Prover了我们达到了 [119:59] 98.93%对就是原来的这一个解决普特南的这个数学系统所以他是主动peach的你Mano我们就是大家都经常有时候会定期会见面毕竟他们是我们种子轮的一个小的一个他们种子轮放了他们是我们种子轮1%的投资人然后现在是当然作为领头整个过程整个过程当然会更加的更加的多几步对这一轮融资的估值是16亿美金已经达到了一个独角兽的标准融了多少钱我们融了有至少是2亿美金2亿美金这个过程中其实你们团队很多人都就是看起来经验都比你丰富很多然后包括也有非常知名的数学家的加入为什么他们都愿意让你来做CEO你刚刚也说你是一个最年轻的一个然后也没有任何的Tech Leader的背景他们为什么对此没有顾虑我也不知道呀我也每天在想这件事情就是可能可能他们也没有意识到我也没有意识到反正就是大家就一起在执行然后现在的一个设定就是所有所有的所有的一些比较strategic的一些事情其实就会就是route到我和苏果这里对所以我们其实能够使得研究者和工程师们有很好的一个环境可以去就是在没有任何politics没有任何人事纠纷的情况下去纯粹的去最新在技术上然后就是去执行所以我觉得这是一个很好的一个frontal lab的一个环境然后我觉得还有一个就是这个问题它是一个非常有意思的问题它非常的宏大它也非常的困难然后这个事情又有很多很明显的12345为什么这些技术上会难做但为什么这些通过好的就是engineering都能够去解决所以我觉得大家其实是被这个问题这个北极星去吸引对我只是那个地水的人对你们也算是现在的一个new lab对吗我们是在那个TBPN和这个滴滴的这个New Lab名单上确实是对你怎么理解就是在相同类似时间内成立的这一波New Lab对我当时融资的时候还没有New Lab这个概念所以低了融资的时候对对对所以就是他们就觉得我疯了就是投资人就是他们他们就是可能就是觉得这是什么呢就是当时而且还有一件事情二月份的时候Deep Seek出来了当时大家对模型这两个字就非常的恐慌大家一听模型不赚钱不要偷就是模型感觉模型还不如一个consumer产品有mote当时大家是这样的一个市场的为什么因为Deep Seek把价格拉得非常的低对它commoditize了模型所以说大家都不想偷模型了然后但是大家没有意识到一件事情我们不是一个模型公司我们是个DPEC公司我们是一个生科技公司我们做的这件事情有点像SpaceX为什么你们不是模型公司你们偶像当于成为一个数学的数学家的大脑啊对就是Lin吧它有一个很古老的一个背景就是这一些做program synthesis我查了一下这个中文怎么说叫做程序综合我也不知道这个对不对然后program verification就是程序验证就是它来自于这样的一个古老的一个领域然后另作为一个形式化语言它目前就是在公开的这个的domain的领域的网上的这个这个总的这个tokens这个就是字符串的这个这个这个这个就是不太大就是它是一个非常小的一个一个数据数据集所以说就是会遇到很多的问题比如说你怎么样能够做一个internet scale一个互联网这么大的像像有多少python就有多少lean这样的一个一个一个数据的这样的一个扩充呢这是这是一个不太不太清楚的一个问题啊lean它作为一个编程语言又带有自我验证的这样的一个性能有点像呃既是一个C这个编程语言又是GCC compiler和C runtime两者合一它是一个非常finicky也就是说非常脆弱的一个语言它的这个它有很多的限制它有很多的就是作为里面的这个object它必须要符合一些种种种种的这个限制它所以它是在作为一个另它本身又带来这些挑战然后呢另里面又比如说我想去验证一个东西它真的是在证明没有给我就是作弊作弊作弊比如说我假设公里n加n等于n证明2加2等于2你知道2加2等于4这一定不是一个合法的一个运算那么我如果要去找一个东西能够去证明它是严丝合缝的叫verify proofverify proof这个东西原来叫做community里面 [124:59] 用的叫做comparatorcomparator这个是比这个我们现在我们自己的这个verified proof慢一百倍的也就是说在我们刚开始的时候我们必须自己要造一个快的东西不然我没法跑我们造了大概十二十三个这一些这一些能够辅助这个link能够更好的去去去去执行的的不管是生成还是验证的的的这些工具然后我们知道说alpha proof用的是这个Monticolor Tree Search蒙蒂卡洛树搜索我们觉得这个太贵了我们看一下我们有多少钱我们觉得我们做不了这个蒙蒂卡罗树我们有得找别的办法这个最后其实和国内这个字节豆包感觉他们seedprover做的这个有点相似这个系统的这个design对我没有理解你为什么说你们公司更像SpaceX因为我们有很多的这些技术壁垒而其实某种程度上如何去训练一个模型当然说更高更快更强然后又有很多的一些大家的一些secret source我们这个问题可能在就是他遇到的这个科技挑战上时间会更长我们至少在种子轮的时候是觉得我们的R&D cycle是会拖得非常长的我们主要的这一个竞争对手我们当刚开始的时候是他们五分之一只容了他们五分之一的资产我们的估值也是他们的五分之一然后他们比我们早开始两年就是Tudor的这个公司然后他们用了两年的时间才到IMO的这个六道题里做了五道题我们觉得至少得花我们很长的一年半一年但我们没有想到说四个月我们就往这个普特南冲我们做出来一个满分然后接下来冲这个研究的一些问题其实都是世界各地的数学教授给这个小野肯老师他发邮件说就是以色列有一个Technion这个大学的LG Fel这个老师给Ken发了一个邮件然后这就是Falconjecture然后那个Ken Ribbit和Ken又有一些交流然后有这个Parshal Vendiver大为成这个波士顿的一个一个一个一个代数代数几何学家他他又有这个一篇文章反正就是我们其实某种程度上在很大的压缩这个时间这其实导致我们也有一些Infra上的一些债要还所以我们现在也有在还一些Infra的债小野肯老师对你们谈的来说是一个非常有标志性意义的人对他像是一个他的性格是一个高中的篮球队教练他的性格是一个就是他会给所有人就是加油助威让大家就是非常兴致勃勃的乐观向上的去去做我们手上的任务的这样的一个人是你找他还是他找你他是你之前老师对吧对他给我发了一封邮件结婚就你向任融资已经公布了对吧但是对但是11月我们之前就有邮件的一些就是交流你当时邀请他了吗没有不敢对吧我不敢我也不敢问叔伯我不太敢就是对叔伯自己告诉你他要来的其实我觉得融资也是这样我不太敢要钱就是我是我是说你我没有办法去说服你你只能自己说服自己如果你想做这件事我也想做这件事我们可以一起做这件事对但我不希望我万一开始引导你我有可能会误导你就是这个大家要大家都是成年人自己做一些有趣的选择然后一起去去承担这个选择的风险所以你跟舒博的过程更像是我我一直在告诉你我在创意的进展然后你等他自己说我要来我知道他是一个工业界元老毕竟你在director这个level上我觉得可能也有很多项目我怀疑交付的时间会是比较长的对在后面这个fear他后面就是这个组织很多的人都离开了对所以他是自己跟你说他要来对他是怎么跟你说的书包就是在Werf咖啡店说的他怎么说的呢他就说好多好的人都走了感觉这个地方不太像是以前的地方然后呢往后就是你要一起做吗我说好那个时候你已经荣当了对二月对吧对已经有一个offer了对然后他有跟你谈条件吗就正常吧就大家就是按照标准的来你当时什么心情我挺高兴的我觉得挺高兴的因为我觉得感觉一个人做这个事情比较孤单你有预感到他会来吗我有预感到但我们当时我当时想如果他来应该一年后来就我们可能我总觉得就是其实我现在对我们的公司现在的一些新加入的这些成员我总有一种就是我感觉我们就是我们希望我们能够把我们做的做的最好让我们能配得上他们的这种价值所以我当时想一年了这个可能做出来一些小成绩然后这个舒博可以来指点江山把我们就是往上再做一步 [129:59] 当然是这样一个想法那你的老师呢老师对他给我写了一封邮件11月底非常怪的一封邮件他大概意思说他要来湾区我说啊你要来湾区然后他说如果他加入了OpenAI或者是DeepMind的话我不应就是他希望我有一个心理准备然后我心想你要加入OpenAI和DeepMind那你为什么不来我这里然后我就说你可以来我这里然后这个时候你之前没有跟他说过这个话吗没有但我也就觉得你如果能够去加入OpenAI和DMine我觉得你可以来我们这里他说那句话是暗示你吗他是真的我觉得需要一些建议当时OpenAI可能给了他一个offer那为什么他说的是你要有心理准备就是因为我们知道他知道我有这样一个公司有可能会可能会有一些竞争关系OpenAI的AI for math的这样的一个Division可能和AXian会有一个战略竞争关系他可能作为我们的我们是朋友嘛他不希望我很突然的听到这一个消息就是他在给一个竞争对手进行工作所以他希望他能告诉我说可能这是他的一个选择也希望我能够理解然后我说那来action然后结果就谈得非常快非常好他是来玩具跟你谈的还是线上自用谈的没有就这么谈的我当时就是我当时飞得乱七八糟11月底12月从我是从这儿飞到了飞到了阿斯维加斯是Reinvent然后飞到了这个Neurips我们在那个Neurips赞助这个AI for Math的Workshop然后我们有一个就是活动可以就是招聘的一些活动我就在San DiegoSan Diego回来然后是这个就是一堆一堆事你怎么说服他呢在你那个zoom会上你说你对比open i你的优势是什么我当没sell他我就说我们非常的就是我们也open你来然后你可能还是得去open来看一看如果你能有时间来我们这边看一看结果他没时间来我们这边我觉得肯定凉了你想他来完去他就直接去open i然后就飞走了他没有在我们这那可能说明我们没有什么机会结果他来了他来你公司了他是来你公司跟你谈好的对他没有来我公司谈好就是他在zoom上我们就定了你截胡了open AI对你怎么说服他呢他被什么打动了呢我觉得首先他觉得我们的就是这个团队更数学这是一个事情就我怀疑发生的事情就是他去了OpenAI之后可能觉得那边比较做数学的同学不是特别多来我们这边的话可能有更多就是数学的一个氛围这个公司的DNA和专注点就是数学而不是一个general的AGI然后数学是其中一个部分可能更有marketing的成分小爷肯贝武认为是继承了拉马努金精神的现代数学家之一而且他之前说他根本不相信AI会超过自己然后后来他内心发生变化可能这是他联系你的一个契机我觉得是他有跟你说过他这个认知是怎么发生变化的吗他有说对然后我其实记得就是我们当时聊的特别的藏挫因为这就是一个截户多长时间就是两三天内OK因为那边那个offer要爆了就爆炸Explode了那我们这边我觉得还有一个很大的原因看加入是因为François ChartrandFrançois Chartrand是AI for数学的这个的2019年François和Gillian LampleMistrow的这个Chief Scientist Co-Founder他们一起写了一篇文章叫做Transformer可以在微积分上在integration上能够比一些像MathematicaMathLab这些电脑系统要电脑代数系统要做得好然后从那开始François就一篇又一篇的去做了非常多重要的工作去让这个AI解决各种各样的就是specialized的就是特殊的数学问题然后在AI for math这个领域里面我觉得就是Ken还有François他们肯定是对对方也非常信心相惜然后François作为我和Suber之后第三个来加入我们的就是我们这个团队的他们就有很多的共同语言然后事实上现在Ken加入之后又有Evan啊Kenny啊就变成了一个It's called a math club就是我们这里有一个数学俱乐部大家都有很多可以聊得来的东西然后他也给了我们这个action prover去解决哪一些问题选择这个问题给了很多很不错的建议我想多问一个关于小悦肯的问题他是个什么样的人他就是这个高中篮球教练他就是特别特别乐观特别特别就是让人你跟他聊你就会觉得 [134:59] 本来就很想做这件事情我现在更想做这件事情了所以他是我们特别好的一个文化上的一个增加然后他也是当然是一个非常好的数据学家他在这个划分函数领域里面就是非常年轻的做出来非常好的成就然后他也是一个很好的研究导师他带我做了很多文章然后还有很多其他他这个REU的同学都成为了不错的数学学者他是个直觉派的数学家吗这个我倒是不知道这是一个非常好的问题我觉得他应该比我更直觉派对但是我比如说我们就是合作的过程中像我一个合作者张胜彤他就是比肯定是比这个我和Kan他比我们两个都要直觉性所以就是Kan我觉得在二者之间Kan的这个我理解了Kan的这个神奇的能力在于他是理论建造者数学里面大概分两种一种叫解决问题者一种叫理论建造者他能够把不同的领域的东西去连接起来然后有一个完全全新的视角看一个问题他能够去发现很好的问题并且给其他可能更善于解题的同学们去做他会觉得他从学校放弃了终身教职加入一个学生创业的公司他会觉得有某种奇怪的感觉吗我没觉得我觉得Ken反正和我们两个都是比较就是叛逆的人对就是我觉得Ken这把这个他在数学教授他同时又是美国这个奥林匹克游泳队的这个教练去给他们分析这个游泳的数据怎么样去把表现更好的提升他又去拍这个好莱坞电影拍了拉马努金的那一部现在又要拍第二部拍这个米尔扎克哈尼的这个第一位女性菲尔兹奖得主的这个电影然后他同时又做很多的就是他有一个慈善基金会就是以拉马努金命名的去给一些很年轻的世界各地的希望能够拿一些资金去买数学课本的同学们一些辅助同时他又是美国美国数学学会的前任副主席然后又是在白宫又有一些政策上的咨询顾问的一些职位所以他是一个非常全面的人他作为一个数学家然后加入一个AI for math的公司介绍一个类似于AI数学家会替代自己吗他倒不觉得会替代自己我们其实大家都觉得我觉得他就是思想非常开明作为一个数学家有一些数学家可能真觉得就是AI去代替自己不是一件好事情但是我们见到的越来越多的比如说Kan比如说Andrew Granville那也是另外的一个很好的加拿大的一个数论家也这个Andrew也是我们他也是著作等身的一个数论学家他们其实一个想法就是随着AI的进步人类数学家会学习在不同的抽象层面上进行逻辑推理这是一个非常有意思的一个点就是我们某种程度上在编程这一块以前编程我记得如果你去这个计算机博物馆就在这附近以前就是电脑计算机就是有那个小卡片然后在那里打洞就是那个那是很早以前的一个Computer Science的一个雏形后面有一些更low level更低层的这些编译器语言然后一直后面到python现在倒可以拿自然语言进行webcoding编程然后数学其实某种程度上数学家也会学会有更高层的抽象的思维比如说我刚才讲的有可能他们就是去说这些问题是值得去探索的然后让AI去帮他们探索我们真心的希望我们的AI能够有具备一定程度上的猜想能力能够让猜想的部分与证明的部分进行某种向上落旋就是我希望它能够随着这个Action Prover能证明的东西越来越多我们每一天证明的东西都会进入到明天的明天的这个应用中不管是作为一个skill一个技能就像Lego Prover的skill library这个设计或者是去作为未来的这个训练数据我希望它一定是self improving的某种程度上self improvement甚至说你可以叫它continual learning当然这是一个最近很火的一个词一个bus word在一个能够有验证signal的验证信号的一个领域像数学来说是可以去试验的这些很好的很前沿的的AI的一些一些东西包括sub agentsskillsmcp这些东西全部可以在我们现在的这个数学作为一个操场一个playground上可以去试验嗯 [139:59] 你们在葡萄南的那个对那个故事可以给大家讲一下好就是大概就是在2025年12月6号这一天早上我们收到了就是葡萄南大学生数学竞赛当天的考卷然后我们是拿到那个考卷之后就我们要做的第一件事情就是我们需要把它变成形式化的这个题目让这个Action Prover我们的这个AI系统去做那我们这个题目当时其实挺有意思早上六道题下午六道题如果这个题目本身是一个正名题的话那么就可以直接就是把它变成形式化如果是他说要求解的话那还需要求解所以其实还是一个挺有意思的一个过程我们所有人都在这个办公室的一个庞嘉莱这个会议会议室是我们的这个war room我们的战争战争室我们就是在他们数学家有些人就在解题所以其实就是解题的这个过程还挺有意思的就是我们我们可以看到说有人类的解法和就是我们最终这个Action Prover产生的这个完全是不一样的一个事物我们在大概当天下午3点58分的时候我们是发现我们有八道题然后我们有八道题的话就是80分80分是一个什么水平80分一共120分去年的80分是世界前五然后但是往年他80分可能不是世界前五前十前二十差不多这样然后我们然后我们就希望能够拿到一个90分因为我们当时就有一个选择我们是否告诉世界我们做还是我们再等一等然后我们最终确实是有12道题就是全部满分然后这个过程还挺有意思当天我记得就在解题的时候就是小野肯教授他有在有一些非常有意思的精彩语录然后我和舒伯我们两个人就是笑的就是前前咬后喝他说不要在现在不是说数学纯粹之美的时刻不要去精确的去搞这些东西现在是战争状态就是在大家在求解的时候他就说能怎么快捷的去去做就怎么快捷的去做就得到那个数值后未进这个Action Proof也其实是和IMO的这个其他的这个标准是一样的就是说如果有需要求这个解法的题把这个数就是一块的未进去因为Lin只能做证明嘛他不能够帮你说是去求解所以求解是人做的是吗求解这个东西是人做的求解在IMO的那个就是IMO的那个考试中甚至是2024年其实这是alpha proof他给的先例就是有六道IMO题然后有一些题要求有一个得数这个得数的话就是要把它一块放进去变成一个证明但是后面我们发现一件事情就是我们其实可以不求解就我们其实因为我们这个系统里面也有一些就是informal的这个model其实我们是可以直接让他就是做出这个解法的最后其实我们发现我们的每一道普通男的题其实我们并不需要做人类求解那一步但我们以为我们要求解所以它挺有意思的小小也很小说为什么说现在是战事状态因为就是时间紧就是我们大概估计说一般早上六道题下午六道题加在一块十二道题最多不超过三道题需要求解因为确实是少数的大部分还是证明题早上那道试卷下来就是六道题四道题要求解然后我们当时只有就是能做得动这个数学题的人就是基本上就是我普特南成绩也不怎么样反正基本上就只有艾文成然后艾文成就一个人在那里就是一道又一道题的做还是非常非常有意思的我们其他同学有些人就是在就是把这个数学题变成林然后看他自己其实也没有做出来多少道就是普特南的题因为就是研究型数学家和就是这种打竞赛在一个最最短时间内的还是很不一样的一个数学家的一个一个一个特性你们公司为什么叫原理啊啊我觉得AXIEM是非常美的词就我自己很小的时候有一本书就是叫数学天书中的证明就是说如果说上帝有一本书这本书里面会有哪些题数学天书中的证明就是说有一些这样非常好的数学结果我觉得就是公理给我的感受就是首先把它跟Lin这个形式化语言它是呼应的就是从一些有限的一些公理中可以推导出新的一些结果就像是有地基然后你在往上建高楼另外一个我觉得就是Axium这个词就我觉得很美它很数学它很克制它很理性它又很sharp反正我非常喜欢Axium这个词他就感觉来自那本田书对然后我们公司里名字开头是A的人也特别多我们Alex Alberto Arum反正一堆就名字开头是A的我们是Axium你觉得AI会把数学的历史推向一个新的阶段吗会我觉得会我觉得这是非常地让人激动人心的一件事情就是我随着这个 [144:59] 我们以前的这个世界能够做到比较顶尖的数学思维的人是很少的我们现在会成从一个mass pool到mass rich的社会我们会从一个数学数学的匮乏到数学的丰富的这个supply这个供给会爆炸这是一个让我个人来说非常激动的一个野心就是你想一下所有没有被解决的理论问题所有可能说是应用科学家们他们遇到的希望有一个数学家帮他们解决的问题全部可以解决就是一个时代的一个时代的我觉得一个可以被定义就是说指数级的数学发现的增长这个我觉得一定会发生然后数学家们会扮演一个什么样的角色数学家们我觉得会扮演的角色就是他们能够提供最好的直觉他们会是能够提供到0.01%的直觉说哪一些数学问题比起哪一些数学问题更值得我们去集中算力去解决就我可能会讲一个这个这部分会听起来显得我非常激进我觉得这个就好像说是很多不同领域的数学家他们比如说三四十个人或者说是十几二十个人会聚起来去谈论说我们的wish list我们未来希望的这些问题被解决然后这些问题的重要性这些问题的连接性也就是说如果你解决了这个你应该能够把这一些都解决这样的这一个过程可能会是他们的主要的数学工作然后实际上是由这个AI数学家去解决这些问题比如说如果我们这当然是两种情况我们人类有可能有有限的算力能够去我们人类决定花在数学的发现探索上另外一种情况是我们其实某种程度上有很多很多的算力我们可以花无限的算力在这个数学探索上这个当然也包括说比如说现在我们可能能够用更少的算力做更好的事情如果是有限的话数学家其实他们某种程度上就是这个资源分配者他们的直觉告诉我们说我们应该比如说200个H200花在这道题上8000个H200花在这个题上某种程度上算力就会成为去与这个数学家对于这个数学题的重要性某种程度上画一个等号这是个资源分配问题如果我们现在在一个无限算力的这样的一个一个情境下的话那就是像是那个The Miss Hasabi's那个Thinking Game思考游戏那个纪录片里面有一刻他在一个这样的一个会议室里面他说Offerfold已经就是做出来了他们刚拿了那个奖现在下一步是什么呢他的手下的一个一个科学家就说我们做一个平台吧让这些结构性生物学家可以去提交他们希望被折叠的这个蛋白我们折完了我们给他发回去Demis坐在这个桌子上他就问说有多少个蛋白然后他说有200个million两亿个蛋白然后Demis就把笔扔在桌子上然后就说结束会议吧就是fold everythingThat was a stupid idea那个平台为什么你去做一个平台呢你可以把所有的东西都折了如果我们在一个无限的算力上的情况下我们就要做这件事情我们要把所有能够人类想到的好奇的数学问题全部解决所有与应用科学家物理学家他们就是在意的一些问题比如说很有意思的一件事情中国剩余定理现在被MIT的这个Ela Fit去用在研究这个有多少个神经元能够叠起来这个Neural Capacity这个空间里能够有多少个神经元这样的一系列的研究中我们做梦也不会想到数论会与初等数论会与这个计算机神经科学理论神经科学产生关系另外一个例子比如现在整个的这个法律与经济这个这个文献都是啊两个人一个是斯坦福法学院的这个Mitro Polansky我当时上了他的law and economic法律经济 seminar然后另外的一个是Steven他是在这个MIT我忘了他的last name但他们两个人就有非常多的就是关于法律与经济怎么样去想比如说我有一个刑法有多少是用来让这个社会不要犯罪有多少是实际上是对这个人他个体的某种程度上的修正与惩罚这个过程可以拿就是微分方程就是有非常非常多的我在法学院的时候就是帮他算了挺多微分方程就是能够去解就是数学其实可以被应用在这个Ting Gower's Fair自讲他有一个非常著名的一个一个一个话就是为什么我们国家基金委什么的需要去继续给呃呃纯数学去提供这个经费呢是因为数学是一个生态系统你有纯数学你就有应用数学你这个纯数学你如果死了你应用数学也就没了你你可能确实觉得你作为一个呃一个政策上呃这些应用数学更与实际的这个市场啊与社会更有关系但是如果你不去做这些基础科学 [149:59] 当然这个也与其他就是学科比如说生物的基础科学也是一样的一个论点就是说你一定要去进行通过理论层面上的发现我认为从数学然后到code到这个编程去在软件层面上去做一些甚至就可以到real world testing实际世界上的一些验证数学和代码某种程度上是孪生兄弟Math is code and code is mathMath is code因为有一个叫做Curry Howard对应就是它是一个Lin就是基于这个我每一个数学证明可以变成一个一个计算机程序Code is math为什么因为Code现在我们发现为什么backend甚至是整个distributed system的webcoding没有办法做到像就是做一个网站这样这么好其实就是因为它有很多的一些没有办法backtrack没有办法做很好的就是hierarchical就是分级的这种拆解对这些能力其实某种程度上数学能够给到他然后数学和编码的这一对孪生兄弟是一个你能够在我们现在这个神类世界上有这个验证的验证信号的一个方面另外一个部分其实就是实际世界里的这个实验对吧比如我扔一个鸡蛋它的重力会到这个地上鸡蛋会碎就是这些实际世界里给我的reward所以我觉得我们的AGI的这个workview就是数学然后编程然后实际的这些reward testing然后everything else对你觉得在AI for math的领域会单身类似于XGBT时刻吗我觉得会然后我觉得就是如果有这样的一个TreatGVT时刻它不单只是数学它一定还会有一个就是coding代码的这样一个部分其实这个事情其实挺有意思就是我们做的这个东西很多人觉得是它对就是验证它有很大的这个意义然后对另外一些人觉得这个对超级智能或者说就是数学推理有很大的意义它其实某种程度上这两者是合一的这个我觉得比较就是这是一个可能不太明显的一个点就是我们我们是在做一个就是AI的一个数学家但是我们又同时是通过形式化证明就是加入进传统的比如说就是LM推理这里面去做的所以我们产生的这个输出是可以比如说几千行就是LIN的这个代码然后这个东西它完全可以就是自我验证如果我觉得有这样的一个Tradgbt时刻的话它某种程度上产品一定要加进来就是这是一个我觉得我们时刻警醒自己就是作为一个就是在把这个系统就是能力见到越好的时候其实要要记住就是说某一天这个东西一定是要尽快的去产品就是出货和落地这是一个点然后我其实觉得就是有一个GPT时刻然后前面可能一般有一个比如说有点像当时早期的时候大家说就是AlphaGo时刻其实我觉得AlphaGo时刻对我来说是两个时刻第一个时刻其实可能是这个Google DeepMind2024年拿到的这个28分银牌另外对我自己个人的一个AlphaGo时刻其实是在今年的就一月份的时候Axium它去能够Axium Prover证明像File ConjectureVendover Partial-Vendover Conjecture这些包括同时就是Deep Mind有一个那是一个非形式化的那是一个自然语言的一个它也证明了一些研究问题其实我觉得是这两个时刻吧一个是奥塞海数学一个是研究数学你觉得AFO Math它会沿用大语言模型的这一套整个的技术范式吗还是会在下面上面做新的创新我觉得就是它是一个很好的你想试什么试什么的一个环境就是我们的环境它是一个它是一个就是它是一个很好的一个设置就是你可以在上面去试你认为一些会成功的一些事情然后这个可能在别的一些没有那么clean的一个domain上不好做就是在我们这里我觉得我们可以做然后比如说我觉得差不多AI for math有一套范式对吧就是从DraftSketch and Proof开始2022年的一篇文章首先呢你让这个informal的模型给你列个提纲其次呢你把这个提纲变成formal的变成Lin的然后呢你再把这一些中间sorrysorry是Lin里面的一个一个tactic一个语法它这个sorry的意思就是说我这一块我不给你证但是你知道就是它一定是对的相当于是让你把它take it for granted的这样的一个第一步就是draft提纲informal第二步sketch这个提纲formal第三步proof把中间的sorry全填上其实填sorry有好几种方式可以填你可以拿这个AI去填你可以拿一个就是有neural network的你也可以通过一些 [154:59] 就是原来ATP的那一些纯规则的没有这个没有这个书贝斯的没有这个AI的这个去拿这些东西去填就是让他自动的比如说HammerLin里面有一个东西叫做Hammer就是Hammer就是顾名思义一个一个斧头斧头就是我一斧头下去这个sorry就没有了这个Lin这个Hammer的这个历史其实特别有意思很早以前其实有其他语言像Isabel是另外的一个定理证明的语言然后另外一个定理证明的语言叫做COQ后面改名叫ROCQ Rock他们就是有Hammer了就是说有一篇非常Match New Hammer它是我如果记得没有错的话它是Isabel的一个HammerLin里面一直没有一个Hammer直到我记得去年六月有一篇文章就是CMU的几个人出来一个Lin Hammer但是Lin的Hammer它并不足够它的这个就是功能并不够涵盖所有其他的Hammer的尝试所以大家就是我们当时就有跟Lin的这个创始人Leod Moral我们说Axium希望能够就是做一个就是我们给你basically我们给你赞助你能帮我们找人做一个全部开源的给所有社区的一个Lin Hammer后来这个他们可能是人力上就是不够人他们不是说没有这个资金所以这个事情没有做成但是到就是今年的时候有一个新的一个东西出来的叫做GRINDG-R-I-N-DGRIND其实某种程度上它能够解决很多的数学的问题我曾经见过一些其他的AI for Math数学公司他有做一些demo其实那些题你如果GRIND一下甚至他都能直接给你做出来这里面没有任何AI的一个成分我们觉得的这个世界是AI和这个formal verification两股力量合在一起去解决一道题就是能够用deterministic不上这种probabilistic概率性系统的我们就拿这些东西把它解决然后令里面自己能够做出什么样的抽象层能解决一些也能尽量解决一些他就是我觉得一个很好的一种系统设置就是说先是最简单的最便宜的能解决就就解决掉然后剩下的再去上这一些呃就比较大块的这些这些这些就是呃大约模型系统有某种让你觉得非常啊哈moment的时刻对我我觉得我们每天都是啊哈moment我觉得这个这个团队还是挺快的他们就是其实我觉得有们每天都是我觉得这个团队还是挺快的其实我觉得有几个东西我觉得可能是比较前沿可能其他人没有第一个就是你如果觉得Montecolo Tree Search这个蒙蒂卡罗搜索太费钱了就是效率太低了的话你有什么别的办法我们希望能够scale inference把inference这里就是去做大这个的一个我们觉得可以尝试的一个办法就是可以看一下Anthropic他有最近讲的一些subagents这样的一些方向其实我们觉得subagents用来做AI for math其实做得很好这个是一个然后David Silver和Richard Sutton他们写过这篇文章就是AI后半场Learning from experience从经历中进行学习这个东西其实某种程度上在一个数学题里什么是一个经历这个经历就是一个数据的trail一个一段到达你最终解决这个题目的这一个部分这个过程全部可以作为你的这个experience经历然后随着你能够让你的这一些subagents能够应用的skill而skill就是learning to use tool学会使用工具那随着这些种类选择种类变多你可以去做scaling learning from experience这些东西我觉得我们做的比较前沿这是这是一个一个我自己个人的一个aha moment所以一个数从比如说40个40个node40个顶点的一个一个一个数一个一个一个一个证明就可以把它转化成一个数这个数从40个我们已经现在scale到4000个就是它是一个更深更广的一个数这是第一个我觉得我们可能做的不错的一个点第二个我觉得有一个我们的aha moment其实是就是我们发现这个数学的这个定理证明的很好的一个AI theorem prover能够转化到它很强的代码验证能力对有一个我觉得就是在这个Varina benchmark上的是我们看到了一个让我们都很惊讶的一个事情然后同时可以生成代码和证明其实这是一个很有意思的事如果你想正常的一个代码是python然后证明是英语就是自然语言那如果你去做强化学习的话你相当于它指着你往两个地方走你到底是python做得好还是自然语言做得好那你如果说是你把证明语 [159:59] 两个目标函数把它就是聚拢起来你让你的这个代码和这个这个代码的证明它都是LIN或者说甚至代码不是LIN吧它是RUST它也是一个它也是一个就是LIN是Defendency Type Theory这个RUST是一个Strongly Type Language它可能就能够让它这个收拢反而能够能有更好的一个Verify Generation就是一边验证一边生成的这样的一个一个时刻这是我觉得第二个我觉得我自己觉得比较美的一个东西为了更好的理解AI for math能不能给大家讲一讲就是在你的心目中AI for math它在整个AI的大地图上它应该画在哪个地方能不能给大家一个miping好AI for math我觉得现在就是convert收敛到大家差不多其实是一个做法就是我先拿一个open source的一个开源的一个一个先讯好的一个模型比如说我拿这个quen或者我拿这个这个这个款的一个模型然后我在上面去做就是做后训练然后做后训练大家做法不一样有些人就直接上2L有些人是SFP然后2L然后最后做好了这样的一个一个model之后把它就是去可以说是放到一个系统里面去然后这个系统里面有各种各样的model有一些model还可以做一些就是非常specialized的一些东西然后这一个系统差不多它去call一些tools然后这些tools一些tools其实还蛮难做的就是要做很多一些lint的metaprogramming然后就整个的这一个这一个系统的这个设计有不同的方法我觉得差不多是现在是这样的一个大家其实都是差不多这么做然后我觉得还是有一点点不同可能我觉得我们和像Sig ProverHilber Prover的做法的比较类似然后我觉得好像是比如说Arsoto他和这个Alpha Proof以前的那个做法有点类似其实大概分两派然后基本上我们比如说就是邀请加入我们的同学的这个AI的这个过往的工作都是呃后训练呀就是强化学习呀然后就是做 reasoning做推理呀然后也有招一些做agents甚至swarm of agents的一些同学然后呃就是非常full stack的这个engineering skill也非常需要差不多是这样的一个一个东西我看到很多研究资料我会觉得如果AI format突破了他应该不会是只解决math的问题它应该是具有放话性的这个观点对吗对这是一个很有很有意思的点我觉得AI for math大家其实讲的一般讲一个核心科技叫做proving就是证明其实我觉得AI for math它能做的东西也就是说能达到一个更多用处的其实是一整套一整套东西我觉得你需要有一个非常好的一个prover一个证明的系统你需要有非常好的一个conjecture提出猜想能够提出数学问题的这样的一个AI然后其实某种程度上这一个能够证明的AI是你能够提出猜想的这个AI的reward就是我能够拿它去拿这个证明这个prover去做这个conjecture的这个reward signal其实有一篇文章叫Self-Place-Erem-Prover就是自我自对异对自对异然后这个其实是董克凡然后马腾宇他们就是这篇文章斯坦福利比格文章然后呢他其实其实是所有人开始想就是conjecture怎么做猜想的模型的这样的一个起步点猜想模型的难点是我不像证明模型我证明出来了就是一没证明出来就是零我没有这个reward了我怎么去说我这个猜想是好还是不好然后除了说拿这个能够证明的这个东西去做一个grounding去做一个去给他这个这个信号之外还需要加一些其他的东西比如说怎么知道你这个猜想是否在数学上是非常无意义的比如说你完全猜想出来了一个不是那么重要的东西就是一点也不重要我也不知道为什么你会让你的prover去证明这个结论那就可能会有一些东西叫Elegance FilterElegance Filter叫做去判断这东西是否优雅然后在这个STP这篇文章里面的这个优雅这个优雅不优雅是靠长度决定的就一个东西它的题目比起它的这个证明来说是长还是短这个是优雅不优雅然后但是这个感觉上就很粗糙因为他们其实他们的那个数据集是叫Lin Workbook是一个比较是高中数学的一个数据集完全这个东西如果做到更高级的比如说本科或者说是就是博士研究的的话你没有办法去靠就是长度来就是绝对作为一个唯一的一个优雅的一个过滤所以没有没有没有什么就是没有特别没有特别强的延展延展就是难度提高的时候这篇文章不足够嗯嗯所以就是怎么去做这个这个 [164:59] 这个猜想目前是一个我觉得比较就是前沿的一个研究问题然后这个猜想的这个猜想家和这个证明家他们俩就是要聊天他们俩就是通过就可以self improving就可以自我提升然后呢他们他们还有一个很重要的一个部分是叫做尤其是我们在做形式化数学证明叫做就是知识库这个知识库为什么很重要是因为大部分就是存在的数学在英语里面存在的数学或者在中文里面存在的数学它都不存在令里面它连定义都不在令里面所以说我需要一个很好的去需要两件事情第一个我需要能够很好的搜索我什么是已知的已经被证明的什么是需要被证明的然后或者说甚至说如果你让我证明一个东西我在已知的里面找到一个反例那我就直接可以证伪对吗然后另外一个需要的就是说把这一些好如烟海的数学转化为形式化的数据转化为形式化的数据的话这个过程就是我说的第二个核心科技叫做Auto Formalization它就不是证明了它是转化它这个转化其实某种程度上一是被忽略了因为大家比如说你如果证明了很多普特南的问题或者IMO的问题你就可以到推特上你就会说嗨我证明了我是一个非常伟大的AI数学家但是如果你只是把这个人类已经就是发现了的写好了的数学转化为了这个形式化的你会得到更少的这个赞美但是这个科技它其实比这个证明要更难至少是一样的难度我其实觉得是更难为什么更难就是如果说我要求比较严格我的输入是一个archive上的数学文章而我的输出要求是把这个数学文章里面所有的定理证明的这个对这一对东西变成LIN的这个代码成为了我的一个LIN的这个输出那我需要几步第一步我需要把这个文章变成拆分我要拆分出什么是什么是就是单个的定理和这个证明有一些文章它结构性的比较好拆但有一些文章一个大的证明里面可能能拆出好多东西这个东西如果拆的不够细的话拆的非常细的这个东西叫做什么叫blueprint蓝图陶哲轩呀还有说是就是Kevin Buzzard呀Alex Kontorovich这一些数学家们他们用人手写出过蓝图他们曾经就是在Polymath还有就是后面的一些大型的形式化的这个项目上他们人手写了这个蓝图之后去丢出去给全世界的本科的一些数学的这些学生去每个人领一个小任务然后所有这些人小任务加起来星星之火可以燎原就整个的这个东西就形式化就写好了然后如果你需要让一个计算机不管是AI还是一个就是Rubis的一个电脑系统去进行把一个从一个PDF一个archive PDF到这一个非常细的蓝图拆分譬如说20页的一个文章变成一个200页500页的这样的一个蓝图拆分使得我能够把这一些蓝图非常细化的东西转化为Lin的话这一步是非常难做的这个需要很强的这种就是分解这种分解推理能力然后所以这其实是一个难点然后所以我其实讲的这整个在AI for math这个岛屿上是一个证明家一个猜想家一个知识库然后这个转化的能力就是贯穿着他们的始终这是我们认为的这个科技愿景然后其实你就会问一个问题说这其实不就是翻译吗把英语翻译成这个LIN但实际上它是不是的因为比如说我把英语翻译成法语英语和法语他们多抽象其实是很类似的有多结构性或者多不结构性多松散多严谨它都是很类似的但是就是LIN作为一个跟Python更类似的一种一种计算机代码语言这个转化的过程尤其由于AI没有见过多少LIN现在全世界的LIN加起来没有多少的Token所以这是非常困难的转化回去叫Auto Informalization就是反方向的转化从LIN到英语这个反而是简单一些因为这个它见到了很多的英语但是这个的话比较难的难点就是你如何确定你转化回去的这个数学完全是正确的你如何确定它没有错误这个我们一般就是让它再转化成另一边就是做这种就是转化去转化回来再转化去看一步一样这个叫cycle consistency用这个方法来去做形式化语言和语言是什么关系形式化语言其实就像是像是比如说PythonPython然后它某种程度上你可以把它理解为 [169:59] 他有就是执行能力对吗他可以就是我可以跑他然后我跑他完之后就会看到一个goal那个goal就说我这证明是对的或者我看到一个报错就告诉我第几行出了一个问题如果说在哲学层面上一点的话其实我觉得数学作为英语的一个子集数学是英语比如数学这些里面的词吧比如说数学我表示一个定理我有这些英语的词汇他这些词汇所出现的distribution概率分布与英语语义里的是不一样的比如说在这个代数几何里面有一个词叫做germgermgerm在英语里面的意思是细菌我记得当时特别有意思在疫情的时候我学这个代数几何所以就是大家就开这个germ的玩笑就是这个germ它出现的这个概率分布它一定与英语里面的是不一样的所以某种程度上如果你希望AI在英语里面做数学这不是一个非常好的至少它绝对不是事情的全貌而如果你把这个数学转化为了代码的话其实我觉得就是他由于刚才我们讲的一些可验证性他其实我觉得更有道理我举一个例子比如说就是在这个LIN里面你如果去看他这个怎么一个程序是怎么写出来的其实还没有逻辑性的他这个他对一些逻辑推理的一些处理还比较好另他作为一个就是自动化自动化形式化证明语言他有一些兄弟姐妹他又有一些其他的这些语言比如说后甚至原来更老的一些SMTSAT对吗这些都是就是基于逻辑的这些就是证明语言然后我们现在这个世界上我们所有的芯片的一些验证基本上要用Cadence这个公司的JasperJasper是一个基于SMT的一个语言然后Jasper就有很多的局限性就会有一个很有意思的问题或者说我们可以头脑风暴如果全世界的SMT挣扎着的Struggle的SMT全部可以被另代替我们会是一个什么样的世界然后又另外的一层问题是Lin和Python之间的关系是什么样的其实我们就回到刚才的那一个点就是Lin可以去作为可以作为一些Python程序的验证其实还是挺有意思的我听下来我会有一个问题因为现在coding也很火对那用math作为手段和用coding作为手段去执行任务的区别会是什么呢对其实这是一个很好的问题他们某种程度上是互补就是coding的话它可以帮我计算出一个output可以帮我计算出一个输出然后数学的话某种程度上它可以帮我验证一个性质验证一个property我比如说你给我一个问题这个问题我可以拿一个编码的这个coding去给你解决我就给了你一个电脑程序然后呢但是然后我就需要去知道这程序写的对不对是否解决了你的问题我现在需要很多输入输出这就我的test cases如果这些test cases都可以不需要了直接我可以验证在我写的时候同时验证你的这个电脑程序真正解决了你要的这一个问题通过link那我觉得是一个非常非常全新的世界但是这里就会出现一个难点这个难点其实我喜欢拿正面的事情去讲我们相信的一件事情就是任何你能定义的你都能证明任何你能写出的或者是任何你能specify就是英语里面program specification任何你能表达的你都能执行这是我们对于coding未来的一个愿景就是这个事情的难点在于比如你告诉我你的这个问题我无法确定我是否能把它写成一个比较严丝合缝的一道在这个形式化语言里面的这一个这个题所以我其实其实这个可能讲的我不知道观众我可能讲的也不是特别好就是可能再去orient观众朋友们一点就是我觉得这个software verification是如下的一个布局你有一个program这个program就是你的这个电脑程序乘以这个specificationspecification就是你要达到的这个目的你的这个目标映射到verification condition就是验证条件乘以proof也就是这个证明而Action做的是这个proof的这个部分然后能够就是就是所以其实但是你要看就是program有对吧就是我们可以现在很多AI可以写很多的这些就是电脑程序这个specification反而变成了难点verification condition这个东西就是做这些形式化语言的这些他们给我们提供我们解决proof这中间差的就是这个specification任何你能 [174:59] 所以这个这个梦想就是像数学一样我举一个数学的例子任何我能写成一个数学问题的问题都会被证明在这个coding里面就是任何能够定义的都能够被被执行被作衰对被执行如果难点是specification它应该怎么解决这就是为什么说在这个数学里面这个猜想很难就是做这个conjecture猜想家这个块很难这就是这其实是难点定义与猜想是难点就是定义比如说比如说我们之前有一个很火的叫first proof的一个挑战有一些数学家他们跟上纽约时报就是讲说给AI出十道题这个open AI做了好像做了五道也不知道对不对然后这个deep mind做了六道好像是对的他们当然都是拿这个自然语言做的为什么比如说我们action就没有办法去参加这个挑战呢因为这十道题我甚至都没有办法把它转化成LIN的这个就题目我放不到LIN里面为什么我题目放不到LIN里面题目涉及了很多定义这些定义完全不在不在这一些就是Library不在这个MathLib里面然后我如果要去定义这些的话这一步目前机器很难做所以由于我无法定义导致我无法证明所以这是我目前觉得的第一个难点对然后在这个定义之上当然也就是这个命题对吧所以我们还是希望的一个未来当然一定是有局限性比如说我们知道就是从我们那两道没做出来的题比如floating point这个非常难做有一些就是计算机程序的这个任务非常难去拿我们这个link去进行验证但现在大家都有尝试去各种各样的方法让就是不能够验证的那一些那一些情况变得越来越少其实我问这个问题是想说AI format它是一个更垂直领域的一个AI的事情是的还是说它能够泛化成一种通用的智能它泛化会泛化的比你这个垂直感受到的效果更慢也更不那么戏剧化我觉得在垂直领域上我觉得你就是是有可能有一个cursor like moment的是你能够感到就是bang就是你能有那种感受然后某种程度上它和就是通用的智能有一些关系但在某一些情况下肯定是某种程度上他们还是在战斗的比如说我们发现就是数学做的好的AI这个跟人谈话就听起来非常傻就是好像这个这些这些这些这些性能是在互相互相斥的但是比如说从数学到代码生成从数学到这些就是代码芯片验证这些很明显是是转转化的你说这个Cursor-like moment它会是一种更产品化的moment它其实某种程度上我觉得是一个概念我觉得好的产品其实它是来源于一个比较深的一个概念就是1980年的时候我们知道1980年代Donald Neuss这个计算机学家他提出的是什么事情他提出的就是我希望让所有能够我希望让所有计算机科学家都能够wipe code整个所有的事情我能够像数学家一样在自然语言里面去做推理然后这个电脑就直接执行但不单只是我们现在讲的这个webcoding因为我们现在还有code review他希望能够把这一些直接代码直接到这个deployment直接可以ship然后我们目前可以在前端做但我们后端做不了整个的这个系统我们也很难webcode比如说我怎么webcode一个control flow我很难去很难去做这件事情这是这是一个一个一个梦想然后比如说你可以猜一猜第一个提出形式化证明的这个人是谁其实比这个Donald Nutt还要更早就是就是Alan Tulling他就是讲说我我就是希望我能够一边编程这个编程完全背后的这个逻辑不单只是就是这个逻辑和就是他完全能够与我的这一个想解决的问题完美的这个契合而不是依赖于有限个测试的这个输入输出对但是我这有限个输入输出对它其实是有它的有它的好处了你知道它能帮我什么吗它能够帮我去specification它可以帮我去做这个定义就是我比如说小军你给了我一道题让我去就是去编一个程比如你让我做一个排序我把这个排序的题怎么样从一个英语的题转化成一个在我这个lean里面的这样的一道题就是这个过程由于我还没有去解决出也没有去证明出这个Lin的这个命题我需要这些输入输出的东西来帮我去做一个验证的信号我在想因为Krissy这个Moment它是让很多不会编程的人也能够做的那你说的这个 [179:59] 领域的career moment是不是会让更多不会做这么高等数学的人也会做数学了呢我们可以用它做什么呢我们可以拿它比如说我们公司虽然有一些同学他们以前做过芯片硬件大部分同学没有做过芯片硬件我们现在可以去用link去证明芯片的性质所以它还是一个非常专业化的有一个专业们看见的人去做这个事情不是不是不是我们公司的就是一般的软件工程师可以去拿LIN去去知道一个芯片是对的对我觉得我表达有问题是我想说的是它还是一个非常有专业需求的一个事情对吧因为每个人都需要就可能更多人需要编编程但是并不是每个人都需要去证明一个芯片的性能我觉得就是在一些芯片的领域上由于可能说之前做不到可能之前的解法是这个SMT这个就是基于SMT的解法做不到我觉得就是在我们比如说每一天就是更consumer更day to day或者prosumer的这样的这个市场上可以就是以下的一个想法就是你一边编程的时候你一边就是他告诉你整个编程不需要任何test case已经完全解决了这一个coding问题这个我觉得会是有意义的我只是觉得在这些芯片这些领域上他目前就是感觉这个痛点更大比如说这个亚马逊在过去的他有一个世界上最好的自动自动推理自动推理团队之一没有AI的就是那个那个纯就是他有很多的这个形式化语言的这些专家他们花了三到五年去写了26万行定理证明的这个代码去验证他们的这我实在不知道怎么说一个用于去最式化CPU处理的一个hypervisor一个工程工程的一个东西他的一个componentmemory记忆memory isolation component我不太会说这个中文他去确定这个东西写的是对的他花了三年人写了26万行这个完全这个AI没有改善这些工程师的生活AI没有改善那一些必须要手把手交着这些几千多个license的去验证芯片的这些人的生活我觉得就是可以在这些领域上你会有更好的pricing power你会有更好的定价格的这个空间作为我们这一个我们的公司这个提供方科技提供方但是我们觉得就是在更广泛的每一个人都要coding的这个情况下我们会意识到verified generation的重要性就你会希望某一天在我要一个call action要一个函数的时候他给你是百分之百不需要验证的还是所以这也算是你们之后可能会探索的商业模式我们觉得就是验证是我们最好的第一个市场这个市场会在什么时候打开你预计就是什么时候是你们要做商业的时候我觉得我们就是我们还是比较坚信说就是一个是专注就是说这一些比较顶尖的这些科技人才要继续把我们的这个系统的这个能力往前变强但我们同时又觉得说可以去开始进行这些小的探索尝试其实某种程度上就是你如果就是有更多的资源然后能够有更多的人在这个团队里能做的事情就可以越多所以我们其实我们还比较某种程度上有点好奇心驱动的去想这个商业模式我们其实还挺好奇这个东西它能证明哪一些芯片性质电路性质它不能够证明哪一些它能够去证明哪一些程序不能够证明哪一些我们其实更关注就是它不能做的这件事情然后其实我们觉得去解决一个有意义的失败比很多个肤浅的成功来的更有价值有时候在我们讨论大约模型的时候我们会说语言是模型的一个拐杖对数学是吗数学是然后没有之前大家把数学当语言了就是把数学当语言来做拐杖这个我觉得不对我觉得就是真的是要把数学变成另这个它就能够成为一个更更更更就是更另外的这样的一个很重要的一个拐杖所以它是独立于语言之外的数学跟语言应该是平行的关系某种程度上是的我们可以看到甚至在我们的系统里面就是更偏有一些问题更适合偏语言的解决比如说你列出这个提纲就是很大的一个部分的胜利那进度条就到了很多另外的比如说适合就纯粹的在这个形式化空间里面去证明它肯定是相辅相成的我们其实觉得挺有意思的一个点是一个就是一个形式化做得很好的一个一个一个墨性系统它能够比如说在这个芯片验证上做得比一个更多语言 [184:59] 要做得更好但是在一些其他的比如说这个通用的这个代码生成的这样的一个一个一个情况下嗯是我需要我也需要这个就是语言这一块因为我需要理解这个用户他可能无法自我表述的很清楚的需求我们觉得把这个语言的这个部分和这个另的这部分放在一块就有意思你们是基于大语言模型的吗我们这个系统里面有不同的模型这些模型他们一般就是经过了大语言模型之后的后续然后是以数学为主另为主以另为主就是输出都是另目标是输出就是另代码然后另代码他自己带了这个程序语言自己带了这个验证的这个性质所以就是这个有意思点就是假设我我什么都不懂密要学我完全不知道密要学是什么然后你写了一篇密要学的文章然后你把这个密要学的文章就是你写的英语的这个文章里面包括一些数学符号你打印了然后你给我看我是看不懂我也不知道你写的对不对但是呢你这个密钥学的文章可以通过Action Prover把它变成Lean然后我不需要看得懂我只要把它一跑我看到一个goal我就知道你这个密钥学的文章是对的这是一个很有意思的点它是一个很好证过程对我们我们接受了我们盲目的接受了这个非常强大的AI会犯错误但是我们相信在一些领域上这些错误将极度的昂贵我们相信能够去做一个尽量perfect的AI所以它能相对于就是在现有的AI之下它可以帮助解决幻觉的问题吗它对于帮助解决幻觉的问题解决所有的幻觉问题还是只能解决一个动作会有两种情况他要么就说这个事太难了我做不到要么他会给你一个正确的东西所以可能是语言是突破边界的那个数学是在把它往回收的那个约束他的其实某种程度上这个我其实觉得人类比如说好的直觉是什么好的直觉其实就是一个配比配比其实就是幻觉和这个这个规律规律推导的这个pattern matching和这个幻觉的一个配比这个会比较合适其实某种程度上语言能够做很好的conjecture这个猜想家我觉得其实跟语言它会有一些它会很需要借助一个很好的语言系统它可以帮你去突破这个边界然后这个某种程度上generation就是生成然后verification验证这两个就是一个来回的这样的一个过程但我们又有其他的方式可以去突破边界并不一定非是要语言模型比如说像François Chartrand和Alberto Averino他们这一个数学发现AI for mass discovery的这些工作他们是通过去找有意思的数学物品物品 object数学的东西去例子去尝试去找到一些直觉然后去把它变成一个猜想的比如说我有很多很多的图我可以让他再做一些就是Local本地和Global整个图全图的这些扰动我可以用这些方式去突破边界然后我甚至比如说另外一些方式做猜想我可以去看一下怎么样去做一个可以做embedding然后可以去做一些其他的方式可以去根据这个语言的这些相似性去反正有很多东西可以做但它确实是跟语言更相关然后而证明是跟证明其实跟两者都有关系你们接下来的一些就是想要达到的目标会是什么样的我们现在当它成阶梯式向前推进的时候我们希望能够我们也解决了一些研究问题我们解决了交换代数的代数几何的然后代数数论的然后还有是一个比较更理想数学比如组合概率意味的我们解决了这些问题我们希望能够选一些目前没有多少定义的这些领域比如我们希望能够看一下动力系统我们希望能看一下这种概率和随机曲面我们希望看一下没有基础建设的这些地方我们能不能去解决一些问题我们想知道这个前沿到底在哪里我们本来不知道我们大概两个月我们就把高中的那个基准级mini F2F这个也确实是一个比较古老也被打的千疮百孔估计不知道多少人训练在它上面训练的一个基准级就把它就是饱和了然后接下来饱和了普特南然后接下来就饱和了这个这个代码就是验证的这个基准级然后我们在研究层面上比较缺基准级说实话因为没有多少就是研究级数学的这个benchmark题不好找然后所以我们只能说找一些未解决的这些问题在每个领域找那么两三个试一试现在希望能找一些完全看起来没什么希望的领域这个可能花的时间会长一些我觉得接下来就是这个A论之后就是我觉得希望我们可能会更 [189:59] 多的往工程往研究上这里去转换可能解决一些光是工程没有办法不足以就是摘起来的这一些这一些low hanging fruit数学家的意义是不是在出题上他要数学家的意义很大程度很大程度我们的数学家的意义在出题上我觉得他们因为尤其你现在机器出题出的不怎么样刚才讲这个猜想家非常非常糟糕目前的表现所以就是确实需要人出题但出题非常难我们现在比如说我们要到哪里去找比如说八百刀就是未解的研究研究题呢你一个教授有这个题你是给给我们还是给他的这个学生呢就是这是一个非常复杂的一个过程所以我们也是希望能够去通过我们的数学家的网络去大家去看有没有题愿意给这个AI试一试吧你们想把它往哪个方向引导啊作为初题的我觉得它一定是要就是满足一个以下的这个性质就是他一定要就是robust to distribution shift就是说不管你是哪一个领域的这个他都能做一点他不能是一个只做因为你要是比如说只做欧视几何那你就是一个几何几何几何引擎对吧但是你希望他能够做更多的领域尤其是那一些目前没有基础定义的领域的数学题比如我想让这个东西去做一个代数数论代数数论里面的很多的东西其实都在这个Mathlib这个图书馆里面已经这个定义已经打好了我只要就是我就很容易的就可以去写出我的命题如果你连定义都没有譬如说在这个动力系统或者说是一些比较高级的组合它就没有这个定义我连这个题写都写不出来这就是这个first proof这十道题的这个挑战我们很难去甚至尝试的这样的一个问题目前这个能力那你可以说为什么就像你拿AI做猜想你能不能让AI去写定义呢AI写定义的能力他们这个社区管它叫library learning就是图书馆学习图书馆学习能力大概的意思就是说让这个机器能够去搭出一个图书馆也就是说从定义包括上面的定理包括上面的去证明这些定理然后去衍生出新的定理加更多的定义这个过程是一个建筑理论的这个过程这个蛮难的就是所以说Library Learning是一个大家目前可能卡在卡在这里的一个地方因为我也不知道这个定义我首先我很难给他验证信号我没有办法说这个定义是对还是错向我一个证明对这是一个一个点然后另外一个点就是是否是faithful的faithful的意思就是说是否与我这个人类给出的人类在数学里面已经创造出来的定义相同的如果未来这些人类的定义都已经被假设我们全世界的人类就是无穷猴子定理无限猴子定理我们什么都不干了我们就把人类的数学全部打成这些定义全部打进了假设就是上帝给了所有的已经存在的这个定义在令里面了就会出现一个问题就是当这个系统要做新的猜想与新的证明的时候他会发现我可能引入一些新的定义能够让我的生活变得更容易但是在这样的一个情况下如果那个定义是一个人类没有写过的一个定义的话我怎么样能够保证这个系统的这些定义不相违背因为我可以定义一个图是好图然后过了一会儿之后就会发现这个东西可能会呈现一个悖论在这样的一个情形下其实是比较棘手的对这些都是比较远较就是比较远的的研究问题但是我们最近我们会在想的事情如果AI for math实现了AGI你觉得它的标准是什么它能实现什么这个Demis它有一个非常Demis Hasabis它有一个非常著名的就是说你把这个AI训练到19101911看它能不能就是去发明发现广义相对论这是一个很有意思的一个定义首先我觉得我不太喜欢AGI这个词我觉得我们可能更是做ASI就是确实这个我们不能够去声称我们做的数学是general的数学它并不一定是那么general的它不一定能带来放话我是这样想的就是我是这样想的就是我们比如说有一个盘子其实我和之前的一个一个同学就是我和我和人工语聊过这件事就是中间你是一个点就是一加一等于二然后打印hello world所有的这些非常简单的这些任务在这个盘子我们当时还真在一个中餐馆这个盘子的外源是比如说证明黎曼猜想找出治疗癌症的秘方这个的方法然后写出一个像莎士比亚一样的或者说像 [194:59] 拿诺贝尔文学奖的著作所有的这些就是人类的超人类的任务就是有一些前沿的这些实验室像OpenAI他们他们想法说我一点一点的我要做AGIAGI什么意思就是我一点一点的把这个圆环称打最终我到我接触到了所有的边界我们不是我们是我们从这儿然后往这个证明黎曼猜想这儿打我们就往数学代表数学的这个超人类任务打打完了之后我们觉得它会发散出一个扇形就是可能说这有个代码验证这有个物理我是发散出一个扇形我绝对不会覆盖到这个拿诺贝尔文学奖这里但是我会有一个比较大的扇形而我这个大的扇形在我这个B2B的这个市场上是有意义的这是我们的一个想法所以我们觉得它是一个ASI其实人类的智能我定义AGI和ASIASI就是ASI我觉得是Specialized SuperintelligenceOK对对对然后HGI就是General当然S一般大家意思是Super Integra我觉得Super Intelligent就应该是Specialized这是我的一个Hotting那为什么呀听起来AAS应该在AGI之上那比如说我讲一个例子比如说就是我可能我数学还可以吧我自己都不会做饭洗衣服就是人类的这个智能也不一定多general那有没有可能AGI实现非常好他把你这个给取代了这有可能我觉得我会更快我觉得就我们现在看到比如说拿这个强化学习做到这个coding上我们看到了就是take off我们看到因为你拿强化学习能把coding做出来我觉得code verification我们在做的是很重要的一环所有这些东西做好之后就是你有这个基于你有既有这个数学去做这些algorithm的能力又有如果把猜想能做出来你就能够达到一件事情叫做recursive self-improvementrecursive self-improvement是一个我们包括很多其他人都非常相信的一件事情我相信这个大家也很熟悉就是说你就可以持续螺旋上升就是我希望你一个世界就是AI AI scientistAI AI engineer然后这个过程中我觉得AXION一定是其中一环但它肯定是但它不是整个的生产系统那是其中一环所以AI for math的尽头可能是一个AI for math是一个我觉得AI for math它比较哲学的一个看法是这样的就是AI for math能带来很多的东西它能够带来你非常的smart它也能带来你非常的right也就是说它既能够带来一个超人类的一个表现也就是我们可以看到甚至像OpenAI他们能够做的AI for math也做得很好但是另外一个很重要的是它能够给你grounding它能保证你的百分之百正确所以在这两个项线上再往上推然后我觉得AI for math是我们公司的这个DNA或者Math我们是我们的公司的DNA验证是第一个市场可能未来会有一个市场是AI for Science所有就是科学他们需要的这个理论Finding可能未来还会有一个市场是最实化就是最实化Optimization就是某种程度上我们经常讲一个词叫就是Diminishing Return就是说我花了很多的力气我最后就只有那么一点的收益所以不知道但这个世界其实很多程度上并不是Diminishing Return的反面是这种沉默性付出沉默性沉默性付出成本的反面是你最后花的你花了很多很多的力气你能够带来非常大的最后那一个mile会有非常大的一个收益某种程度上比如说能够去把所有的edge case边缘性情况都覆盖的搜索引擎比如说像google他就会赢得搜索的市场然后比如说像我们一些文艺工作者们他们能够就是好和非常好的这个区别是天差地别的所以在某种程度上我觉得像验证一个这种边缘情况很耗费很多的钱和人力很多这些资源和这种比如说最直化我需要目前大家花了很多的工业界的资源去探索这个小数点后1000位是什么比起小数点然后第三位是什么虽然在一些其他的情境下小数点第三位比小数点第一千位要有要有意义但某种程度上我们既需要我们是需要既需要这个median又需要这个outlier数学我觉得给了这样一种一种DNA我很好奇啊你们公司就是有数学家的公司和你那个竞争对手他不要数学家的公司他DNA区别或者什么我觉得我们公司既要数学家我们还要一个他们不要的就我们我们要很多就是代码生成的人就我们有很多就是编译期代码生成的这些同学我们其实我们相信多元产生智能其实有两句话是多元产生智能就两句话我比较相信一个就是降维打击另一个是多元智能就是我们觉得就是就是为什么我们比如说你刚才说AI for Math的意义是什么AI for Math它其实在探索推理的一些非常难的问题 [199:59] 各种程度上能够尤其说是泛化不如说是比如说你现在有你有一个吹脸一罩的这个这个这个自负串的这个这个趴虫趴虫的数据然后你很明显很难就是你你你你你你基本上通过就是就是就是这个规律的这个找寻能够做很多的事情了你很难撞墙你很难碰壁但如果在数学这一个就是目前令 data非常少的一个情况下你动不动就能够遇到一些就是蓝路虎所以你你你 hit 这些 roadblock 是更快的所以呃 某种程度上我觉得我们做一个更难的事情希望能够垂直下来给其他的一些领域就是某种程度上能够去去去去去去降维打击呃我讲这件事情的原因是比如说我们现在Ximprover能够生成一个20页的一个数学证明对吗但我然后我可以非常快的去验证一个目前在芯片验证领域是一个比较复杂的一个一个 puzzle因为那些需要的是一些比较可能说高中数学学生或者初中数学学生会的每一句法分离讨论而不是什么我想想啊不是什么numerical然后ike semi group对然后这是这是这是我的一个想法嗯哦我刚才说三个不好意思我说我说忘了一个就是三个这三三三个背景的人他们联联联合起来其实能有很多想法比如说AI和这个就是有这种compiler背景的人他们可以用一些方法去做很多的synthetic data generation去做这个合成不是合成不叫合成数据就是拿AI去生成这个Lin的Data而不是靠人去打这个Lin因为你想就是我去找一个数据提供家比如说Macor Touring这一些做这个数据商他们可能就整个平台25个专家然后可能Lin才打的不怎么样那我这个东西是没有办法去大规模的去做的所以我必须要拿AI去做那怎么样呢去做需要代码生成我可以用Fusing我可以用Repair我可以用就是Failure Categorizer我可以有很多很多的方式是这一些人能够给我们的不同的视角AI和数学这里当然也有很多我可以想就是正向推理反向推理就forward and backward conjecturing我可以去想很多一个数学家如何去有点像当时就是早期期类的expert system所有这些东西可以连在一起我觉得我们是一个idea rich的一个公司就我们有很多很多很好的想法然后我们人不够去执行它所以我们现在在我们12月份的时候当时Kent加入他第15号员工现在已经30人了竞争最少的人了不知道好像50到75吧还是比我们大好的对怎么理解数学是现实世界的沙盒数学是现实世界的沙盒因为你既有验证的这个信号又能够有更规律性的描述更结构性的数据某种程度上我比如说我们要在生活里咱们俩现在来想着猜想然后咱们俩再把这个猜想证明我好像只能想到一个数学猜想和数学证明不然的话我们可以说猜想一些生物的东西然后来一个实验室去做一些动物实验这个任何与现实世界更有关的这一些验证的过程其实可能会比数学的这一个比较简明的这个沙盒要困难和复杂的多也就是我为什么非常就是respect我的一些朋友们他们在做就是AI for科学的公司比如说Periodic LabsLanfetus他们在做然后原来是叫Future House现在叫Edison这个Sam Rodriguez也是我们MIT的这个校友他们在做就是一个一个AI Scientist很多很多人在做各种各样的这一些这一些尝试但是就是如果你想要很快的一个AI scientist很多很多人在做各种各样的这一些这一些尝试但是就是如果你想要很快的一个印刃然后你又希望又能计算又有逻辑我觉得数学和代码是好的选项对AI for science和AI for math它不是一个overlap的赛道对吗不太是我们能AI for science他们其实很多在比的是这个iteration circle这个有多快因为你想如果他们出现了WetLab出现了实验室我身边很多朋友有各种各样的实验室我的这个知道这个Lila这个Lila Science这个公司Jeff他们还有George Church在的那个公司他们有什么Robot实验室机器人实验室这个听起来非常的对非常的非常的非常的自动化但是他们所需要做的前期的投入是很多的Lim Fetus他们最近这个实验室又搞起来又有其他的一些实验室像Madra Michelle Lee他们都有很多的这些他们是一个赛道我们某种程度上如果他们有想要我们解决的一些理论上的一些问题我们希望能够帮他们解决但我们某种程度上只停留在一个数字世界我们不走到他们这个实际世界去但是你可以帮助AI science你也可以帮助代言模型其实你们是一个拐杖 [204:59] 工具对对我们我们觉得也不能算是拐我们是拐杖和工具比如说我们可以去验证他们生成的代码来帮他们减少幻觉这个蛮重要的我们可以去我希望的一个世界是每一个就是物理学家他们都有能够找到他们的理论物理学家就是我他们都能够每一个每一个神经神经科学就是做一些真正是动物实验的的人都能够找到他们的Ella Phi这些理论的这些计算神经科学学家而这些过去数学家们他们停留在比如说自己的学术圈子里面他们可能去很少的一些合作他们很少去与这些这些应用科学家进行合作我觉得未来就是希望能够AXIUM的AI数学家能够去帮这些AI for science的这一些科学的这一些探索去解决一些理论上的问题然后他们可以去进在实际的生活中去做验证你刚才说了很多AFMath它的验证能作为验证的手段对那它能有一天像一个如果你走形式化证明你就有验证如果你不走形式化证明你就没有验证你们现在走的是形式化证明我们走形式化那如果不走形式化证明它从往的是哪里呢不走形式化证明它可能是我觉得可以去尝试我觉得就是它可以尝试尝试一些怎么样做通用的推理吧我觉得AI for math有可能有一天像一个天才型的数学家一样提出非常好的问题有非常好的直觉他能成为那个创造的人吗这就是这个最最难做的这个部分但是我觉得可能我们和那个竞争对手的一个区别是我们打算做这件事他们不太打算他们好像直接要落地了他们落地成什么就是他们打算直接做这些商业的这个东西他们觉得IMO金牌可能就是就是这个终局了就是可以我们还是希望我们真的能希望把猜想做出来这个我觉得我们目前有很多的一些试验和探索然后也碰了碰了不少碰了一鼻子灰对但是我觉得这个事情碰了什么一鼻子灰就是有做不出来的情况比如说就失败了你这个失败到底是当时我记得这个失败发生的时候我们的这个正名家这个还做得不太好所以我们分不清到底是哪一块出了问题有很多的这些想法都可以去做但是我觉得我们要做这个猜想之前希望能够把我刚才说的这个核心科技二也就是把这个转化能够做好这个auto formalization把这个自然语言倒令这个转化我们希望能做好我们觉得能做好这个的话能够有更大的既是一个能拿更多数据的手段又本身能够对证明做一个很好的一个帮助然后我们才会去做这个猜想当然我们现在可能也在做一点但是就没有完全的ramp up没有说整个公司打猜想对猜想其实是什么数学最有魅力的地方是吗猜想其实是就比如我作为一个数学的一个学者我是很难我很难去提一个好的猜想然后比如说给到比如说假设说现在有一个reading course有一个本科的一个大一的同学希望能拿一道题对吧作为一个reading course最终的一个我觉得我很难给到这样一个题就我觉得需要猜想所需要的数学能力是蛮难的所以我们特别高兴就是Kent能够加入我们其实他是他是非常他是猜想家他是高产的猜想家他跟拉玛努金的关系是什么我听说的故事是这样的就是首先故事一就是他的父亲是当时一群要就是筹钱众筹给拉玛努金修这个在印度修这个雕像的数学家之一他的父亲是一个非常非常非常出名的著名的一个一个接触的一个数学家也是做数论然后当时是印度政府说是要给这个拉玛努金立一个雕像但最终没有实现于是这个拉玛努金的遗孀这个女士他就给这个拉玛努金的合作者世界各地数学家写信于是他们就是一起去做然后他还回了信就是建成这个雕像之后所以Ken的办公室里现在还有一个他父亲给他的这个这个留下来的就是拉玛努金的遗孀写的这一封信然后另外的故事二就是当Ken他是一个我印象中当他是一个本科生他好像是在芝加哥大学他当时就是有很多的社团活动然后可能课业呢也没有特别占据占据他所有的时间所以他的祭典也不是特别好然后他好像高中也没有毕业反正就是对反正就他就是一个非常叛逆的一个少年然后他的父亲就是拿拉完赌金的故事勉励他就任何时候开始也不算晚你不需要像你的这些已经上了多少数学课的同学一样你才能够做数学你完全可以自己现在去追赶上来于是他进入了他的这个数学 [209:59] 我是下木之后就开始非常非常努力然后就是做了很多非常好的数论研究对看的父亲也是前不久今年年头去年年底去世了所以也是非常值得纪念的一个数学数学代表之一他的兄弟们都非常的都非常的就是他来自一个数学学家他来自他的他的两个兄弟一个是著名的小提琴还是中提琴某个提琴家另外一个原来是密歇根大学的校长对他和拉玛努金都被认为是那种直觉型的数学家对不对我觉得就是拉玛努金是更尖锐的直觉型解题型然后而Ken我觉得他是擅长他提出猜想的方式是连接很多不同的视角他是一个发散性思维的人他不是那种嘿这就是一个公式这个东西一定是对的那是拉曼努金所以我在想如果AI做的是验证的这个事情是形式化数学那他其实训练的是一个更能验证的人而像拉曼努金这样的天才他能够被AI训练出来吗他会不会是两种类型这是一个很好的问题大家说拉马努金为什么就是essential AI也就是当时这个transformer paperattention is all you need你需要的只是注意力这个注意力机制这一篇文章的这个作者叫Ashish他有一个公司叫essentialessential是做pre-training先训练的一个公司他们先训练的一个模型就叫拉马努金人家说拉巴努金的那种浑然天成那种直觉其实是有可能是预训练的产物所以我们现在并没有做预训练我们现在主要做的是后训练我们有一天可能会做中训练但我们可能很确实你说的对就是拉巴努金并不一定是一个能够通过后训练诞生的一个数学家他是怎么预训练的他就是我不知道他不是他好像是有很多他的这个宗教仪式然后他原来是会计然后他在喜欢电影里面反正是拍他有时候祈祷的时候能够看到一些数学的其实我觉得对对对这个感觉没有办法就不是说我们能够后续练一个AI能够做到这样的但是拉巴努金到了这个剑桥之后他接触了就是证明他知道如何写证明了然后他就使得他的这个数学的这个影响有有更指数级的爆炸他有更多的呃更多的他想到的直觉他可以进行证明然后变成了新的直觉我们可以训练这个AI去证明所以说还是会对这个东西有帮助的嗯小野肯是后训练中训练还是预训练的场合他有说过这事这个不知道我肯定不是预训量的而且你看他的预训量好像不只是数学对我们现在大家的预训量也都是什么都有目前其实预训量我觉得能够去往下去就是做的能做很多东西我觉得预训量有大量的可以基于数据能够去走的研究方向但是只是某种程度上也没有大家没有在做比如说你觉得有哪些可能呢我觉得就是在就是你这个就是其实就是一些数据的一些我知道的就是怎么做的可能涉及一些其他公司的一些这个这个这个秘密所以可能不太能讲但我们也没有去很深的去想先训练的事比如我不做于训练对吧我们不做我们目前没有做的打算为什么你不做于训练呢太费钱然后我们也觉得大部分的另的这个东西可以从后训练甚至是我们会做一些我可能会做一些Mid Training那有一些人可能就把中训练化到这个预训练的一样了对其实我们确实是认同说是有一些基本的这个能力是需要通过预训练中训练来来来来来来提出的我能理解你们是一个创业公司你们要做的是AFOMAT那那些大厂OpenEye DeepMind包括DeepSeek自己他们为什么要做AFOMAT我听说的就是比如说Gemini就花了非常非常多的的想法在这个预训练在预训练上面然后他们的这个甚至说他们的甚至说有些有些公司会希望从LinData里面去希望能够买LinData去做一些预训练就我们现在的这一些形式化的数据甚至可以更多的在预训内他们要去做什么呢他们为什么要做他们是要做一个垂直的专家还是要做一个他们可能他们就是AGI他们就是general的就AI for math是一部分AI for math并不是每个就Gios没有对目前我觉得比如说OpenAI走的是informal这一个他其实是Kevin Wilder [214:59] 然后他的个人的科学雄心就是要做科学发现然后我好像就是Deep Mind里面有几个队伍同时在竞争做AI for Math有一个formal的队伍有一个informal的队伍XAI5不太确定有然后Anthoropic我觉得他们有但是只是作为只是作为帮助他们提高推理推理效果的就是说他比如说我有一道题吧一道数学题他先把它informal变成formal然后在lain里面验证完之后再回来提升他的推理分数但是并没有把这个作为一个专注点其实我觉得作为这个一个如果我是这些就是玩家之一的话并不一定会去做我们现在做的这件事情的原因是我一样的人才的这种这种高密度人才的队伍我可以把他们再继续在代码生成或者说在一些更红海的一些目前竞争咬得比较紧的领域去做得更深去把他们的护城河筑起来然后完全可以就是和我们或者是我们竞争对手这一些做得还可以的这些创业公司去进行去成为去合作然后这有点像比如说OpenAI他们就是会在搜索这一块会call EXA或者是call Parallel这些搜索做的比较好的公司所以你们这个行业现在目前是蓝海并不是蓝海我觉得这个东西是比较难比较难不太像蓝海其实也比如说就像是机器人的Foundation Model一般比如说派和skill的两家然后我觉得现在就是创业上就是我们和我们竞争对手两家就是估值也差不多总共融的也差不多一个新一点一个就是比我们两年前差不多是这样的一个状态对你来说挑战是什么呀执行的速度执行的速度与学习的速度我们现在会有一个对我个人来说我执行的越多我学习时间越少这是一个非常痛苦的一个过程就是你我以前可能说我每天有多少的时间能够用来阅读我现在可能少了这些时间但我又有那么多的事情需要执行所以某种程度上这是一个挣扎然后这个挣扎容易就是会我相信就是我们其他的一些很好的科技人才他们有类似的research和engineering ratio的一些挣扎就是一些trade off我们希望能够执行速度很快我们也希望探索商业模式的这一些从一个技术的角度去探索从技术和好奇心的角度去探索商业模式但同时我们要做的这些事情确实是挺多然后也困难还挺大的所以我们就是担心这个速度这是我觉得最大的一个苦恼因为我们现在是我们现在是七个月成立七个月的一家公司我觉得期待也由于这个A轮巴可能也期待比较大我们还是希望能够还是能够做长期主义的事情我们有点怕说是一个是怕执行的不够快另外一个是怕由于要执行的快导致焦虑导致这些就是方向上出一些战略错误对你来说实现A4Math的终点更重要还是说成为一个更成功的商业公司更重要我觉得作为一个就是Founder来说你对你的这个员工和早期团队你负有责任所以这不是一个某种程度上我觉得这不是一个这不是一个纯科学项目就是我们必须要成为一个一个一个一个能比较长的一个一个一个企业一个公司但与此同时我觉得这个公司的DNA就是登月其实我非常对我非常喜欢问社他们这个名字天哪这个名字简直是太好了这是这个公司的DNA如果我们就是太去逐利商业化的话我们会其实是一个平衡然后我们可以看一下我们竞争国对手的公司他们公司的起源其实是因为Robinhood的这个Founder CEO他可能现在还全职在Robinhood他可能希望有另外的一个让他感到比较有激情的生活有热情的这样的一个项目所以他们可能在早期的时候更讲这种科学雄心我们认为是我们认为是科学雄心然后但是我们我觉得理想的现实主义者和现实的理想主义者两种都是不错的不错的不错的这个这个这个落点但是不能是太远就不能是对有一天你们公司如果创业失败了你觉得可能会是什么样呢是因为什么我觉得这个事情其实挺有意思的就这个事情它的结果一定是极好或极坏就这个公司其实没有一个在中间的一个可能性当然要么登月成功了要么登月失败对就是登月成功登月失败某种程度上为什么说像SpaceX呢要么火箭发上去了要么火箭坠毁了可能火箭要坠毁几次才发上去可能每次都差 [219:59] 其实这是为什么我觉得就是像伊尔马斯克他作为一个就是企业家尤其你看他早期的时候还是一个非常锐意进取的一个值得学习的这样的一个企业家的一个模式比如说好几次就是贫死对马他的公司也只能两个留一个但是就是他很坚定的说Boss永远是羽羽雄长都要见得这样比如瑞达利尔在Principle里面也是这样我自己也是这样的一个认同我觉得这个公司是一个binary outcome然后我觉得如果我们是失败了或者我们很成功其实都是有可能发生的事情如果失败了你去干嘛这是一个非常好的问题我自己有一些个人的雄心对我看吧当数学家我觉得我可能会去希望看一看我觉得我那一年的神经科学的学习的一个心得就是我们基本不理解人脑我们完全不理解人脑我可能会希望做一些跟人脑相关的事情不是跟人脑就是跟神经科学相关的事情可能是动物呢我可能会希望看一下这些我觉得就是brain and machine interface的这个vision目前的implementation都不太足够就是人机交互的这个目前的选项我觉得太不理想你今天怎么看待硅谷这些模型公司的竞争啊不管是这些大的模型公司还是这些new了我前几天还在跟一个就是我的一个XI的朋友在讲其实为什么说为什么说我最后不想去做一个就是金融或者说是一个量化交易员呢你会出现一个问题就是你的你的你的英语书是一个短期内能够决定的一件事情我觉得这个事情是就像Peter Thiel讲的就是这个比较激进垄断导致创新竞争导致平庸这种竞争会导致平平会导致没有一些长远有一些很有长远想法的人他就要自己出来做做New Lab这其实New Lab的产生就是因为好奇心与创造力是我们人类的基本需求这就是因为可能说是在一些前沿的一些大的公司里面无法去做这一些满足他的burning passion的事情他就要出来然后我觉得可能是一个很有意思的点就是刚才说到这个好奇心为什么是人类的基本需求可以我们可以假设一件事情就是action prover非常的成功或者说是我们竞争对手的这个他们的非常成功反正就我们中有一方非常成功然后所有的数学题你给我一个千禧年问题我这个AI就把它全部解决了这个时候还会有数学家吗这是一个非常值得去思考的一件事情我答案就一定会有就是你给我一个一百万行令代码的一个我一定要去看里面是怎么做出来的你不让我去看我都会去看这就是人类的这个好奇心的体验体现由于这个证明最后被产生的方式这些去看懂了他的数学家又会有新的猜想新的想法这就是整个这个发明发现的这一个这一个循环其实就是就是然后就是AI做了可能AI做了这个发现让数学家更好的发明然后然后这种好奇心和这种探索的这种愿望意念是一个我觉得人类无法被压制住的一件事情所以说不管是现在是100 million1亿美元的大包也无法去压制住这一些青年研究者的好奇心所以他们就会去做出来我们看到做出来多么有意思的东西比如说Stefano Armand他们做了这个Diffusion Model更快更好的这个推理模型我们可以看到就是比如说就Periodic我们第一次把这些顶尖的这些AI人才就是去在一个就是现实世界他们要做这个material science这是一个非常有意思的一个方向他们不怕这些massive的这些data然后他们其实就是然后比如说我们看到有recursive他要做AI与这个硬件之间的这个AI提升硬件硬件提升AI这是非常有意思的一些方向我觉得这其实是一个这背后是一个基本作用力这个基本作用力就是人类的好奇心然后我觉得可能最有意思的点就是有些人说现在是一个泡沫吗还是说现在是登月就是有一些公司它成了它就登月了然后有一些公司登月了人家真的试了很努力大家真的是每一天996一块去朝那个梦想努力结果没成那就是泡沫其实我觉得就是我特别希望的一个 [224:59] 环境有点像我也知道说有一些好的学府的一个环境就是不怕失败MIT有一门课就是learning to fail你如何更好的失败就是单单这个每一个这种登月项目的失败它都会在资本市场上掀起联谊对吗我们会从这个就是私有市场一直到这个公开的市场会有会有连锁的反应你有你有可能说这是非常不负责任的就是为什么这个一些可能说pension fund一些大家的退休资金最终通过好几层的投资到了这个私有市场去给这一些有想法的研究者去满足他们的好奇心呢这是一个这是一个很我觉得很公平的一个问题但是就是如果说这一些好的有想法研究者不是由于他们自己的这种虚荣心或者说是我自己要占山为王不是由于ego而驱动的而是由于使命而驱动的所以导致他们不是碎片化的好几个比如同样的一个问题吧就是八个尝试他们真的就是在一块了他们从不同的背景不同的技能不同的这种不同的对于这同一个理想的解读聚起来了去朝这个东西我觉得这就是一个比较比较legit的比较比较靠谱的一个尝试我能理解这一波的NeoLab他们都有different的信仰也有不一样的Bets那当有一天他需要跟这些大的FrontierLab竞争的时候怎么应对这个竞争呢刚才我们说了你们AI format之间的竞争对吧那当你要遇到OpenAI你的竞争是DeepMind的时候你怎么竞争对我觉得这是一个非常好的问题我觉得首先第一个就是会有一些结构性的问题会导致如果说他们需要一个单位的创新是需要有多少单位的资源的而这个比例的话在一个早期的创业公司是非常高效率的这是第一点我觉得我们公司就是在做的一些事情我觉得可能在另外的一个环境会更难的去达成也就是为什么许多人从脸书来到了我们这个公司的原因然后这是一个点然后第二个点就是其实吧你作为一个underdog这个黑马你好像除了这个效率之外还有这个人才这个之外人才是人才密度因为毕竟他们会有更多的人才你没有什么资源能够和这些大的这些玩家抗衡但同时这更有意思的一件事情上是OpenAI曾经也是对着Google的那批黑马他也是那个就是在Google要把Elia就是最后counteroffer抢走的时候焦头烂额不知道怎么办的也是那个曾经也是对着Google的那匹黑马他也是那个就是在Google要把Elia就是最后counteroffer抢走的时候焦头烂额不知道怎么办的也是那个曾经一度发不出工资的这样的一个小玩家所以这其实是一个很有意思的一个点就是我觉得历史的钟摆来回摆动它就是大家螺旋上升但是又有很local的这种扰动某种程度上是有There is always a way这个东西我没有办法证明There is always a way就是你得信对然后信的可能就是喜欢加入早期创业公司的这一批人比如说Human's End这个公司最近融了很大的他们的这个co-founder是Google的第七号员工他到了现在的这样的一个人生阶段仍然认为好奇心是他就是所拥有的最珍贵的东西值得他倾家荡产你这么说我能理解很多包括我去跟赛宁聊他们其实有different band他们甚至是一个anti收集了一波anti的这个派别他们也非常反感这种剧烈的红海竞争然后觉得也阉割了研究员的创造性对其实是我是这样想的就是可以就是在一段在所有的这些就是local的扰动之后你看到的整个的这个宏观的这个局面是什么样的一个竞争的结果就是能力在飞速的上涨另外的一个结果就是好的且快速不只是好的好的且能快速验证是好的的东西被就是被做到最scale up的一个状态但是完全有一些可能可以时间长一点的东西没有被实现这是一个机会成本对但所以说竞争他也不能说不好他就是确实他这个让我们人类在这个AI的这个进步在非常短的时间内达到了一个一个非常高的一个一个一个进步速度嗯你刚才会说到你的自己的自我奖励机制从从团队里面获取这种能量变成了从事情中获得能量现在的你是从事情中还是从团队中现在我是从事情中现在我是从事情中然后但是我觉得团队是一个很好的一种它会给你一种安全感它会给你一种就是你有一个你有一个你有一个能落地你的脚还在地上它让你觉得grounded [229:59] 你事实上能够让你就是break out的那种那种冲动的那种能量有可能是愤怒有可能是有可能是悲伤有可能是就这种某着一口劲我就要去达到一个一个让我们这个队伍达到一个什么样的一个一个一个一个一个目标的这种的这个能量他不由团队中来他由事情的本身来嗯对那个让你最 burning的对终点是什么我觉得就是这个事情就讲起来就是有一个莱布尼茨他有一个想法他叫做Universal Representation Theory就是说所有你能够表示的这句话听起来很怪所有大部分你觉得能表示的东西你都能表示就是我觉得我目前非常期待一个让推理能力成为最顶尖的推理能力成为一个默认状态的一个这样的一个情况然后且是能够自我验证的推理能力这是我目前个人的一个理想其实就是有些时候就可能说人一辈子他能剩下什么有一些数学家他一辈子解决了一个非常困难的问题他被这个问题就是人们因为这个问题记住他他可能这个墓碑上就写着他解决了这个问题这一个人一生这一个问题你想这个加罗瓦21岁他就觉得我就挂了然后拉玛努金他是因为这个营养不良还有各种各样的身体疾病也早也三十几岁就挂了就人人类要多少人出一个加罗瓦多少人出一个拉玛努金然后你如果说是能够去用AI去复现这样的一种数学家然后你又有那么多已经存在的数学家能够与他互动然后去有新的这个这个这个就是Javance Paradox对吧就是就是这忘子我也不知道中文怎么说他的意思就是说当你把一个呃一个工具变得能够你做出来让它更便利更普遍的时候就会有更多的用处比如说我最近我们公司好久就是第一次找了一个找了一个能够帮我去处理一些呃每一天就是杂事的这样的一个一个一个一个同事他来了之后我们就是一块做的杂事反而变得更多了就是这其实就是Jewan's Paradox就是这些科学家这些物理的生物的化学的他们能够与这个AI加洛瓦或者说是所有的这些数学家总和他们能够有多少的科学的理论能够被被被被发明发现就数学家们和这些AI数学家能有多少数学的就是基础数学的这些东西被发明发现这其实我觉得这是我的一个你想从算盘到会计师就是当时是商务贸易从这个微积分到这个物理各种各样什么力学然后是thermodynamics就是然后到工业革命对吧然后从这个当时一个叫Babbage查理斯巴贝奇他这个能够去算这个log对数算得更快的一个babbage engine这是电脑的前身当时在哈代写我作为一个数学家我是一个数学家的道歉这个mathematicians apology好像不是这么翻译一个数学家的读白他就说我这个东西反正也没有任何的实际价值后面就有就密码学就有对吧我们看Victor Mueller他是一个他也是书博当时的同事也跟Axium很多的互动这个椭圆曲线基于椭圆曲线的密码学密钥学的就是就是泰斗之一的这样的一个人物他是一个纯数学的一个背景然后就是在在CS看了一眼然后就看出来了这样的一个一个理论这对于很多就是纯计算机的这一些同学们有非常大的一个价值这这这是终局但是有人说这个终局之后怎么办呢这个就不知道终局之后我觉得还是要我觉得其实就是钟摆的摆动又会卡但我觉得AI for math没有像AI模型被scale up一样被scale up而我们希望能做这样的一个人这样我们能知道天花板在哪我们可能又能回到research然后又能这样就是钟摆的来回摆动我见过很多的70后80后和90后的CEO也应该是第一个00后的CEO我不想就是画这种代季但是我还是很好奇就一个00后而且是女生的公司会和之前的这些公司或者是就有任何的不一样吗你觉得特点会是什么呢我这个对我这个其实是非常好的一个因为我自己最快乐的一个状态绝对不是CEO的状态我自己最快乐的状态 [234:59] 他就是我能够当一个research scientistinter为什么是inter呢就是这个我说的话如果比较愚蠢这个大家认为是正常的这是我最快乐的一个状态我是真的想做这件事然后我如果能够有另外的一个很明显我可以加入的一个地方我就会去加入他而不会把这个事情单独做起来所以这是我的一个舒适的一个状态所以我不太心理因为事情本身而创业并不是说你想当一个创业者而创业我特别不想当一个创业这个能理解对对我反正就是所以我不太吸引油这个可能大部分对所以就但也有时候有一次闹一个笑话就是我有一天特别就是想做这个Benchmark我想做一个就是好我不是说吗那个基准级就是到博士级别就很难搞我当时就把我们办公室有那个数学背景的同学们我就说我想搞这么一个东西我也不知道就是现在搞这个是不是优先序上是对的你们都是搞数学的你们要不跟我一块我们分一下就是你负责这个领域你负责这个领域每人找个二三十题然后完了之后我们这个之后我就后面就被我们那个一个比较元老的工程师就说了说你让这一些这个实习生的同学们就是还有这些比较年轻的工程师觉得这是一个非常重要的一个任务这和优先许是是相似的我说为什么是重要的任务呢我说这不就是一个side一个hobby的一个project吗他们说但是你是一个CEO所以你跟他们讲的时候他们就会觉得这是一个正儿八经的一件事我真的要去把这个当做我的前几件事情去做从那以后我就我就更hands off了所以就是这是一个非常非常有意思的一个事情还有什么不同吗你觉得可能和我觉得就是我觉得我我觉得我做这个CEO的一个好处就是这是一个technocross rule的一个公司就是我们的技术人员他们是整个公司的主干且和定向和锚点就是他们有可能由于我并没有一些strongly held beliefs所以导致我觉得我们就是很多ideas都可以被由于我没有一个特别我自己其实我有我有一些特别坚信的方向但是很多其他的一些就是很low level的一些东西就是一个bottoms of the culture所以我觉得这个公司的文化是一个是一个比较比较有意思的一个一个比较Pixar梦工厂对你们公司的会势都是用数学家来命名的有什么有特别的对对如果你想如果这个梦工厂或者迪士尼的这一个CEO是一个已经假设OK一个梦工厂的CEO已经是一个就是拍过多少个这个好好莱坞或者迪士尼的一个导演的这样的一个人做CEO这个地方就成为不了梦工厂为什么因为他们会觉得这个人是对的应该听卡的所以我觉得反而是这种Bottoms up的这种这种culture对创新来说是最好的需要一个intern对我觉得intern挺好的我非常愿意给Axian当intern你们的会议是有任何有意思的吗有对不同的名字他们就是叫做高斯 庞加莱希尔伯特Loveless还有土灵这个中间大家差点打起来因为怎么命名为什么差点打起来就大家喜欢的数学家不一样大家说你有了你有了这个你有了土灵你没有church这个不行然后你有了这个loveless你没有nother不行就是反正我们还接受到世界各地的邮件说为什么不把Emily Nother作为一个会议室我们说我们不好意思我们目前只有五个会议室后来是怎么选择取舍的好像是先就是我也不知道最后是怎么取舍大家反正就是还是在slack里面经过激烈的争辩大家认为庞加莱希尔伯特高斯这些都是polymath他们在数学里面不只会一个领域他们会好多好多领域所以拉马努金就是这么落选的他只会输论所以说就是大家要找这种就是我们觉得要是做一个AI数学家希望他什么领域都会没有distribution shift这样的一个问题所以要找这些polymath图灵是跨世纪的当然这个Sugo他也ly his body on the table说如果你不给其中一个叫图灵我就走了我说行行行那就是图灵然后完了之后我们希望能够有一个女数学家然后这个女数学家我们觉得loveless其实就是在Babbage Engine这里也不错这其中有你的偶像吗我的偶像是Goth他在对然后Punkery其实庞加莱和François Chartrand他们家里是他们都是法国人然后他们家里那个族谱还是连着为什么Goth是你的偶像为什么Goth是你的偶像 [239:59] 我想就是他是就是解题里面的天才对吗他这种他这些故事什么词规划求证时期变形然后包括就是我喜欢数论然后高斯在数论里面的这个都是非常基本的就是fundamental的一些贡献高斯比如二次互反律然后各种各样反正高斯在初等数论他有点像是我学数论刚开始的时候初等数论里面就好多高斯所以然后又他又是一个年轻数学小王子然后反正就整个我还是挺喜欢高斯的对如果可以穿越时空和历史上的任何一个数学家共进晚餐你希望选择谁你想问他什么问题我觉得就是去跟Erdol共进晚餐的话他给你讲的那些描述毕竟是组合学你晚餐这个就是table上能听懂然后Erdol是有又是那么一个就是peculiar非常古怪的一个有趣又古怪的一个性格古灵精怪的我觉得跟Erdol会共进晚餐会比较有意思另外一个我觉得我觉得跟Grozen Day共进晚餐的话如果不是我的话就是说另外一个人他跟Grozen Day共进晚餐应该意义会很大因为但是我这个代数几何学的不是特别好所以就是跟Grozn Dick就容易浪费这个宝贵的机会你看当你说到这些数学家的时候他们都是这么有趣的人对那如果有一天AFOMAP能做到所有数学家能做的事情会不会是一件很无聊的事情我有想过这个点我觉得我其实我一开始觉得是一个非常就是非常非常我当时觉得是可能会是一个我不希望让这个局面是一个非常遗憾的局面因为就是可以说数学家们他们之间的这种友谊他们的合作的这个关系他们的文化社区是一个非常有意思的一个文化就是比如说有一个数学家生日大家会给他办一个生日的一个峰会然后所有他的学生他的合作者们去轮流去讲一个这个人所做出来的数学的贡献或者是一个跟他们合作的一篇文章我曾经就是作为一个硕士生在这个牛津去过这个Roger Heath Brown的生日峰会然后像Ben Green James Mayer他们都在那里然后当时就觉得是非常的感动就是这是一个非常好的一个一种传统然后所以这人的这一个元素我觉得在数学中他永远不会被磨灭我觉得AI会把就是数学的很多很证明可能能够帮数学家们去很快速的解决但是这个猜想然后以及直觉以及构造以及这些方面我觉得数学家们仍然会有非常多的乐趣然后它仍然是他们会成为智力的灯塔对所以我们刚才说的那个当然这个也不一定我们能解决这个当然是有一时候你做做梦想着自己能把它解决了会不会反而是一个不太好的一个添加因为比如说这一些数学家们非常珍贵的这一些legacy他们的他们的对但是后来觉得他们就是会有更多的问题他们会难倒AI像他们已经在难倒AI一样做基准级他们会永远永远是智力上的挑战以及大家这种互动应该会很有意思所以我们刚才说的那个问题拉曼努金和做一个验证的AI他其实还是偏这边对吧偏验证他并不是那个天才型的选手对这个我觉得直觉就太难做了我觉得直觉可能五到十年有可能对但是我有一个很我有一个比较又有一个比较激进的一个一个想法就是我觉得大家现在如果看有多少解析数论里面的问题是被一遍又一遍的在一包很标准的证明方法里面去抽抽这个证明牌就是就就一个牌一个卡牌一个卡牌一个卡牌就这么重复的熟练的去运用比如说我看这个major arc minor archardy little 圆法这个circle method就能解决一些一些就是bonding的就是上线下线这些这些方式解决一些一些概率法解决一些然后比如说你去上筛法又能解决一些筛法也在被就是有一些人他们不解决任何问题在提升筛法能做的筛法作为一个工具我觉得就是已经能有的这一些工具能解决很多很多的问题然后我们会说一个人直觉很好可能是他很快的能够想到怎么样去重复的我们现在讲的这种直觉我可能讲的是说给大家一个完全不同的一种一种一种一种方法和机制这个我觉得是 [244:59] 五到十年你有过一个说法就是说热爱数学就是看到了上帝的面容为什么会说这句话我是这么觉得的就是我很小的时候就觉得说有一些有一些基本的这些真理然后我觉得数学家科学家他们存在的这个意义之一当然就是去把这一些东西进行发现和探索其实我这是我16岁我曾经写过一篇文章我当时是这么至少是这么想的然后后面就是林耀开这个就是创立这个Action的时候就是不是说老跑步吗早上斯坦福大有一个那个就是教堂叫Memorial Church这是就是纪念教堂然后如果你去从那个就是我们Pawato这边往那跑然后如果平常我都是绕着跑因为就是特别晒那一天就是往这个草坪底下去跑然后就是突然我就在那个教堂的下面了然后当时那个阳光也特别好然后那个教堂上有壁画有天使十字架其实有那么一点spiritual的一种感觉一点灵魂的这个感觉就是觉得可能说如果那个就是一个人的这个木质碑上可能印了一个他曾经证明出来的这个事情是他的智力遗产那么如果能够让这个东西乘以一亿你会不做吗可能不会所以当时有这么一个想法当然这个我觉得也自己就这是一个出于ego的一个想法就是说我可能说想我这个公司能够去作为这样的一个AI for math的一个unlock这个想就是我希望登月也希望登月的是我们这个肯定是出自于一点这种这种ego或者是就是自私的雄心壮志但是总体上这个事情我是非常希望它会实现的对就算我们是失败了可能要谁其他人登上去了也是一件好事虽然你现在还很小问你这个问题好像不太好但是还是想问你希望你的墓质背上写的是什么呢你是希望你是一个数学家还是一个就别写其实我是一个比较就是觉得体验比较重要的人我反正要活过了我也有体验这个就无所谓我都不知道我要有什么物质背不重要就不重要你会希望你自己是一个数学家吗也不重要不重要我觉得我曾经是觉得很重要的这是这是这是我曾经觉得就是我一想到我可能就没有办法成为一个数学家我有时候一开始我就还哭就我我还是一个比较比较比较emotional有时候会有这种创业的时候对对对那个时候是是这么觉得啊然后后来觉得其实就是我想当学徒对我其实哎对其实就是你要非写一个什么就写学徒就是我想去呃在尽量多的一些智力领域上能尽量多的去学一些东西比如说这为什么你看我跳来跳去就是数学然后跳物理为什么又跳物理因为我高中初中物理可差呢我想着怎么着学一下吧然后去学点神经科学也学的生物那一块学的不怎么样但是我觉得跳这个计算神经科学学的挺有意思然后AI挺有意思然后学学这个量化交易前沿在XTX真的是很感谢那段经历然后又去学学法律然后法律喜欢各种各样的从反垄断by the way反垄断是一个非常就是antitrust是一个非常就是像树状的一个逻辑的一个一个非常非常像数学的一个学科合同法也是然后又有那种完全不像数学的比如宪法就是宪法其实这个这个或者说是这种民事诉讼这些就是庭审这个最初级的庭审这些都是讲故事的一些一些这个这个这个领域然后呢就是所以我还是希望能去学很多的东西就我觉得AI for math其实对我来说我人生最快乐的时候是我拿到那个我找到那个GitHub的那个link然后我把这里面的那个文章的Apps全读过一遍那是我人生最快乐的几个月然后那个时候最快乐的几个月那个时候Shubo就跟我一块在读然后现在跟Shubo一起做然后当时最快乐几个月那些作者他们陆续加入了AXIA我们现在有如果你说前30篇AI for math的文章我们就是大部分都是作者都在我们的AXIA这里所以又他们就是每天和你就是一块去去冲这些目标的战友又觉得非常的快乐其实我觉得就是这可能是不错的一个定理你现在是什么的学徒我现在是怎么能够让一个一般来说创业公司都会死掉怎么样不死的一个学徒一个创业者的学徒一个一个创业者这个词听起来太好了就是就是创业公司99%他都会死掉所以就是怎么我现在是就是Don't Die这个Brian Johnson有一个好玩的Don't Die Movement我现在是Don't Die的学徒你看你的第一个自我奖励的方式是通过人来获得的第二个是通过实验 [249:59] 来获得的你说你今天今天钟白已经到了事情这一边但是人能给你提供一个安全店让你觉得grounded对那有一天你作为CEO当这两个事情发生冲突了对冲突过呀这个冲突过我们也开过实习生对就是我们也冲突过但就是这个事情我觉得就是你任何的乐观主义收起来你要谨慎的做决定你要想很久就是因为毕竟是要对就是可能人就是要负责然后但同时我有另外一边就是很多时候你觉得为什么要想很久是很多时候你觉得人与事冲突了的时候其实是你自己不够好就是你可能这个人可能都跟你关系很远但是你总是有一些由于你自己技能点和能力的问题是能够让这两个事情不发生冲突的就是他走到冲突的那一刻一定是因为你自己本身曾经有做过一些错误的决定就算这个人可能是一个你不认识的如果公司很大这是不认识的员工他一定是有一些管理层的一个决策他一步一步的进头trickle down到出现了这样的一个问题嗯所以我还是比较相信一个词叫authorship就是authorship就是作者就是你是你自己人生篇章的书写者和作者所以你你不能够有觉得是可能不能够觉得说就是一个情境他就能够决定你的一个决定是你决定让这个情境决定你的决定的所以你也可以决定用其他一些方法去使这个情境不要这么糟我是这么想那我们最后还有一些小问题我们会让每个嘉宾给我们的观众推荐一本人生之书你会推荐哪一本他要真的对你人生产生过很重要的影响他不能是数学书你也可以说是数学书数学书的话如果是年龄比较小的观众我推荐初等书论里面对书论讲的真的是很好如果是数学书其他数学书我觉得戴文波的那本分析书论我觉得很好然后对我还是比较喜欢书论如果不是数学书的话我是那个我挺喜欢红楼梦的就是我确实是挺喜欢红楼梦的甚至是红楼梦很多学者他们去研究红楼梦这个是一个曾经在我小时候对我比较有震动的一本书然后刚才也讲到大雅宝互动家二号对我人生产生影响比较大的其实有挺多关于一些企业家的一些故事比如说伊隆马斯克的故事就是说还是他之前的一个人太太他讲的是他晚上睡不着翻来覆去然后就痛苦的咆嚼马斯克痛苦的咆嚼然后包括说是一些其他的说是华人心说就是pain and suffering这些东西我觉得就是由于就是可能看到过他们的这些故事会让你有些时候比较难的一些感觉像嚼玻璃的日子里面会觉得这就是一个正常的一件事情你觉得现在训AI跟你当年训自己有什么不一样这是一个很好的问题对我觉得有时候你会觉得有点像比如说就是看到他这个表现刚刚好了一点马上给他更难的提这种curriculum sampling对吧这是一个很有意思的一个事情比如说让他能够去给他比如说看到他做Bluforce的时候又觉得是跟自己曾经的数学家的感受有点像没有说特别应该有区别但我目前没有特别能够想得起来的点就是你感觉你看到相似的时候你就会特别有这个你的大脑里的神经元就在发人假设AXM的AI在未来证明某个重大的猜想但在证明过程中使用了一个新的公理这个公理不是现有数学的一部分但是看起来非常的合理你会接受这个证明吗能想象到所有的数学家们就是感觉世界末日了一个思想实验我们看到了AI在尝试用各种各样奇怪的功力去帮他作弊这个事情已经发生了对吗就是我刚才讲的其实这个事情Deep Seek还为此受害他当时说Deep Seek Prover我忘了是哪一个version说做出来了Penit and Bench上的当时600多大碰碳本上的题就是Sota在各位数然后那个Deep Seek说我们做出来了49道事实上只做出来47道有两道题其实就是这个这个AI在作弊我觉得如果这个公理大家觉得是自然的大家就会接受它但是这个事情我觉得就可能是一个大家以前没有探索的很足够的数学领域不然的话你可能会认为存在机合理或者不存在机不合理这个公理可能已经被假设了所以可能是到了一个有点像 [254:59] 我们看代数几何混这个组合除了均和的这个代数组合学这个我们可能未来有一个我瞎说啊probabilistic analytic这个真的是瞎说可能我们未来有一些就是混的混了好几个领域的这样的一个东西大家再往里面加东西我觉得就是是可以按照接受和不接受两个世界照样去运作的当然你这个branching factor现在是二你如果继续这样你就会有无限多个世界然后就会一团混乱然后有一天大家可能就会说回收我们把它Titan但这个其实是事件某种程度上是一个人类文明的一些构造所以我觉得大家是可以的就比起比如说物理你要加一个什么定律这个可能大家会觉得其实还就更不可接受一些其实挺有意气的刚才我们其实也谈到DeepSeek你会怎么看中国AI现在的发展包括DeepSeek包括字节包括KidneyMinimax等等公司你觉得在未来的AI宇宙里中美会是什么样的关系和角色我很respect就是这些中国的这个AI玩家就是比如说我很我很诚实的说我觉得就是豆包他们做AI for my soul非常的好非常的好然后他们也是非常短的时间非常执行力强的一个团队跟他们的一些同学比如说袁正跟他们聊过就是非常好的一个团队我觉得就是他们然后他们可能会选择或者选择部发一些文章然后我觉得就是这些ideas可以就是流通还是挺挺好的对但是当然大家可能最核心的一些东西还是会可能不在文章里写然后可能会做一些他们没写什么的deciple但是就我还是觉得如果是要做纯粹的科学与创新的话就是稍微往学术一点就是少一点就那种商业的一些顾忌多一点学术的就是信任与纯真我觉得是好的一个希望大家一起啊是一个好的就是工业界的一个practice对中美呢中美的话我也不知道就是我觉得好多反正人才不分世界对吧但大家可能有就是有些同学愿意在中国生活有些同学愿意在美国生活之类的就不知道你觉得2026年你对AI发展会有哪些语气2026年我觉得大家应该能把这个会看到很快我觉得我们能看到第一个continual learning的一个小模型我觉得我们很快能够去看到一个非常好的multimodal reasoning model我们很快所有的这些就是什么agent economics全部会被scale up我觉得我有一些个人大胆的预测我觉得很好值得做的一个orchestrator是很好值得做的然后我觉得sub agents刚才讲过是很好继续做的哦我觉得formal verification tooling应该作为RL reward完全是underexplored这个和我们做的也很有关系对你刚才说的第一个和第二个分别你说的是被谁做出来第一个continual learning持续学习我知道有一些不错的团队我感觉他们很快能出model是小公司还是大公司小公司全是小公司都是new lab都是new labmulti model也是吗multi model也是new lab他们应该很快就会就是很快就会问世了在Styles的一个公司也是我的好朋友对当时也希望他能来加入action最后祝福他一些快问快答一个全球范围内你喜欢的食物全球范围内喜欢的食物喜欢就是寿司任何的寿司一个全球范围内你喜欢的地点喜欢地点吸你为什么我小时候第一次出国是去吸你一个少有人知道但是必须知道的知识点可能是一个冷知识你可以自己打CP你最近对于生活的一个非常新鲜的鲜活的认知是什么或者体验可能我最近过得也不是特别鲜活我每天早上就是几点钟起来然后一直工作到晚上几点我鲜活的认知是什么或者体验可能我最近过的也不是特别鲜活我每天早上就是几点钟起来然后一直工作到晚上几点鲜活的认知和体验就是我觉得还是每一次我去就是在跟就是心希望能加入AXIENT的同学聊的时候就会觉得未来无限好未来无限希望然后觉得感觉到那种自己曾经做这件事情的初心并没有因为就是反复日复一日的执行感觉被打磨掉就是觉得非常的快乐感觉像是两只鲸鱼又在找到了彼此的这个聊天频率这个还是挺好的所以招人是一个我非常快乐的事情鲸鱼找到了自己的聊天对就是有些鲸鱼它那个就是频率跟别的鲸鱼不一样然后如果说你遇到一个人然后你们都以前是学数学的然后可能你们现在都对AI for math有一些理解但你们又同时有一些新的理解然后你们聊一些东西的时候还挺有意思另外一个我觉得比较鲜活的体验是我们就是发现非常多了古老的一些技巧对我们现在的这个比较前沿的研究有这个有这个有指导的价值然后这个有点像这个24视频它有一个叫如将不进与谷为新还是挺有意思的每一次有这种callback我觉得特别有意思像世界是一个世界是一个云我们又回到了原点你心目中影响AI进程的 [259:59] 我觉得第一篇我觉得是其实是Christian Zagady的那个白皮书Christian Zagady的那个白皮书都不是论文就是他想未来应该是什么样的这是第一篇第二篇我觉得是可以看Gilliam Lampel和François Charton的那个就是发现说可以去让Transformer去做一些一些Task然后后面当然这一篇论文是他们开始很多的尝试后来拿这个东西去找其他的构造第三篇这个讲过了第四篇其实我就是一堆bundle就是从Kiminaprover到DeepseedproverGodoprover一和二SeedproverHilbertprover所有的这些就是真的在拿RL把它做起来了的因为我们刚开始的时候连就是从来没有一个RL做的formalprover我们刚开始的时候连这个都没有我们在融资和这个做这个法律使得这个钱到账的这个过程中出现了Kiminaprover基于当下的认知一个你最关键重要的大词是什么我bet system我不bet model我bet就是这个system有非常多的事情可以做然后包括orchestrator然后我另外的一个基于与这个又相关的一个bet就是我完全相信recursive self-improvement是很快就能够做出来的然后有一个问题就是如果你做出来之后就是然后呢你是然后做什么这个东西就是能否就是我觉得可能会出现一个这个需要一些forward deployment的一些东西我觉得forward deployment的东西还没有在AI的时代得到一个革新让我觉得传统下次会死我们工作室叫做语言及世界工作室当你第一次看到这个名字的时候你会想些什么我第一次看到这个的时候我想的就是说我觉得数学家们他们在几千年和或者几千年几百年他们都是在拿英语写代码或者说拿中文写就拿他们的那个本国语言写代码就是他们在进行的是逻辑的推理但是他们是在自然语言里面去进行的逻辑推理这是一个让我觉得非常神奇的一件事情然后由于这个特质现在我们可以看到说是比如说就是做这个计算机的同学们可以拿自然语言去写代码但数学家已经做了就是几千年了所以数学它所有带来的这一些结构啊这一些逻辑为什么说和这个代码验证他有帮助其实是有这样一个特性这是我当时在想的一件事情然后另外我在想的一件事情就是说如果你去把这个世界想象成一个manifold一个比较高维的这样的一个几何错谱的一个流行你这个语言它这个带来的或者说是基于tax-based的就是next token prediction这个AI它到底在这个上面有多少探索了多少然后又flatten了哪些呢我反正就在我曾经有一段时间在想这个因为我在想怎么调loss function但是这是我的一些感受