Hello，大家好，我是小俊。今天我们来到了美国硅谷，此刻正在扎克伯格最早的创业所在地 Facebook House。这是一栋外表为淡蓝色的可爱的小房子，而今天也将迎来商业访谈录最年轻的一位嘉宾，她是一位零零后的华人女孩，名字叫洪乐潼。她的探索方向是 AI for Math。所创办的公司 Oxim 刚刚完成了估值为十六亿美元的 A 轮融资，而他引起了很多人的关注，则来自于这样一条新闻。
五十七岁的美国终身教授突然辞职，去给二十四岁的华人女孩打工。那接下来就是我对洪乐潼的访谈，因为我确实在每一个时期都觉得是自己是那个环境里面最愚蠢的那一个，最怎么样努力都看不到结果的那一个。在你的心目中，AI for Math，它在整个AI的大地图上，它应该画在哪个地方？我觉得大部分我知道的就是，嗯。
Founder就是创业公司的创始人，他们都对就是苦难上瘾。我听下来，我会有一个问题，因为现在 coding 也很火。对，那用 math 作为手段和用 coding
作为手段去执行任务的区别会是什么呢？没有人喜欢融资，没有人喜欢融资，它不是说难，结果难，它就是累。嗯，呃。你是一个复读机，你一次一次地说一样的事情，你一次一次的接到一样的问题，真的我就能我我其实可以把它录下来，然后我就给你们大家发，对吧？
你们反正问题也是一样的这个。但是呢，就是从这一些大量的比较无聊的这个过程中，有一些让人很激动的谈话。通常这一些谈话是你最终选择的，选择了投资人。比如说，我印象特别深刻的，我们最后的领头方 B Capital，我跟 Howard Morgan，呃，就是有一个对话。Hello，乐童，还是先给观众朋友们打个招呼，并且做一个简单的自我介绍。
好，Hello，小俊，谢谢你邀请我。啊，我是洪乐潼，嗯，Axium的创始人和CEO。啊，对，嗯，我想我们的聊天可以从一个故事开始，就是很多数学家在说自己被数学打动的那个时刻，都叫做被数学击中的时刻。比如说高斯就说像闪电一样。你自己有过这样的时刻吗？我就是自己解题的过程中，这个稍微就是低频率一些，但是我经常在看别人结果的时候，有一种哇，这个东西怎么这么美的一个感受啊！
我印象中特别深，其中一个例子就是说，啊，第一次看到这个，啊，模型式椭圆曲线定理，就是说每一个这种啊模型式，它都对应着一个呃椭圆曲线，相当于是把。呃，一个比较代数性的一些一个一个表达式和一个呃更几何性的一种几何呃呃物。几何物体，呃，就是联系起来。然后我觉得，就是数学中这种两个领域，然后他们相当于中间有一个交集的这样的一个例子，还是每一次我都是觉得非常非常非常优美的。
然后呃，我印象中就是还有另外的，比如说概率，然后物理，那里面又有一堆的可以就是呃，让我觉得非常就是有意思的结果。嗯，然后我自己解题的话，还是就是小的时候可能见得不太多，就是觉得数学还能还能这么玩。就是当时从初等数论的时候一直推推到这个二次互反律。我当时在美国的一个叫罗斯夏令营，然后他每一天就给你每一天给你一个题集，然后你要把它让全部做完，还挺多题呢。
全部做完才能拿第二天的题集，像游戏打怪一样。然后如果你做不完所有的题，他就不给你下一个题集。然后你就看你隔壁的那个同学已经就比你就是多了三个题集，有更多有意思的可能是正确的东西。但是由于你的证明能力还没有跟上，你一直到不了。然后到最后到二次互反律的时候，就是他给你呈现了很多的证明。我在这个过程中一定是觉得有被数学击中的时刻的。
然后呃，就是觉得非常。表达非常简洁的东西，它后面的这个证明可以很深，然后也可以有很创造力的一些解法。我有一个问题，它可能会很好回答，也可能会很不好回答。就是有一天我跟A
I在谈论数学的时候，它提到数学是一种结构的语言，所以我想知道，从你的视角来定义数学到底是什么？对。啊，这个确实不太好回答。我觉得数学它有一点像是说是人类我们决定说去创造一个文明的体系，然后在这个文明的体系里面，由于一些就是我们愿意去说是。
呃，我们认为是是对的一些公理，然后往上去搭建，就是我们我们他其实某种程度上是数学家，他有一个契约，就是说哪一些东西我们是愿意接受，是呃理所当然的。然后在这些东西上面，最少的理所当然，或者说不一定是最少，看你从哪一个角度去看。有一些人他会去从 compression
压缩这里去去看，他希望是最少的公理；有一些人是去希望能找最有意思的，或者说就是搭搭配最合理的一套公理系统，然后往上再搭建，然后往上搭建的这个过程中，其实我觉得这个过程是。
很多人觉得数学是解题，就是我有一道题，然后我把它做出来。但就是往上搭理论的这个过程其实很有意思。一般是先从一些数学的一些例子出发，一些它就是呃，比如说是一个一个序列，或者说是一个集合，然后你去发现一些规律，然后这个时候你觉得很自然而然的下面的一个题应该是怎么样的，然后再去证明它。所以这个过程其实有一点点像艺术。
我觉得数学是一个介于艺术与科学之间的一个存在。所以数学到底是一个被发现的过程，还是一个被创造的过程？这是一个这个千古千古千古的难题的辩论辩论点。嗯，你是哪一派？我觉得就是呃，如果就是一些数学家，他们有一套比较相似的训练背景，或者说他们在同一个领域里面，他们阅读了同样的一批呃代表作，他们会有一个某种程度上比较大的一个默契。
去说，我们认为这个很自然而然的，它应该是是什么样的。然后，如果说出现了一个，比如说最有意思的就是，当拉马努金他从印度来到了英国，他遇到了这个哈代和Littlewood。他们就是 Hardy Littlewood，他们两个人就是一直就他们两个写 paper，他们写了很多很多的文章。然后拉马努金来到这里，就是像一个外星人一样，他说：“嘿，这是我的这个草稿本，上面这些东西全都是对的。
我从来没有接受过数学的这个训练，我不知道怎么去证明它。”然后哈代和 Littlewood 就会觉得。这些东西看起来很有意思，他们很新，然后他们和我们之前做的东西又感觉是又感觉这个东西是对的，但是所以他们就开始用证明，所以某种程度上证明是一个与原来的这一群数学家所不太一样的一个一一些一些人，他们可以用证明来来来说服他们，证明其实某种程度上它是影响力。
就是我只要能够去把这个东西严丝合缝的逻辑证明出来，我这个数学的发现就是可以被接受的。然后在它被接受的这个情况下，当然了，就是又会说你这个证明是美还是不美，是自然还是不自然。这个我们之前看到很多国际的数论学家去看，呃，张益唐先生的这个呃的的数论证明，他们就觉得这个证明是。和他们熟悉的一些学派非常不一样的一种证明方式，但是在呃，就是非常著名的那一个。
那一个结果就是，呃，素数的这个固定的这个差，这个他们觉得是是正确的，所以他们又接受了这件。事情，于是就是又开始去互相的去去学习和整理他们的证明方式。比如说James Maynard的二零二二年的菲尔兹奖，他有另外的他的一套的证明的这个技巧，然后他的学生们去继承他的证明的技巧，然后他他和这个张益唐先生的这些就可以进行，大家可以进行比较，也可以进行简化。
这个过程其实是非常非常有意思的一个一个智力过程。你是哪一派呀？啊，是那种直觉派、天才派还是证明派？我一直就是非常希望能当直直觉派、天才派，然后这其实是我很小就是痛苦的一个根源，就是我一直发现我自己没有什么特别大的数学天赋，就我是一个蛮力型选手。对，我是蛮力型选手。就是你给我，我我小时候在打数学奥赛的时候，我记得他们说，就是每个卷子的第一道题几何题，欧式几何题。
欧式几何题是必拿的分，你如果不拿欧式几何题，你连这个三等奖你都拿不到。然后我就一直做不出来欧式几何题，我我我倒是可能能做代数不等式，我的大脑可能更偏代数的符号的表达，然后几何和拓扑实在是差。所以我一般就是去把每一个点，然后每一条线，就用这个复数法，就是大力出奇迹。我最后我不需要去理解这个几何题它背后的几何意义，我就把它完全是就是照本宣科的去拿一个套非常复杂的复数法去把它就是解决出来。
我可能会需要比别人多两到三倍的时间，导致我可能其他题目的时间分配不均。但是这是我做这个几何体的唯一方式。其实最有意思的是，二零二一年开始，就是 Google Deep Mind 他们从他们很秘密的开始一个这个 Alpha Geometry 的这个这个项目。就是说，如果我们这个拿AI去证明欧式几何题非常困难，感到困难，能否把它变成符号表达？
它这个不是复数法，跟跟我说的这个人类，我这个人类做的方式是不一样，但它这个背后的哲学是一样的。我把几何的图形变成这个符号表达式，于是这就是他们就能够通过这个东西去解决。呃，好像百分之八十一的就是AI的，呃，就是AI能够解决百分之八十一历史上IMO的几何题。就这是一个很有意思，这是一个我不是天赋型选手的这个解释。
呃，解释一，我有一个解释二，就是我在MIT的时候，我身边所有人，他们都是天赋型选手。所以你只要就是看看左边看看右边，你就知道自己不是天赋型选手。但是呢，我我不放弃，我是打不死的小强。就是你给我一道题，我三个月我做不出来，我继续想。我记得当时Henry Kong教授他给了我一道。Sphere packing让我去想一些关于二十八维的这个 sphere packing 的一些小的问题。
这个东西当然不可能，就是期待一个本科生完全解决。然后我六个月我什么都没有想出来，但是我每一周我就去说，哎，我这是我试过的，我没有成功。然后我又试了一周，我又没有成功。所以，但这个这种蛮力型其实某种程度上会和一些天赋型选手存在一个互补，就是说他们可能有一些脏活累活不愿意干的，我可以把它去干完。所以你的这个过程，有点类似于AI的过程。
AI是这种蛮力型选手，AI是直觉派吗？现在AI里面它也分了这个比较天赋型、聪明型的AI和这个和这个比较蛮力型的AI。比如说，我们现在这个我们公司的这个AI系统。它里面就是它是一个系统，所以它中间有很多的模型。它有一些模型就是能够很很快的去呃呃认定这个题目应该是被一二三四五六七步这么大概证明出来。然后就是偏形式化，见到了很多Lean这种形式化语言的AI。
他就会说，哎，反正我就是一个 tactic，一个 tactic 的 tactic 是 lean 里面的一个步骤或者说是策略，它能够让你就是从把你的一个很复杂的问题一步一步的去把它解决。它更是这种严丝合缝，就是小步小步走，然后不是之前刚才讲的那一个能够列提纲的 AI。所以其实 AI 这系统里面两种就是类型的 AI 数学家，它也能相辅相成。
某种情况下，其实最有意思的是，呃，当看到一道题，就是我们发现，在我们最近，呃，我们公司在这个普特南大学生数学竞赛中，就是这个 Action Prover AI 拿了满分，嗯，呃，然后是呃，人类历史上有五个满分，啊，过去的九十八年一百，呃，一，一九二七年开始第第一次普特南数学竞赛，然后这是第六个满分，是一个 AI 拿到的。
然后我们就有看这个AI的解法，有一道题我印象特别深刻。我们队伍中有这么一个同学，他叫做 Evan Chen，他是美国就是IMO呃数学竞赛队的这个教练。所以他是非常天赋型的一个选手。他看到这道题，他画了一个图，然后我们所有人当时在那个会议室一看到这个图，我们就说：“哦，那你是把它做出来了，就一个图的一个解法。
”嗯，这个AI果然就没有找到这个一的一个图的解法。我们看到了就是几千行的这个Lean代码，它是就是硬生生的把它。某种类似枚举、类似分类讨论，然后呃，就是一步一步一步核实，去把它就是。干出来的，所以就是这是一个大力出奇迹的AI。他可以看到这个机器，他会去，就算是一道很明显可以去做创造力解法的一道题目，他可以去通过他自己擅长的东西去给出给出一个完全不一样的解法。
其实我觉得去比较人类与AI就是得到的这个证明解法背后的数学是一个非常有意思的过程。嗯，所以数学不是人类的特权，对吗？呃，现在感觉上这个自动定理证明这个领域，呃，发展的很好。其实这个领域它呃不能够叫是AI的胜利。他在呃没有AI没有这个深度神经网络的时候，就有一群呃呃电脑计算机科学家，他们就是去希望能够使得呃基于规则的电脑系统能够去帮助人类去解决呃能够解决的数学问题。
然后，这就叫做自动定理证明（ATP）。然后，ITP就是交互性定理证明、互动性定理证明。就是，毕竟有一些ATP无法解决的，就是过去会有一些人类，他们是数学家，他们也会去呃写这种Lean这种特定的这种啊程序编程语言。他们就会去与这个电脑系统一起去合作证明这件事情。现在其实我们只是把这个ATP中的这个人类换成了一个AI而已。
它这个这个这个古老的这个学科，其实某种程度上是ATP与AI的这样的一个一个交集，嗯。我相信很多人都还是会对你很好奇。你虽然一直在说你不是天赋型选手，你是一个蛮力型选手，但是你的过往的背景非常的强，嗯，所以还是想聊聊你自己。你在广州长大，广州是一座非常有烟火气的城市，所以你的小时候的成长环境是什么样的呀？
对，呃，广州是一个非常非常有烟火气的城市，呃，其中我最深刻的一个童年记忆就是，确实有很多好吃的。就是感觉，呃，到了后面长大，就是留学，感觉就是食物上比较比较匮乏，尤其是和家乡的家乡的美食比起来。呃，我爸爸妈妈，呃，我们是在广州啊，我在广州出生长大，然后我们住在就是离学校很近，所以就是每天可以走路去上学。
然后有些时候上学的时候就也会想想数学题，然后也走到不知道哪里去，就是这种呃呃，说是就是想数学的同学们经常犯的这样的这个习惯，我也有啊。走路到学校多多远啊？呃，就十分钟。然后就是有时候会会开始游荡，因为就是就是有时候脑子会想想别的事情。其实我觉得这是一个非常快乐的一个状态，呃。后面就是我最近创业，呃，我有一个这个呃呃导师，他讲到一个概念，就叫做呃
bounded attention 和 free attention。
bounded attention 的意思是说，呃，被框架住的注意力，然后 free attention 是说自由注意力。比如说我们呃每一天早上起来，我们会看到很多邮件，然后我们会有很多我必须要执行的事情，因为我不执行这些事情，可能说有一个期限性，你必须要把它执行掉。这个时候你的大脑是在一个呃被框架住的注意力的这样的一个情况下，对。
然后呃很多很成功的企业家他们是。非常有纪律性的执行家，他们就是每一天日复一日的去compound复利他的这个执行，呃呃，这个很好。然后，所以我一开始就是创业的时候也非常希望我每一天能做多少事情做多少事情，但是就是后面这一个。自由注意力其实是能够区分一个平均的一个创业者和一个很很好的一个很有呃策略性和决策性的一个创业者的一个区别。
其实是在自由注意力这里，或者说一个数学家自由注意力这里，是可以把人与人之间的这个差距拉开的点。所以，当你所有的时间，呃，自愿的去，由于说我要做一个像，呃，就是像军训一样，我每一天就是要干掉多少活儿，你可能会使得你这个自由注意力这一块儿，呃，反而是欠缺了，你丧失了很多的机会成本。所以我就是特别有时候怀念小时候，就是走路上学的时候，就是有很多这种自由注意力。
某种程度上，呃，就是就是人家说爱因斯坦的洗澡事件，这个这个过程中其实能够呃有很多很有意思的一些，就是大脑能到一些很有意思的地方去。这可能是灵感和直觉来到你的大脑里的时候，嗯，对。但是呃，这个事情是它不是一个线性的，不是说你投入多少自由注意力的时间，呃，你其实也有可能自由注意力的时间你什么都没有想到，然后在后面的你可能在被逼迫做一些任务的时候，在中间你会就是有一个callback，就是回到了你。
其实自由注意力给你大脑里面打下的这样的一个一个一个基础，你反而会在那一刻，可能可能你大脑也不想做那些无聊的事情，他就说：“哎，我想到了这样的一个呃比较有创造性的一个一个想法。”所以自由注意力和绑定的attention和限制性的注意力，它应该是结合的，它有配比吗？呃，不知道，我觉得大家的配比不一样。人家说有三种创业者，第一种叫visionary，就是有前瞻性的野心家；第二种叫做呃执execution啊executor，就是执行，他就是能够。
呃，其实扎克伯格，我们在这个Facebook小屋，今天特别特别有意思的一个场地。呃，扎克伯格他就是一个执行狂，就是他是一个执行、执行、执行、执行、执行的一个人。然后你可以看到他，嗯。每隔一段时间会有一些呃行动去弥补可能前瞻性的决策落后，所以他是一个非常就是执行的执行派的一个企业家。然后第三种就是销售派，就是他是呃能够呃销售派其实并不是一个。
负面的词就是他有非常好的沟通能力，他有非常强的与不同的这个受众沟通的能力，然后他能够去影响别人、引领别人，然后把一个队伍就是这么建起来。呃，我我一直从来不觉得我是销售派，这个是肯定肯定不是的。呃，然后我呃也不是一个多好的执行派，其实我也我可能就是也不能叫做前瞻性，这个前瞻性是说是对的。我就是想做一些事情，然后我想做一些事情会极度乐观，然后我极度乐观的情况下，嗯，就算是往下就是跌一点儿，它好像也也还也还行，也还达成了一个一个KPI。
所以你觉得你是第一种visionary？我觉得我是visionary。我我反正肯定不是salesman或者是executor。你刚才说扎克伯格是属于第二类，属于他是第二类。对，你觉得像其他的一些企业家呢，在美国这边一些知名的企业家啊。知名的企业家啊，马斯克是是是是visionary，这个是绝对的。然后Sam
Altman是salesman啊，然后啊，我觉得一定要互补，就是嗯，也比如说扎克伯格，他身边全是梦想家，看Shrap这个CTO，梦想家，嗯，他也有其他很好的。
执行的其他执行的人，就是我觉得光互补也不行。你要有一些是你的同类，然后有一些是互补。呃呃，桑德伯格做了很长时间的很好的执行家，呃稳健的去，呃把零到三千人的情况下，这个文化都把持得很好。其实我觉得Facebook非常强的一个点是，就是每一个Facebook的人他们都bleed purple，就是他们的血液里面就是紫色，就是就是Facebook的这个颜色。
他们紫色，紫色代表什么？呃，紫色就是Facebook的办公室有很多呃很。疯狂的颜色，其中有一个很明显的是紫色。其实这个是因为扎克伯格他是他是嗯，color blind，他是呃很有一些颜色光谱无法区分，所以说他的那个就是办公室有非常大胆的大胆的颜色和。其实去看那个Facebook的这个园区，像是一个梦工厂，它有二十四小时的这个雪糕店，就是冰淇淋店，然后有地方让呃，就是大家去玩鼓、玩吉他、玩乐队。
呃，我们公司大部分的人其实之前都是在Facebook的，所以你很了解他们。对他们有一个非常强的一个叫做。Bottoms up 的 culture 就是由下往上，嗯，而不是往，而不是上行下效，它是这不是 top down，就是 top down 非常 Google，然后 bottoms up
非常的非常的 Facebook，所以我们公司其实某种程度上，呃，并没有一个定义文化的机会，我们某种程度上沿袭了，呃，呃，我们大部分的早期创始员工他们本来的文化。
好的，关于Facebook，我们后面还会聊到。好，我们先回来。嗯，你在广州那个城市是怎么长大的？对，就是呃打打数学竞赛，然后呃我看看百家讲坛。我是非常喜欢这个百家讲坛。对我非常喜欢，就是所有的就是呃中国的这个呃文学与历史啊，我喜欢就是看那些历史故事。我当时记得就是易中天讲三国，然后。啊，诸子百家，然后就是还是非常快乐的一段时间。
我特别喜欢文学，就是黄永玉，他有一本书叫《大姚大雅宝胡同甲二号》，然后比我老的老头。啊，就是那本书的书名，然后其中讲到了这个呃中国的这个文艺界呃就是画家，然后作家，然后他们呃各种各样的画家、版画家、雕塑家，然后呃他们都住在这样的一个北京的一个胡同里面。我妈妈她是她是北京的北京人，所以说我们家某种程度上，我们虽然住在广州，然后又有受很多这种呃呃京城文化的这个影响。
对，所以我发现你小时候自由注意力。是很旺盛的啊，很很旺盛的自由注意力。嗯，因为你并没有把所有的时间都集中在数学上。我我对我也被数学教练小时候就批批评说不是最刻苦的那一个。OK，但是，我如果遇到一道题，这个题就是要跟这道题去死磕。我就，这是某种程度上，你如果看我花了多少时间在那道题上，你会说这个小孩很刻苦，但这个过程中像玩儿一样，他不。
它不像work，嗯，就我觉得区分说是呃这个框框住了的这种呃限制性注意力和自由注意力的这个其实是一个主体感知，就是你到底觉得你是在玩还是在工作？然后我觉得呃我小时候大部分的事情都感觉是想玩，然后就是那些学校的作业就是一般课间就是写完，然后我放学之后就所有的时间我就是。可以做一些其他的其他的事情，呃，后来就是大概是初一的时候，呃，发现就是可以去，可以发现了一个一个事情，就我可以去找一些就是更高等的数学书看。
就小时候是呃意识到说我一直要做数学竞赛嘛，所以我要比如说我三年级做五年级的数学竞赛题集，就是一直是做数学竞赛更更更更更高级的。但是到初中的时候就开始，我为什么不去学学高等数学呢？所以就是开始看就是呃微积分呐，就是当然实分析、复分析，哇，然后就觉得非常有意思，因为它不像是一个零和游戏了，就是做数学竞赛的时候总觉得。
其其实，比如说，在这个呃广东省的这种奥数这种这个训练环境下，呃比较痛苦的一点就是你的同学们他们要跟你考同一场试，所以对于一个一个小孩来说，这种友谊的这种概念也比较复杂，就是竞争它就是特别存在。但是你如果是看高等数学这个。你这它没有，它不是一个零和游戏，它是一个正和游戏。你你可以自己就是到你想到的这个深度广度，然后你可以找一些你们班里就是对这个比较感兴趣的同学们一块去讲，然后你们不需要某一天同时去参加某一个考试。
所以那但是你还是要回来打这场零和游戏。对，我还是要打这个零和游戏。然后这个就是零和游戏上就非常吃亏了。有些时候看到一一个卷子吧，就是四道题，最后一道你就发现是数论。啊，数论多美啊！你你可能刚最近看了这个高等高等数学里面去学了更多，就是数论的呃呃这种这种这种高级的这个这个概念。然后你就一套卷子，你如果你的理智会告诉你，你要在这个零和游戏中取得高分，你应该先把第一道欧式几何题把它做出来，接着你做第二道代数不等式，然后最后这道数论题大概率你是做不出来的。
你要是做出来，你就进省队了。然后所以，呃，你不应该拿到这个卷子的第一刻，先从最后这道题开始。但是我当时由于我就是课外的这种非常浓厚的兴趣，加上我非常的喜欢数论，我长大也是就是做数论，我我我觉得我非常非常的爱数论，于是我就会先从这道题开始，然后一般来说这个时间就开始流逝，然后在一个呃一个一个固定的一个比赛时长中，这是一个不是最优的策略。
你是一个竞争欲很强的人嘛？因为你刚才也提到，呃，就是在打比赛的过程中，这是一场联合游戏，也会影响一些友谊。你是一个竞争力很强的人，我觉得我在呃拒绝被驯化，成为一个竞争力很强的人。你在拒绝，对我在拒绝被驯化的时候意识到了，我我意识到的，对我当时你你很难不意识到，你你小学数学奥奥数奥奥林匹克学校的时候，我记得四年级到六年级对吧，每每一个月考一次试，然后每一个学期之后，他把你呃一班到二十四班全部重新排列，嗯呃就是说你如果二十二、二十三、二十四班是重点班。
啊，然后就是，呃，一班在这个楼底，二十四班在楼顶，然后你每每学期之后，就是把你这个，呃，都同学们就是换换教室。二十四班的下去了，下到十九班了，不是重点班。你楼梯也往下走，你这个心情肯定也不是特别好。你一班在哪儿？呃，一班在楼底啊。我我当时进去的时候我是四班，然后我记得就是就在这个洗手间旁边，这个感觉就是说明这个我入学考试考的是真差，对吧？
不是天赋型选手，就卯足了劲儿想上这个二十二、二十三、二十四的那个楼顶，呃。听说楼顶这个风景也好，对吧？就这一个一个四年级的一个小朋友，他肯定是会呃有这种就是争强好胜心，就是在一个比较呃呃大家就会有这种压力的感受，然后。呃，我后面是觉得就是这个不好玩，我不想玩这个。后面是什么时候？呃，初中吧，初初一初二就我开始看这个，呃，高等数学书的时候，我就开始不太想玩这个游戏。
哦，那你做出了什么样的改变呢？在你不想玩这个游戏之后，嗯，就是客观条件上你还是要去参加那些考试，你还是要去排名，你还是要去竞赛。我不是那么在意了。就是我一直不到初三，我没有，就是初三要打初中数学联赛了。然后我就是呃，开始初一到初，我临到临初中数学联赛，我才开始准备初中数学联赛。最后好像好像也考的非常好，这个初中数学联赛就是，反正我当时还特别就是惊讶，我觉得我肯定是要考砸，但是呃初中数学联赛考的挺好，然后到高中的时候就是更多的时间就是呃当时还学英语，对高中的时候又又更多的去学英语，毕竟当时也打算是要出国，所以就是更多的时间花在这一些这一些事情上面，然后嗯呃我我其实觉得做出来的改变。
改变其实就是我发现一个有意思的事情，就是你在一个群体里面，你如果发现大家有一个很清晰定义的一个目标，然后每个人都往这个目标，也就是当时的不管是下一个季度的什么数学竞赛开始呃准备的时候，呃，然后你自己有一套完全不一样的这个呃。mental
model世界世界的这个模型，你就会开始找呃这个群体里面的一个tribe一个部落，嗯，你会希望能够去建立一个小的一个部落，嗯，然后去找看谁跟你一样想读这个跟这个考试没有关系的书，然后你就会和这些人成为很好的朋友。
我记得我初中的时候有一个有一个游戏，我到现在其实我们也在有时候闲的无聊也在玩。就是你有一个n乘n的一个格子，你有一个棋盘，比如说八乘八的一个棋盘，然后你可以从这个任何的一个格子开始去走马步棋，就是你只能去走。这个跳马就是二乘三，就是的这个每一步你只能这么走，然后你呃连续的这样去走，然后你每走到一个格子你就标一二三四，就这么开始标，最后你的目标是说我能够走满每一个格子不成不重复，嗯，或者说你走不满每一个格子，你希望走到一个更高的一个数，比如说八乘八的话，你希望尽量靠近六十四，你不要在呃五十你就停了，你希望至少到个五十九，就是。
这个这个游戏，我当时我记得，我初中就和好几个好朋友们一块玩，然后我们就特别希望，呃呃，我们一个一开始开始比，看谁的数更大，后面我们就希望能够去证明说，任何n至少是五的一个一个棋盘，你永远有一种能够走满整个棋盘的方式。我们希望拿，就是我们当时猜测应该能拿数学归纳法去证明。如果你要去拿数学归纳法去证明，你就需要在呃n比较小的情况下去构造一些呃比较呃有代表性的一些base case基础情况。
于是这个是一个非常复杂的工程。然后我们所有的这一些对这个游戏比较感兴趣的同学在华附，呃，我们就开始去构造，然后非常难构造，然后所以就是群策群力一起构造，让我有一点想到我们。等会儿我们应该会聊到的，就是形式化证明，比如说陶哲轩老师，还有就是，嗯呃，Alex
Kontorovich他们做这个素数，呃素数定理的这个这个证明，然后他们就是把它也是分了很多项不同的项目，让全世界的几百个数学家和Lean的这个编程，呃呃这个编程编程的同学一起去把这个事情搭起来，有点像就是数学，其实某种程度上大家强调说。
这一个人他是一个天才，他一个人证明了一个困扰其他所有人几百年的一个猜想，然后他是一个多么厉害的数学家，他有一种呃个体性的一个强调，就是说这一个人他非常厉害。但数学，如果你去看，呃，软件工程师他们几百个人、几千个人去做一个一个project、一个大的一个项目，它是合作性的，合作性就需要一个比较好的一个结构和把它就是。
把这个呃任务去分分散分散成不同的小任务，呃，这个过程其实我觉得是很有意思的。然后某种程度上，在玩这个马步棋的时候，我们当时就是我反正一个人肯定是不可能把所有的这个这个这个例子找出来的，我需要我的这些同学们这个小部落的这个帮助。多少人啊？这个小部落一般是三到五个人，三到五个人。对对对，都是数学很好的人啊。
我们当时是那个数学班，就我们整个班都是数学很好的人。然后就是上课就不听课了，就是就是传纸条，那个纸条上就画着这个格子，就是说这个你看，我又找出来这样的一个，就是n等于比如说九的时候已经被我q掉了，就是非常快乐的一一段时间。在这个这么快乐的时候，你的成绩是什么样的？呃。就我，反正要不到大考，我也不太，我还还行吧。
我反正也到了那个，反正你的最终的目标就是你初中好像我们是九十个人，你要进到一个二十二十五、二十七个人的一个一个数学组，高中这个数学组，所以我也进去了。我记得我们当时是啊，七个女同学，好像初中，然后呃到这个高中好像就是二十五、二十七个人，三三四个女同学，反正就是也那也那也那也进去了。但是这就很奇怪，因为你说你不是天赋型，你是蛮力型，可是你实际上花的时间没有那么多。
对，这就是一个很有意思的一个点，就是我认为你在学这些高等数学的时候，某种程度上你的竞赛的这个数学，呃，也在得到这个潜移默化的提升。就这是这其实是很有意思的，就是我们等会儿应该可以讲到，就是我们发现最近有一个AI的一个发现，就是说，哎，我感觉我像是这真的是我每天在想的事情，我不是在打硬广，就是一个数学非常好的一个模型，它在编码能力上也非常好，就是它会有这种东西叫做transfer
learning，就是转移技能的转移。
嗯，呃，我觉得肯定有这么一定的程度。反正我当时我记得那个考试嘛，就是从初中考到高中的那一个考试，我是。觉得我肯定要完了，然后我的爸爸妈妈说你应该没事，你就去那里做一做，你看一下就是结果怎么样。反正觉得应该你能考好。然后结果我觉得我应该是拿了满分那一次。然后我觉得我我连几何题我做出来了，我十十几十几个嗯十几个大大大的考试中没有做出来过一次几何题，所以那次也可能是运气比较好。
哦，这个很神奇，就是从学习上对于你来说，突飞猛进是来自于你其实变得更发散了，而不是更聚焦了。你不是更努力的去做题了，而是变得你可能兴趣爱好更广泛了，你更想玩去做这件事情了。对对，呃，我当时是这么觉得的，但是这个事情到后面，我在大学的时候，在MIT的时候又觉得还是要学会聚焦。哦，就我，我觉得可能就是数学好这件事情，它没有公式。
然后我一直也不是数学最好的那一批，就是每一次大家可能说，呃，你以前打数学竞赛，然后可能现在在计算机的这些同学里面，我有一定的这个数学背景。但是我在麻省理工的时候，我身边的每一个人他都比我聪明，每一个我是整个数学系里面最愚蠢的。是你自己这么觉得，但是别人也觉得自己才是最蠢的那一个。呃，我觉得他们应该是意识到他们是很聪明的，他们意识到自己是天赋型选手的。
对，哦，为什么呢？为什么你会有这种感觉？你觉得自己没有他们聪明，就是你的背景在别人看来就已经是天才型的选手了。对，但是我当时我的同学们，比如说任秋雨、张胜彤、高继阳，就是这些人。每一个人都是在这个我小时候看着他们的新闻长大的。我看着他们的新闻长大，看到他们去了北大数院，看到他们转学到了MIT，见到了真人。
我每一天就是在就是顶礼膜拜这些大神。就是我当时在MIT的时候，这种这其实是一个非常有意思的一个一个点。其实甚至是有一些其他的小国的这个IMO的选手，比如说我有一个好朋友，他是这个呃比利时的这个这个IMO来到MIT。看到美国和中国的IMO们，然后也知道大家的IMO分数，他也会有一个心理落差。我这个其实没有落差，我的期待就是我是最最傻的一个，所以我我其实就是适应的也很好。
我反正我就觉得我每天很幸运，我和能能能和这些人一起说话，一起上课，一起做作业，我觉得还挺好。所以你对你预期没有那么高。我预期没有那么高。我觉得我当时觉得我来到MIT吧，我可能以后就去做这个量化金融了，因为我可能反正你说这个数学博士为什么他会要我，而不要其他每一个人都是IMO金牌呢？就是他肯定肯定，我觉得我肯定也考不上数学博士，所以我那我就反正我记得我大一的暑假我就是呃本来是要去桥水桥水基金去实习啊，啊因为当时就我想着我要做金融嘛，那我肯定秋天就是校招的时候开始大一去递简历，然后我记得去去啊还是挺高兴的，就是能能当时去桥水，然后当时疫情来了。
疫情来了的话，就呃，桥水就变成从一个呃，就是呃呃线下的变成一个网上的这一个实习了。然后同时，当时就有另外的一个机会，就是呃，我当时被呃Professor
Kanono，呃，小野肯老师，我们就是他现在也加入了你们，在Axim，对，他是呃，当然他是一个就是神级教授，他有一个就是REU，REU的意思是Research Experience for Undergraduates，是在美国是一个名词，就是给本科生的暑期数学研究项目。
这这些项目他们竞争非常的激烈，他们是美国的这个呃自然科学委员会，他们去呃取赞助的，所以他们的这个经费有限，经费有限就是能去呃录取的同学们也也有限。然后我当时就被小野肯教授扔到了这个waitlist候补名单上，然后他给我发了一个邮件，他说我在候补名单上的名次比较靠前。然后我当时感到非常的激动，因为呃，当时我身边的朋友们，我刚才讲的这一些大神们，他们都已经被录取了，他们在同一天已经收到了录取函。
我看到了一个邮件，说我在居然能够到这个候补名单上，我居然还能够在候补名单上名字比较靠前。然后我当时就觉得，哎，我可能还是想去做数学研究，因为我觉得我如果这个暑假不去，人下一个暑假可能就不要我了，我可能连这个候补名单上我也上不去了。所以我就，呃，最害怕最后居然被捞上来了，因为可能疫情吧，可能好多同学他们就暑假不想在一个一个一个一个数学夏令营，他可能还是想，比如说就是在家里可能隔离啊之类的。
所以拒绝他的人那一年比较多，我就被捞上去了。我被捞上去之后，我就没有去敲水。我最后是结束了大学结束的时候，那个暑假去了去了敲水。你们家里有刻意的引导你在数学上的发展吗？呃，我觉得有。我觉得我妈妈她有一个这个危机意识，她小时候数学特别不好。然后他是吗？对，你们家大人有数学基因吗？没有，就是彻底没有。哦，嗯，他数学特别不好，他数学就是他其他可能都好，他就是数学不好。
他就觉得说，你要不就是先就是学一学数学，因为可能到后面你数学会是你学科里面比较落后的一个。哦，他是觉得你可以就是呃笨鸟先飞一下。你的青少年时期获得了特别多荣誉，这个非常的长，我就不念了。我们到时候可以给大家打出来。小朋友时候的事情了，对，只是小朋友时候的事情。那这些对你来说是轻而易举获得的吗？我们刚才聊天里，其实他们好像都不是你的当时的目标，对不对？
呃，他可能考试前两三个月成为了我的目标。对他，他，我觉得我还是比较呃喜欢去做一些有创造性的事情。比如说，我记得当时大部分的时间确实花花在了就是对于数学自己的探索上，嗯，然后。你说这些目标，它其实跟这个也有很大的关系。嗯，对，它反正都是数学，它只是类型不一样。你可能说准备奥赛，我也有准备奥赛的时候。我准备奥赛就是在好像是很短的一段时间里面就刷了七十五套卷子，然后就是就是当时他青春是一个纸的那个杂志，然后就一页一页的，每一天就是做一页，然后做完把它撕掉，然后就是七七十五套卷子，七十五套卷子做完之后没选上去打那个比赛。
就是我觉得我的这个，所以一直对荣誉这个事情，我的感受非常复杂，因为我确实在每一个时期都觉得是自己是那个环境里面最愚蠢的那一个，最怎么样努力都看不到结果的那一个，然后最呃绝望，某种程度上就是。对他不是一个在舒适区，持续的不在舒适区是一个非常，嗯，我觉得是对人很有就是塑造的一个一个体验，就是呃失败是你的默认项，你是在持续的不在舒适区，对自己的要求比较高，你就会觉得什么都是失败。
但是你又很乐观，对，就你没有因为失败很痛苦，没有，就是你，我觉得是可能是因为你很乐观，所以你经常失败。你每一次就很乐观，觉得自己能够到达一个一个去，希望能够去成成成就一件一件事情。然后失败某种程度上其实自我定义的，并不是说客观定义的，可能客观看看来不是不是失败。你们描述一下你的一个失败的体验，内心的体验，它是一个外在的什么事情触发你内在的体验？
对，呃，就是麻省理工的第一个学期，它有一个叫做成绩保护。成绩保护就是所有的这些新生的同学们，他们都可以就是上任何你想上的课，然后你不需要去担心你的成绩不是一个A，因为这个GPA变得非常的重要，嗯，啊。我我身边有两两两类同学。我当时住在这个麻省理工的一个很有特色的一个宿舍楼，我们这个宿舍叫做东校区。东校区的这个，如果你走到东校区的这个庭院里面，会看到那种木头做的过山车，两个树之间有绳索，然后有一群人在玩喷火，就是这是一个非常呃麻省理工精神的一个黑客的一种一种非常nerd
nerdy的这样的一个文化，大家就是。
我我反正我当时住在这里，也觉得非常有意思。然后我在整个东校区的这种环境下，我在呃西边楼的三楼，这个Three West，这个叫Floor Pie。Four派就是因为它是三楼，所以呃，大家叫把它叫做派楼，就是圆周率楼。然后这个楼上住的全是IMO，就是这个楼上呃不是IMO就是IPHO物理物理的，或者是IOI就是信息奥赛。
遥远住在这个楼上，就是这是美国的一个奥赛选手。然后呃，这个台湾的这个呃于于红勋住在这个这个楼上，就是我们整个楼每一个人都是我的偶像。然后。所以他们就给了我一个建议，就是说你就是去上最难的课，然后你就是去上呃，你可能都呃没有这个预备知识的这个课。然后我就真的去上了这个课，因为我身边的当时玩的比较好的同学，可能都非常的有这个乐观精神，他们可能也从这样的学长学姐这里听到了一样的建议，所以我们有好几个这个大一的这个小朋友去上了这个博士概率论。
博士概率论，我们想，哎，概率论嘛，这个我们知道概率论是什么，我们就开始在想一些可能让我们算一些可能比较复杂的不会算的概率。不对，第一天开始上上来测度论。测度论从这个呃Lebesgue哇，从Borel Sigma Algebra开始讲起，从这个呃测度论背后的代数，一个叫B B Borel的一个代数开始开始讲起，我们我们就我们就就是面面相觑，我们我们完全不知道这个就是发生了什么。
然后，这其实我觉得是一个很有意思的一个体验，因为它不是一个竞赛环境下我自己一个人考砸了的这种失败，就是有好几个这个同学们，大家一块儿去，呃，去感叹一个事情很难，然后在一个在解题小组里面，我们一块儿去尝试，就是群策群力去把这个题集，MIT特别倡导合作，就把这个题集做出来。然后这个这个过程，我觉得特别特别有意思。
所以你这次就是你的不舒适感是来自于你选了一个更难的东西。对这个考试，呃，好像是满分试卷是四十分，然后这个期中考整个班的平均分就连带着，我不知道是混进来了多少我们这种呃吃了雄心豹子胆要上这个课的本科生，呃，平均分好像只有九分。哦，就是平均分只有九分，然后我们我们我们的分数都是五以下的个位数，我们这几个大一的小孩，所以我们肯定是拖这个平均分后腿的这个主力军。
哦，那你的失败体验来来自于哪里？呃，来，所以你我从来没有在一个考试上看到自己一个四十分的考试，我能拿四分，四分对。但是你知道，这是因为我选择了更难的事情。他，我觉得他也不会触发你自己觉得自己很失败的这个机制。对对对，我我什么失败都不会触发我自己觉得很失败的机制，就是我我我把这个失败当做是我的这个default默认项，嗯，对，所以我就我就开始说，那我要学分析这个课，我学不好的原因就是因为我的分析的底子不好，于是我就开始很认真的去重新把我可能十四十五岁学过的Rudin的实分析，我又再学一遍，嗯。
那你的自我奖励的机制是什么呀？你在追求什么呢？你在那个时候，你你这是你选自己选择的一些选项。我我自我奖励的机制机制，其实这是这是一个很好问题。其实它有很多重机制。我觉得我有，嗯，我在就是年纪比较小的时候，这种。社区感，或者说我有这个朋友，或者说我有呃战友们，这个大家有这种呃 camaraderie 同志的这种友友情，一块儿去去去做某一件难事情。
MIT 它特别倡导就是呃攀登，就是登山队，呃。这这个这个会给我很大的一个一个一个奖励的感受，就是我们没有放弃，就是我们期中考完了之后，我们大家一块说，就要么就一块 drop the class，就是都都把这个这个这个课给退了，要么就一块继续继续做，反正就是也有这个保护机制了，第一学期。然后我们大家就决定一起继续上这个课，就这个事情。
我年纪比较小的时候，这种呃奖励的这种感受，其实来源于啊这个社区或者说是小团队小团队。然后，呃。这这我我不知道是为什么，反正近几年是不来源于人了，嗯，近几年来源于，就是可能这个非常难的这个事情本身，嗯，就是近几年可能可能我觉得是年龄小的时候承受能力虽然说仍然说是呃就是经历了很多失败，但你自己感觉到麻木对吧？
仍然不有没有这种失败的感受，但是在。近几年可能真的是对这个东西完全没有呃负面的感受，所以就是这个难的事情本身，我有种对 pain and suffering 这个黄仁新呃老师讲的这个有更多的这种 suffering，反而对这件事情有点上瘾。为什么？我觉得大部分我知道的，就是嗯，founder就是创业公司的创始人，他们都对就是苦难上瘾，嗯，就是。
对苦难上瘾，嗯，对，就是其实这是一个不一定很健康，就是甚至就是有一个有意思的，我听一些风险投资人他们说，他们找这个founder就要找这种对疼痛上瘾的founder，我我听起来这个感觉非常的这个不可理喻，对，呃，就是他们有一句话叫做chip on the shoulder，chips in the pocket，就是说我感觉我的肩膀上有。
一些重量可能是我以前的一些伤痕。这个chip就是。在这个肩膀上的这个 chip 能够转化成口袋里的 chips，chip 就是硬币，就是钱，嗯，就是就是可能说某种程度上对于疼痛的上瘾，从这一些当然从这一些风险投资人的角度上来说，能够转化成一个呃小创业公司的成功，嗯呃，这是一个我觉得比较激进的一个理理论，但是某种程度上它有它有一定的一定的正确性在里面，嗯。
你从小团队的这种奖励机制啊，到这种事情的奖励机制，这个分界线画在哪？疫情，麻省理工就你没你没有团队了，就是MIT毕业了以后，就是不是不是我我大一的时候下学期就疫情隔离了，OK，所以等会儿你零零几年，我是我零一年，嗯，对我零一年，然后还没有到二十五，二十四二十四岁对，然后我呃二十四特别好一个数，你可以玩二十四点，对，然后嗯就是。
对对对，当时就是就是大一下学期，所有人就就赶走了呀，就不在学校，就是呃就off campus了，然后所以就没有小团队了。那那课还得上，对吧？那你必须要去学会从这个这个事情难的事情本身里面去找。找快乐的感受，嗯，所以我当时觉得就是学习曲线是非常陡的。他对我，M I T对我是性格真的是有很大的一个塑造。
我觉得就是每一个呃我遇到的在麻省理工的同学，他们都特别能吃苦，他们会在雨天、暴风雪里面去跑晨跑。就是我前一段时间，我上周末还去了波士顿一趟，就看到又是一个下雪天，blizzard那个暴雪风暴，红色警报，他们还在跑步。这是一个非常有毅力的一个学校，然后这种毅力它是非常有感染性的，它让我，呃，终身可能无法达到MIT希望我们能达到的那种毅力的程度，但我会希望往那个方向努力。
嗯，就是什么难做做什么，什么痛苦做什么，什么长期主义做什么，然后。对，还有一个我觉得就是刚才讲到小团体这件事情，就是，呃，他也就是训练了，就是说在压力来临的时候，其实对任何的人际关系都会有一个比较大的挑战，就是可能说是呃有一些呃呃一对一的这些人人际关系，也可能是一个团体的这个人际关系，呃，保持自己韧性和就是自己的内心的这种坚持和能够去影响，或者说是不一定说是影响吧。
去促进一个一个团队，他们都有这种感受。其实我觉得这是一个非常非常非常困难的一个技能。然后这种技能，我记得当时就是，呃，巴菲特、查理芒格他们就有在一个访谈中讲到说，如果你看到这样的一个人，一定要把他就是，呃，就是招进你的这个组织里。他的标，他的信号是什么？他的标志是什么呀？标志是一个，嗯，自己内核很坚持、很技术派的一个人，同时能够有呃领导力，嗯。
但是领导力这是一个非常满的一个词，就是leadership，在美美国的语境下，我觉得和中文的语境下它有一定的一定的区别，嗯。我还是觉得，就是你千万，如果你想，就是领导力里面“领导”两个词，你就没有办法有领导力，就是一定就是服务型、跟随型。哦，对对，就是最好的领导力可能是服务型。最好的领导力就是别人就是就整个团队在登山的时候，啊，你不是前面那个拿着喇叭的那个，你是就是后面递水的那个。
嗯。你刚才说不想打零和游戏，嗯，那你觉得你当时在打的是一场什么游戏？当时就是，如果我去学高等数学的话，我就可以就是，呃，有有种，就是你你感觉有浩如烟海的，不是你已经知道的这一些数学的这些概念。他其实这是一个很有意思的点，就是我在数学的呃竞赛中，我是有一个就是 syllabus，就是有一个考考试要领，可可能说每一年就是都是这些考点。
然后在高等数学里面，我只要去新引入一个定义，新引入一个概念，我可以基于这个概念与以前的这些概念去，呃，发散出新的这种定理和问题。然后这个某种程度上看着像搭积木，就是其实有一篇就是呃AI for Math的一篇文章叫做Lego Prover，就是就是说像乐高积木一样，就是你可以往上搭一个搭一个自己的小宇宙，这个这个过程是非常快乐的，嗯，这个过程是。
不受竞之竞争所限制，它不受竞争。你你你就是在跟，就是你可以在历史上的这一些站在巨人的肩膀上去去去探索一些一些事情。嗯，对。你为什么高中毕业去美国读本科，没有去比如说清华北大这样？呃，我我是非常确定我是希望能够出国，我挺喜欢麻省理工的。就我可能也确实看了一些电影，我在草稿纸上写MIT，我可能不一定是想出国，我可能想来MIT。
为什么？哦，这那个是段子是真的，是吧？这这是真的，我真的在在在那个上面。对对，如果说我想去另外一个学校，比如想去哥伦比亚大学，哥伦比亚可能要写的比较长，MIT都简单，就三个字母。嗯，对，是在数学草稿纸上写的。对对对，就是就是数学吧，就是呃，必须要一张白纸，必须要一个铅笔，不然反正也什么也做不出来。就是有一些数学家，就是他对这个纸质和这个笔，他也有一些挑剔。
我是这样的人。然后，如果你有一支非常好的铅笔，然后你有一个白纸的话，你就开始想画画。然后你可能就是我还画很多图形。我经常，我直到现在，我们 axiom 的这个办公室上白板上，如果你看到那种素描的那种立体立体几何图形，就是我画的。就是我喜欢 doodle，所以我就是我 doodle 的一部分，我就会写 MIT。
我对 MIT 信念感特别强，我非常想去那里。我看了，呃，比如说从这个，呃呃呃，就是 Good Will Hunting 这个电影，对吧？里面讲的就是这个 MIT 那个非常呃标志性的这个大大走廊啊，就是 Infinite Corridor，叫无限走廊。这这些这些事情对于一个一个一个小孩子来说，我觉得是有很多的理想主义在里面的。
这个是怎么种到你脑子里的 MIT 这个怎么？我怀疑就是看电影，就是MIT，它可能就是在这个呃pop culture流行文化中，它成为了一个哦哦不，还有很多很多的这个数学家、物理学家，他们是他们是MIT的，就是尤其是还有还有很多宇航员，他们是MIT的。那你为什么本科学的是数学和物理啊？双学位？对，肯定我要学数学，这个我是知道。
我第一天，呃，他们还讲说怎么样去探索你去学哪个专业，我肯定知道我要学数学。呃，后面在物理和计算机里面想了一下，后来还是就是选物理，就是呃，某种程度上当时对呃对量子比较有兴趣，然后当时上了很多就是量子物理的一些课，然后。呃，同时就是我做就是数呃就是数学概率那边的一些研究，呃，比如说 Professor
Scott Sheffield 他的呃随机曲面的那一些几何概率的这一些研究，有很多东西他动不动就说这个东西在物里面有一个意义，这个东西在物理里面有一个意义。
然后我听他讲的比较多了，我就想我也想学一下物理来了解一下这个到底在物理里面有什么意义。嗯，我初高中我就是我小时候物理特别差，所以这是一个大胆的决定。哦，OK，不是你大学又拿了很多的这种荣誉，这个是怎么做到的？就是你面对你你你觉得你自己是里面最蠢的，然后最笨的一个，然后你也不是很想竞争，但是你还是从结果来来说非常好。
对他，但他不是竞赛的，他有点像是这种，呃，我大学的这些荣誉，像是就是可能一个教授他提名你，然后你自己也不用就就他不是说你要去一个考试去去去坐在那里多少分钟。他他就是你可能你做你自己的事情，然后学校可能会希望提名你去一些去拿一些奖项，所以就是和现在为什么比较欣赏你，或者 professor 为什么比较欣赏你？
我觉得可能就是呃是一个比较高产的本科生，哦对，然后我觉得他们也很有鼓励性的意味，对，可能说呃看我可能平常就是呃学数学学的比较比较辛苦比较累，就是呃特别怕我就是就是可能说就是不不走数学了，可能也有一些鼓励性的一些意味，真的吗？哦，我觉得是的。我觉得就是这个数学环境啊，尤其我感受到MIT的数学环境，教授们都是非常nice、非常友善的人，然后他们都非常呃希望每一个人好，给每一个人最好的建议、最好的推荐。
就是没有说你们啊这些MIT的数学的同学们是呃去竞争有限的名额的，就是其实某种程度上，你们每一个人有自己喜欢的数学，你们喜欢的数学和别人喜欢的数学不太一样。你们就是我，如果你喜欢这个领域的，我就介绍你去这个教授。这这个世界非常大，就它变成了一个无限的游戏了。在大学期间，对，没有那么的竞赛和竞争了。对，然后我的教授们他们是非常非常好的人，就是我一我印象中当时有说，当时就是疫情，就是中美之间也呃就是停飞了，就是没有航班呃。
呃，后来就是赶紧，就是有航班的时候就想飞，然后那个时候要写一些信啊，给这个就是就是说这个人可以回来。这我们的教授都是非常好的，他们对每一个他们的这个呃呃门替他们的这个辅导的同学都都非常的好，非常的照顾。嗯，比如说这个北美数学本科生最高荣誉摩根奖，你是怎么拿到的？呃，摩根奖，我觉得就是有我的教授他去提名我，然后有另外的一些教授，包括Professor Cano，他们有写推荐信，对。
然后接下来其实就是评审委员委员会的评审委员会的这个这个决定了。三十年摩根奖的历史，每年说虽然有一个人拿到，然后有大概两两两三个人是就是也亚军和季军，呃。这些亚军和季军和拿到的这个人的数学水平没有什么差别，然后可能还有很多没有被 recognized
到的同学，他们都非常的好，就是在我们的当时的那一个圈子里面，我并不觉得我是数学最好的那一个人，就我觉得某种程度上，呃，就是但是有那么一波大家觉得就是可能研究还做得不错的本科同学，其实谁拿到谁拿不到，就是这这个这个事情的随机性是很大了的。
对，理解了。嗯，你在本科期间在数学上有哪些新的探索？你感觉你喜欢什么？对我当时喜欢还是喜欢数论，然后当时可能有就是一个抉择，就是哪哪哪一个哪种味道的数论是做更代数数论还是做更解析数论？这个中间有有一些想。就是决决定，我印象中当时还是做了很多的，就是模型式对，然后做了一些椭圆曲线这一些的工作，是在Professor
Oono的这个，我多余一半的文章其实Professor Oono，然后和I O在他的呃就是这个夏令营的里面的合作者，我们一块去去写的，对，嗯。
然后硕士去了牛津，硕士去了牛津，为什么学了神经科学没有继续沿着数学的路深造？但是也近，动不动往数学系跑，呃，就是数学系也离我们那个学院也比较。不太远，对，就就走十分钟。然后，呃，神经科学那边是我其实当时出了一件事情，就我可能非常想知道，就是人脑是怎么样的一个一个构造。就是当时家里有一些事情，就是我可能想对啊，我当时爷爷有一些，对我当时想对大脑有一有有更深的理解。
对，然后，呃，到了那里发现，你如果要对人脑有深的理解，你需要做实验。呃，我之前做过果蝇的实验。果蝇的实验是非常简单的，你就是把它这个头盖骨一撬，然后你就拿一个管子进去，然后你就看它的这个 neurodynamics。这是果蝇，这是一只一只小果蝇。但是到牛津的时候，你要考一个就是 license 一个证，你才能去做很多的动物实验。
去考这个证的时候，需要你去杀一只老鼠。我当时就是那我我我我我做完了那一次实验之后，我当时就是我要走计算神经科学，我不要去做动物实验。在英国，就是其实计算神经科学和AI他们的这个关系非常的紧密。在有一个UCL的Gatsby呃Institute里面，呃，他是原来的DeepMind的Miss Hasabish在那里做了他的postdoc博后的的的工作。
然后在这个之前，Jeffrey Hinton其实是就是是是AI教父吧，他是found founded了这个Gatsby Institute。这个Gatsby Institute它叫做盖茨比中心，它叫做计算神经科学中心，Computational Neuroscience。但他实际上其实就是大部分都是AI的faculty。
然后我跟就是Andrew Saxe教授，然后包括Andrew Saxe他的一个collaborator其实就在斯坦福叫Sean Gill。我们当时有做一些研究，然后还有啊Tim Barrans，然后Will Dorial，James Whittington，就是有很多非常杰出的又懂数学又懂AI又懂一些神经科学的研究者。
然后我当时是一个硕士的一个一个一个同学。当时我反正我记得我见到他们中的任何一个人，我当时就觉得非常的。激动，我就觉得我我感觉这个人好像能带我做做研究，然后觉得这是个非常好的机会。所以你是被AI点燃，你不是被神经科学点燃了？最后。我最后是就我的我的那个快乐来自于来自于AI，不来自于神经科学。然后还当时还就是要写那个硕士论文，就是这一些我刚才讲的这些研究员们，他们要一起来协助我把它写成一个更神经科学的一个毕业论文。
因为就全是AI，后来怎么写的？写了个啥？呃，就是有其实有找到说，比如有一篇其实就是continual learning的一篇，哦，呃，去去去去看这个neural dynamics。然后另外的一篇是，就是去看一个假设一个呃 one layer linear transformer，这个理论是理论机器学习能做的事情非常有限，在这样的情况下你也找不出，你也没有办法做 exact neural net。
你就可以去，但当然记我印象中非常大量的线性代数，非常大量的矩阵运算。就是在出现在然后前面那一篇大量的这种就是欧迪对其实都是非常基础的数学应用在这一些呃可以有嗯有有AI与呃认知科学背景的背景的这些项目上。那你博士为什么又去读了数学和法学在斯坦福？呃，我博士这个数学我是本来本科的时候就是 defer 了，所以就是本来就知道自己要回去哦，回去读。
所以我啊，我当时是本来打算可能本科之后直接去读数学博士，就是没有去经过这个呃牛津这一层。为什么牛津去了呢？呃，因为罗德奖学金，我觉得是一个非常好的一个机会。OK，我我有另外一层，就我从小喜欢打辩论，所以我觉得在就是牛津的这个呃呃有这个Oxford Union，它有一些训练你去成为一个更好辩手的一些活动，然后包括是后面到法学院去做呃就是呃litigation诉讼相关的。
我不是我不是并购那边的，我是诉讼那边的。就是呃，暑假实习之类的，其实都是因由于这个辩论的这个呃，很很小的时候开始辩论的热情，嗯，所以你其实整个的发展非常的综合。能这么说对吗？呃，可但我差的也是，实在是差。就是综合一般意味着是没有短板，就是我还是有很多很多短板。你差的是什么？短板是什么？我很很多事情我都就是做的不太好，比如说我，我印象中当时地理是非常糟糕，我到现在呃没有任何的方向感。
我就是我我我觉得我是一个比较spiky又就是。不太好的就是不不太会的东西也非常spicy的一个人，我是一个high variance的一个人哦，哎，那经过了数学、物理、神经科学、AI，包括法学这多重学科，你站在这个交叉路口，你看到了什么呢？就在你对可能在站在博士的那个时候，对，呃，当时看到了就是几件事情，第一件事情就是。
我当时对宪法非常感兴趣，然后我当时就是宪法里面它分几种宪法去诠释美国宪法的这个方式，呃，比如说 originalism 原点主义，就是说所有宪法现在我们看到的是基于国父们就是建国的那一些人他们的原旨原意来应该来这样诠释宪法。这是这是第一种，然后第二种就是叫做
textualism，就是说宪法写的这个英语字儿是什么，你就把它读成什么，你不要去想他们原来可能想的是什么，呃，你就是去呃一字一句的去解读，去看到一个定义，特别像一个数学家可能会去会去做的一个诠释。
第三个呃叫living constitutionalism或者叫policy
consideration，就是说这个宪法它会呼吸，它会与时代一起成长。呃，原来的宪法是这样写的，我们应该把它看到二十一世纪去怎么样去解读它。呃，就是，然后在我在法学院就当时对这些东西非常感兴趣。我是一个呃非常嗯，我是一个textualist，就是我是一个按照它是什么样就是什么样的这样，这是我的呃我的司法哲学呃judicial
philosophy。
然后当时他们就有人说，如果你想去了解这个到底是什么意思，因为我们不知道这些词是什么意思，可以去拿一个就是L M。去去去去给他一些就是一些data，让他这些data可以包括什么在里面也值得商榷，可以包括这些建国文献，也可以就是包括现在的一些呃一些一些一些新的当代的一些一些政治与哲学的一些一些一些一些著作。
然后我当时就有一个想法就是。如果我们已经到了一个能拿AI去看这个宪法是什么意思的这样的一个时代了，我为什么不能拿AI做数学？嗯，我当时就在课上，我在想这件事情，我就觉得AI应该可以做数学。然后我就想到一件事情，就我最好的一个朋友之一，就是呃，他叫Kenny罗，他是呃帝国理工啊，Imperial College，他交换到MIT，我们大一就认识，然后我们一块上了很多的课，我们是非常好的朋友。
然后他还教会我怎么下这个象棋。他是这个象棋的这个大师，然后他就是告诉我，从二零二零年开始告诉我他在做Lean，他在做形式化证明。他是最开始令里面什么都没有的，呃，就是Mathlib是一个空空如也的一个一个library。他把他里面所有的本科的代数、本科的分析，去把它一行行的把它打出来，做基础的这个建设的那五到七个学生之一是Kevin
Buzzard的学生，所以他就我就我当时我就在想一件事情，就是说AI如果能去做。
法律是去看比较structure的东西，就是这个东西到底是是什么意思，而不是研究的是比较specification这一块，而不是。比如说，让你去拿AI去判一个这个人到底有没有杀了另外一个人，一个普通的trial court一个case，而是去看这个constitutional law比较就是precisely define比较严谨的去去定义的这个。
那我需要数学，不是英语，而是一个更结构性的。一种一种呈现，而这个Lean这个形式化语言，它就把数学变成了一个代码，所以它就可能能够去。我当然就有一些这样的一个想法，然后当时同时和Shubal我们在这个呃一个叫做Verve的一个咖啡店，我们一开始认识的，然后接下来。我记得在 Palo Alto，在 Palo Alto，对，就是呃 Verve 咖啡。
现在墙上还有我们两个当时就是照的一张拍立得相片。他当时说，你买了一共买了一千杯咖啡，你就可以照一张拍立得。我和叔伯在那一定买过一千杯咖啡。哦，对我们，我们给这个咖啡店就是带来了非常多的这个营收。那我们现在整个办公室的每一个人，他们每一天都在这个咖啡店。呃，然后哦，Shubal，OK，对对，然后我们当时也一直在聊这件事情，就是陶哲轩老师有很很多的，嗯，不管是嗯播客还是就是写的博客，啊，讲就讲这个形式化证明。
然后我身边的就是Kenny，他我我知道他有多对这个Lean进行狂热，他现在也在AxM兼职，所以就是好多好朋友们，大家现在就是慢慢的聚到了一起，就是希望能做能做这件事情。我当时看到的一个事情就是，嗯，一切我们认为的不可能都有可能。然后，如果是这样的话，对我个人意义最大的就是让AI能够帮助我进行一些数学证明。
尤其我不是天赋型选手，我有些时候真的是花某种程度上，你说AI能够帮助最大的是谁？是那些蛮力型数学家。就我就我可能真的就是我要枚举多少个可能性，我要经历呃多少天去验证一个非常呃可能是一个standard
argument一个标准的一种一种一种一种一种证明方式。我按要按照那个比对，我记得当时呃就有一个一个事情，就是Ben Green老师有一篇文章叫Sharkovsky Theorem for Shifted Primes，他讲的就是说。
我有一个集合，我要保证这个里面的集合的a和b两个元素中间的这个差值就是a减b，它不是p加一或p减一，p是一个素数。然后我能够就是呃，从一到n中数出多少个这样的一个一个一个一多大的一个集合。然后我当时就我看到那篇文章，我想这个东西能够被证明多少的数学问题？就同样的这一套machinery，就是Ben
Green老师的这一套这一套发明或者是发现，你可以把它去做function field，你可以把它去做。
呃，当然说做shifted sum of two squares没有特别大的意义，可以做x方加y方加减一，这个没有特别大的，不知道有没有特别大的意义。反正就是这一套的东西是工具，是可以用来做很多的事情的。AI应该把它完全解决。AI应该能够达到一个一个很熟练运用所有Devanport里面数论的呃工具与技巧的一个博士生的程度。
我当时觉得这一件这个事情一定能做，然后我就开始想怎么能做这件事情，就要算力，就要我要想我有多少的这是哪一年？二零二四，二零二四年，二零就是你跟舒博频繁的进入咖啡，出入咖啡馆的那一年是二零二四年，对，二零二零二二零二四，二零二零二三年九月份到二零。二五年的十二月份，去年十二月份，啊，不，二零二四年的十二月份。
OK，对。就差不多，因为我当时还在我第一年，其实我大部分的时间就是呃，我在作为一个法学生的时候，I had a lot of fun，就是我我每一天就是感觉特别的特别的神奇。我我从来没有任何的呃，就是作业是让我去阅读的，阅读这三十页，这就是你的作业。我我的我的本科是一个工程学校，一个MIT是一个理工科学校，我不是一个文理，我没有接受过一个liberal arts的education。
哦，嗯，所以我就非常非常希望能够多读点书，然后我可以，我我还想练练英文写作。我当时觉得我都可以去，所以我那一年就是，但是。就是第一次吧，可能科学数学它不在你的生活之中，就有点想念。然后就是我想念的时候，我就跑到那个咖啡馆去。我坐那个校巴，当时没有钱，当时是是特别就是一穷二白，打不起Uber，然后从这个。
呃，这个这个斯坦福就是坐八分钟的一个坐，你要走二十分钟。你走二十分钟到这个大草坪，你到了大草坪，你就可以坐一个就是校巴，坐校巴八到九分钟你就到了这个火车站。这火车站穿越一个隧道，里面有一些流浪汉住在这个隧道里面。你就可以到这一个Wirth的咖啡馆，舒服就在那里，你就可以去跟他聊这个科技与科学。哦，他那当时已经在Meta上班了，他一直都在，他是在Meta是八八九年的一个Meta的一个元老，他是呃Meta的Facebook
AI Research的Director，就是他当时跟呃他当时跟田云栋老师差不多时候进去的，就是可能还比田云栋老师早一些。
那你你们怎么成为朋友的呀？我也不知道他是谁，他也不知道我是谁。那你们怎么认识的呢？我们就在这个咖啡馆的这个桌子，就是我一开始到那写作业。我一开始到那就是我有三十页的阅读，每堂课有三十页的阅读，我就抱着这个这么大的这个法律书，我就抱着这三三个法律书，我就我就我就去去，其实其实挺就是非常不不不不明智的一个选择。
你有那么厚的书，你抱着他们去做校巴。但当时就是你为什么一定要去那里去做作业？在 Palo Alto Downtown 啊。就是我可能我们这个法学院的图书馆，就是一般周一到周五待的有点闷。我说实话，就是嗯，它有地毯，然后有点密不透风，就。环境，你周末你就是想放松一下心情，对。然后我记得这个味儿福咖啡馆的一个点，它那个庭院有很多狗，对。
然后它只有周末有狗，就是它周周中的时候，那些狗的主人可能没有时间带它们遛狗。我我当时一开始去那里的motivation就我可以读书，我可以喝这个，我会点一杯抹茶，然后我就可以看狗。这是我的一个我的我的快乐，就是就是读读法律案例，呃，做笔记，看狗，喝抹茶。然后然后就是时间一多就总是我和发现我，然后然后就有这么一个呃每一次看的感觉非常面熟的一个人，然后我们就开始聊起来了。
哦，是在里边还是外面？因为它有里边一个区域，外面一个区域。对，在里面啊。对，你们可能共同坐在一个长桌上。对，一个一个六个人的桌子。对，然后唯一的一个六人桌。这个六个人的桌子里面，其他的人也永远都在那里。哦，对。哦，成了一个常客。对，谁开始先聊天的？应该是一个，就是没人打算聊天，好像是他坐在窗边，然后那个太阳特别晒，然后我需要那个窗帘拉起来，这么说上话的。
啊，然后呢？然后接着就对话是怎么？我就说，我就是，我就，我就，我就like非常谢谢你帮就是拉这个窗帘。然后他就说，我经常看到你。然后我就说是我也经常看到你。然后一个谈话就开始了。嗯，然后那怎么聊的数学的呢？发现他有他学过数学，他的本科是数学，他的硕士也是数学，然后他后面他好像还读了两个数学的硕士，我印象记得不是特别清，反正就是，然后我的那个呃，就是他就很好奇我，就是他觉得我应该是个法律学生，因为我有这个书，然后我们就聊这个，我当时可能我不知道我在看。
哪一块儿呢？我反正就讲这个这个案例是非常的离奇，然后就，反正两个人就开始做朋友吧。就是我觉得还是感觉这个二十一世纪就是有很多事情都是在互联网上，大家不太到一个咖啡厅、咖啡馆去聊天了。嗯，你聊了多久？我们聊了就是我们一两年，我们是朋友，我们不知道对方在哪。那他不知道你是斯坦福的学生，他知道我是斯坦福的学生，但他不知道，他可能知道我是呃法学院数学，但他不知道我，他可能不知道我有一个数学研究背景，就是就是他可能。
他好像听说过摩根奖，他听说摩根奖可能是因为有很多摩根奖的同学转入了AI，比如说老王Alper在Anthropic Greg Yang XAI的co-founder，就是Morgan Prize is like a thing in AI。然后呃，他不知道，但我也不是一个什么人物，他不知道也没关系。但是我我是真不知道他是一个这么厉害的一个一个AI人了。
你这还是Meta吗？他现在就是你知道他在麦他吗？我当时不知道，我一直不知道他在麦他。呃，后来你们是怎么开始决定要创业的呢？就是在你们这种漫无目的的认识、漫无目的的认识和聊天。对对，我有我有一天，你们这种谈话持续了多久？持续了一年半。聊什么呢？这一年半，聊科学历史哦。啊，对，然后就有一天，我印象是秋天，二零二四年的秋天，那个时候我刚开始那个数学的PhD，但我当时很多的时间其实在给XTX去做一些工作，就是XTX是一个呃呃一个一个量化金融的一个，我暑假就是后半段在在那里，嗯，然后我我当时就觉得。
我在那里就是觉得，天呐，这个AI更更有意思。就是你，XDS有卡呀，对吧？它它有卡，所以你能做的事情就比你在盖茨比做的事情多很多。所以就当时觉得AI很有意思，然后回来，然后就我有一天我就跟我是去跑步，我就是晨跑，然后跑完之后我不知道为什么我就觉得好像这个事情真的要真的要发生，然后我就去找Shubh，我说这个事情大概如果我想融资要融多少钱呢？
然后我们两个人在那算，我们算就是多少张卡，然后也在那儿就在那儿就拿了张那个餐巾纸在那算。然后我们就说，好像这个事情还是得做一个创业公司，就是没有可能在学姐去做。那我那一个学期在做X D S，我疯狂的往C S的那里跑。有一个C S最斯坦福C S，我觉得最好的一门课是一个叫做呃，就是First Year P H D Seminar。
每一个教授为了就是招新的学生，他们就会去讲他的这个Research
Highlight。你你每每一周去就一个学分，你每一周每周三下午去，下午五点，然后你可以认识你所有其他的一些。计算机系的同学们，我就坐在后排听。我是个数学系的，然后，然后完了之后，你就可以知道，我的天呐，就是有这么多，就是做机器人的他们在做什么，做这个，呃呃，computer
vision的在做什么，你就反正就是非常，it's an intellectual feast。
你是在哪一刻决定辍学要创业的？啊，其实我大概知道，就我开始融资的时候，我就知道我总有一天要辍学，就是就是先开始融资才辍学的啊？你是先开始融资再辍学？我就先开始融资再辍学，因为这个我不能辍学，因为我辍学了我没有身份，我要拿到我的这个身份工作签证，我才能够辍学啊。所以我拿到我的工作签证，我就辍学了。哦，因为就是一般来说，投资人也期待你辍学，就是你很难说是同时，你的就是硅谷这个一般拿到融资就是开始要，呃，甚至有些时候辍学是融资的
closing condition。
OK，为什么不是 Shubal 当 CEO 是你当 CEO？书包当时其实还在一开始，大部分的时间他还在卖了。嗯，他没有，他他到后面他他不是定义加入你的。OK，因为我们当时谁都不知道这个事情能否得到这个投资人的支持。嗯，这个事情是想不想不明白。嗯，所以从哪个月份决定的？我从我从九月份就决定了，但我不到十一月我没有融资，因为我一直在劝自己不要做这件事情。
为什么？我不太喜欢。就是我当然，我觉得中国语境下的创业者是一种就是气质，在美国语境下，现在就整个 valley 都是 founder，就是创业者某种程度上辍学创业，他就是浮躁。我其实觉得，如果我是一个本科生，我绝对不会去辍学，然后去 Y company 那边。就我某种程度上，我觉得我是最不可能创业的一个创业者。
我非常的喜欢向往学界，我非常的希望能够去做更多的数学的一些探索。我非常喜欢在大学的一个环境，所以我就两个月是在劝退自己，然后但是每一天早上还在跑步，然后呃跑步的时候想事情想得非常清楚。到后面确定是非常非常确定，然后，但是我但是非常非常确定的时候，马上就感恩节了，感从感恩节到圣诞节的时候没有微信上班，所以你要么就是那个时候到感恩节融完是有十天，要么你就来年再融，所以我当时就来年再融。
哦，那两个月最后你是怎么经过了怎么样的C O T，然后决定一定要做？我当时去读了这个科学史哦，然后科学史读了科学史，真的读了科学史，就是全创业读科学史，就是多少个先是从维基百科开始读科学史，后面要找书读科学史，然后有一个叫AI for Math的一个GitHub repo，嗯，这个GitHub
repo里面大概有几百篇文章，每一篇文章的abstract我都读过，然后有意思的abstract我就会把整篇文章看完。
然后我就做了多少次费曼的过程，在就是纸上去想，如果说我这个东西要搭起来，应该技术上怎么做？我不可能说我自己觉得这个事情不会成功，然后去骗别人的钱，这个事情我觉得做不到。所以我当时就到了一个程度，我发现我觉得它不一定是一个研究问题，它是一个工程问题。它这个这个东西的科技的风险就没有我一开始看上去的那么高，然后在这样的一个情况下，我觉得是负责任的去做去做这个这个这个创业，要开始融资，嗯。
所以你是在自我验证这个过程是在，对我我觉得就是某种程度上，你如果去，呃，就是吸引一些风险投资，你需要自己一定要对这件事情比较确定、比较了解，不然我觉得不太负责任。但你质疑自己的点，可能是说会不会我，呃。这是一种浮躁，这是一种跟风。一个是是不是火了，一个是是不是浮躁跟风。这个我倒知道，我我特别我特别反对做一个AI founder，所以我知道我绝对不是浮躁跟风。
反对做一个AI founder是为什么？就是我。我从因为我在MIT，然后在MIT就是有创业社，然后我的好朋友们一起去打那个Jane Street的那个啊，就是呃量化金融比赛，黑客黑客Hackathon的这些同学们，他们是创业社的社长。我当时就两个队友，他们两个就是这个创业社的社长，叫我去活动，说有这个free sushi免费的寿司，我也不去。
我觉得，我觉得创业不好，它不是一件好事情。我觉得还是要做教授，这个有点不务正业，是不是？呃，对。然后我觉得，就是我总觉得，比如说一个以非常产品为导向的这样的一个创业项目，感觉像是昙花一现。我当时也有这样的一个感受。然后我希望做的事情是非常长时间的，非常难的。所以我觉得一般和一个创业的一个这种风险投资的一个周期可能不一定吻合，所以我我知道我不是浮躁跟风的那一批，然后嗯。
我当时还有在在想，就是我又没有什么别的办法能够做这个AI for数学。然后我当时还尝试去，我要不加入一下别的做AI for数学的公司。然后就在这个Verve的咖啡馆，这个我们现在的主要的竞争者，这个公司的CEO Tudor他也是常客。于是我有一天还就见到了Tudor，然后我就说：“哎，你们你们你们招人吗？
”然后我我当时真的是想，就是我是想做这件事情。要是我能跟别人一块做，我也不用自己去去从零到一，就感觉。太复杂了，就是然后，呃，这是主要的质疑点。其实不是一个感感性的，我是不是浮躁，我是不是跟风，就是我到底会不会这个东西。然后我就我就去研究这个AI for Math，真的当时就是看paper，然后这个过程也非常的快乐，就是非常非常的快乐，非常快速的去学习一些主要的一些idea。
从比如说二零一八年一篇文章叫ATP Boost。在没有AI的情况下去去去去去去做这个形式化的这个定理证明。然后我看到 Bartos 一个波一个波兰人是这个作者。我们现在 Bartos 就就在 Action。然后我当时有另外的一篇文章叫嗯呃 Pattern
Boost，就是是。从呃很多的呃数据中去找里面的这个 pattern，找这个规律的一个去从呃很多的图中去构造新的图，去为数学家去找例子和反例的 pattern。
不错，当时看 Francois Charton 是这个作者，现在 Francois Charton 也在 Axie。然后我当时看另外一篇 AI for Math 的文章叫 Into
Int。然后这个是拿这个呃一种translative的翻译的一种方法，从问题能够翻译到解法，问题能够翻译到解法。如果看到了很多这样的例子，下一次来到一个问题的时候，是否能够直接翻译成解法，也是嗯做数学发现而不是数学证明这一这一个这一个文献里面的Alberto Alfaroino，他现在也在X。
就是所有这个美丽的过程，就是我所有这当时我作为一个学徒去看这些巨人的肩膀，这些这些文章，他们现在都聚起来了，都在Action，这是一个非常非常我觉得神奇。做创业者，我觉得其实这是最最高兴的一个过程。你又形成了你那个小团体Community，对对对对。你你去问你那个竞争对手能不能加入你们公司有没有机会？
他对怎么说？他说你是你是你是什么的PhD？我说我是数学的PhD。他说哦，我们只招计算机的PhD。哦，为什么AI for Math？对，为什么呢？我不知道，他当时就是这么说的。哦，但是你们团队很多都是math，我们团队呃这么说，嗯，我们团队有三块儿，呃，我们团队有非常多AI的人，就是强化学习agents，就是就是applied AI的这一些人，我们有很多的。
做代码生成的人，就是 programming language，然后呃很多是 compiler 编译器的人，比如说 L M compiler 那个主要团队在我们这儿，然后他们很多其他的工作，compiler arena，就是所有的这些呃 compiler，就是深度学习去帮助
compiler，就是代码生成的这样的一群人，然后他们当时也是呃 Yang Lequan 那个 code word model 三十二个 billion 的那个模型的后面的里面的一部分团队，然后都在我们。
然后有一群是数学，这数学里面比较 tricky。数学里面有，嗯，纯数学家，像 Kanono 小野小野小野肯教授，像 Evan 陈，我说的这个这个 IMO 的这一个教练，然后也有做 Lean 的，做 Lean 这个语言的，里面其实就像 Python 里有 Pytorch，它是一个。图书馆和Python，它是下面的真正的那个编程。
Lean里面也有Mathlib，是一个数学图书馆和Lean这个作为一个编程语言两两拨人，所以我们也都有。我们又有这个做Mathlib，像Kenny罗还有他的朋友居建章、张居建，就这样的一些非常好的。好的，同学们。然后我们又有就是做 meta programming，meta programming 叫元编程，就是去把 Lean 当做一个编程语言来使用，去创造出里面。
令更多的工具，更多的抽象，呃呃层，这样的就是相当于你可以拿 Python 去写一个 Autograd 的一个一个一个著名的一个一个一个一个一个 coding 的这个这个呃编程的一个面试题啊，你可以拿 Python 写一个 Autograd。我们来了一个同学，他他他拿 Lean 写了一个 Autograd。
对，所以就是这这里面又有很多块儿，所以并不全是数学的人。我们很多的，就是招ML的同学，他们很多背景。我们我们队伍里面，就是当然说算上实习生，四个M五个IMO，所以说五个IMO，然后啊啊，就是他们会有很多数学的prior，就是context，就是他们理解这个数学过程是怎么样的。但我们要求非常强的，again，这是一个工程问题。
又去二四年九月，哎，你刚刚萌生了想法，但是在努力劝退自己。对，十一月决定要创业了，然后要等那个就是圣诞假才能融资。呃，等了圣圣诞假，圣诞假你干什么了吗？圣诞假干干了很多事儿啊，和叔狗一起在读文章。哦，为什么是你们两个一起？呃，他对你就是他他已经说我要我要我要加入了吗？他当时没有，他当时就是在Mela，就是他当时，呃，他圣诞假闲着也是闲着，我们两个人就是找像像是一个reading
group，因为当时吗？
不，他当时在旅游，他圣诞假、感恩节他都在，就是在不在一个地方，我们在Zoom。哦，对哦，你们还我们能要开会？我们我们发现我们就是讨论我们阅读的心得。我们发现我们能够是很好的联创团队的时刻，是我们发现我们两个都非常讨厌Zoom。我我没有办法跟人开Zoom的会超过一个小时，他没有办法跟人开开开Zoom的会超过四十五分钟。
我们 Zoom 了四四五个小时，每次都，这是我们发现一件事情，我们思考的方式特别的又相似又互补，所以我们就非常享受每一次我们的一些技术技术的探索。他现在是，他是一个，呃，他当然，你看他二十年的GPU经历，十年的AI经历，他是当时酷达第一批就是开发者，然后当时二零一五、二零一六年、二零一四、一五一六年和吴恩达，呃，和他们这个百度这个硅谷AI研究室。
哦，他加入了百度。他当时是二零一五二一六，这是他进入AI的，他的第一步的AI。哦，哇哦，是吴恩达说：“你懂GPU，你懂点数学，反正这就是AI，来吧。”然后呃，当时有Dario，就是Anthropic的founder，他们当时有那么一群。小团队都在百度，都在百度，是美国啊，就在美国，就在硅谷。当时百度是这这，他们后来叫百度 mafia，像 paypal mafia 一样。
这些人后面是做了多少就是重要的工作？多少个嗯，早期的 open ai，多少个啊？比如说 dario 就直接是 anthropic 的这个 founder，嗯，然后嗯，非常好的一个一个，他们当时就是 scaling works。我们就是做这个 deep speech deep voice，就是把大量的这些 speech voice 的 data 去去扔进去 scaling works。
他们当时办公室有一个就是一个一个一个理念，叫我们绝对不招一个语言学家。哦，他们当时是做的Deep Speech和Deep Voice，他们需要语言学家吧？按道理，他们不招一个语言学家，有一点像我们当时我们现在公司这个做编译器的这个团队，他们当时一六一七年拿就是机器学习要去革命这个呃呃compiler code generation代码生成，他们就说。
当时就很多就是编译器的这些专家说你不可能做到的，他们就说我们不需要你们，我们照样能做到。就是拿AI进入一个领域去革命这一个领域，某种程度上是我们这整一个现在二现在三十个人了，但当时就是早期这个创始团队的一个DNA。我们希望我希望能够拿AI去去去给数学去做一些一些一些嗯革命性的一些改变。你看他们说。他们不招一个语言学家，嗯，要用AI去革语言学的命。
对，那你们是不是也应不应该招一个数学家？我们以为是这样的。我们我们以为是这样的。我们当时定了一个事情，就我们不招到第十五个人的时候，不要招一个数学家。为什么是十五个？就随便说了一个数，我们当时觉得我们钱也不是我们的种子轮，大家可能看起来数额很多，对于我们要做的事情来说，大家的普遍的想法是我们under
raise了，我们是raise的不够，我们的种子轮啊，所以我们当时觉得人的这个人头是限制的，到二十个人我们可能就没有办法再招人了，所以当时觉得那只能说那就那就以每十五比一这样的一个数学家的一个比例去走。
但是他那句话的逻辑是，我不需要语语言学家，语言学家背景可能对这个团队是负分。对，我们现在的想法就是，我们招数学家需要他非常的思想开放。呃，早期的时候，其实有一个叫做 Frontier Math 的一个 benchmark，与这个 benchmark 相关的一些同学，当时有希望，就是我们有互相都希望能够一起合作，让他们加入 Action。
但当时就发现一件事情，就是一些数学家背景的同学，他对 scaling 这件事情，他有一定的呃呃呃呃的一定的犹豫，他对或者说不是犹豫，他就不愿意，他不他不喜欢 scaling 这个这种这种哲学。他觉得说，我数学是一个工艺，我是个手艺，像日本师傅捏捏寿司。我你怎么能就是给我一个？当时我们说我们要做Internet scale dataset。
有同学就是接了我们的 offer 之后，就是就是不来了，就说我不要，我不要做 internet scale dataset。我们觉得又是要 scaling，又是要更好的 sample efficiency。就是当然说 sample efficiency 这个效率是一个非常，呃，样本效率是一个非常，也是一个非常满的，非常非常多意思的一个词了。
但是我就拿 Percy 梁教授的这个话，就是他是做乘法，嗯，我们觉得来的数学家。我们现在希望他是跟我们对着干，就是是他们做 adversarial 的，就是就是与我们与我们相对抗的去做啊 benchmark 基准集的的的的的的创造。就我希望你能够。感觉我们的系统哪弱，然后去就是，当然是越做越来越难的这一些、这些、这些基准级。
所以某种程度上，呃，就是Ken，就是呃呃小野Ken他加入之后。呃，我们的这个基准级的这个集结是我们的第第一号人物。嗯，我们继续把那个时间线来捋一下。好，呃，我们刚刚说走了，就是嗯，当时已经说到了圣诞假期，然后你们你们有一个reading group，对，音乐开始融资了。OK。对你，你们读了多少文章？
那个阶段哦，读了好多。呃，当时，而且当时我记得圣诞节，我们有一个叫圣诞大礼包。呃，杨凯玉老师他们写的一篇文章，Gabriel Proesa他们一篇文章叫做《呃形式化》。Formal theorem proving形式化定理证明，AI的下一个前沿是一个survey paper。survey paper就是它不是一个研究论文，它是一篇介绍其他所有研究论文的研究论文。
它就是把这里面领域的捋了一遍。然后我当时我记得我我那篇文章还。我记得他第五部分是有这个目标，就是说，呃，我应该一个好的AI数学家能够做到什么样的事情，在这几个象限上，他能够有什么样的就是能力。这是一个我们，我们就把它做成了我们自己的表格。然后，这个之前就是从从第一行到最后一行，我们我记得我当时就是就是每一个提到的，就是直接和间接提到的这个文章，不管是引用里的还是就是只是提到的一种逻辑，我就是比我已经有的阅读笔记，我想我还有哪些没读到的，然后还真有一半没读到的。
所以那个AI for Math那个GitHub整理的也不是很全。然后就是所有的这一些，当时就感觉就是我原来知道的，像是。一二三四五个很好的做法，现在这篇文章给我连成了一个面了，就是他他让我理解这个这个big picture了。我就是更更，我觉得我的理解反正是当时有很很显著的深刻，所以这个谢谢谢谢杨凯玉老师这篇文章。
对对对，嗯。然后到这个假期结束，舒博决定加入你吗？那还没决定加入我们，他到了就是后面再决定加入了我。他是觉得跟你一起讨论很有乐趣。对他当时，因为他是一个元老，他是一个AI的一个元老，我们我当时都没有敢问他要不要加入我们，就是我。我我我想着就是，现在他为什么开始？你们是怎么开始这个阅读的呢？就是硅谷这个文化，就是很多就是AI的这个元老，他可以做你的天使投资人，或者他可以去做你的advisor，就是他会，他会。
这事情特别流通，就是硅谷是一个非常有魅力的一个地方，就是学界、工业界、老师、同学，呃，就是年长的研究者、经历丰富的研究者和就是刚进入这个呃这个这个工业界的研究者，呃，他们就是汇集非常的流通，非常的非就是非常非常多的互动，就是。大家是谁不重要，做什么事儿比较重要？比如说，比如说舒博他另外的跟他呃他指导过的创业公司也有很多，比如说皮卡对吧？
这个啊呃对呃文景就灯米他他们也是，其实啊啊灯米他是当时进进入这个就是Facebook的时候，舒博还是面试哦面试官OK对对，所以他也跟Mestral Mestral那整个Founding
Team本来在拉嘛。就是是Shubal他们同一个org下面另外的隔壁的那一个team，就是大家都包括其实Mistral这个队和我们队伍的这个Fonsal，另外一个其实我和Shubal说加入之后第三个加入的这一个这个人关系也也也很密切，就是他们也是很多年的朋友，然后嗯。
你们是抱一种tutor的关系吗？没没有tutor，就是我，就是两个人，嗯，有不同的背景，看这个事情的角度不一样，嗯，呃，所以我们就聊了很多比较呃哲学性的一些一些一些研究的一些想法。我们当然就是觉得自己读的读的足够多了之后，就想就是有哪些可以做新的事情。然后就是做新的事情的话，又其实可能连接到哪一个古老的AI的其他的领域的一个一个做法。
比如我们当时看到的一些我们想做的事情，就在James Zhou的那个AI for Science那里，他们有做。比如说James Zhou这个实验室一直有做与其实可以对AI和数和数学很相关的东西。然后，包括比如说，我们当时想做怎么样去做一个
conjecture，怎么样去做做好的猜想。呃，当时斯坦福的这个呃计算机系就有同学在呃以呃希望能够造一个AI AI科学家这一个呃这一个愿景去做怎么样去能够去提出好的呃呃呃机器学习的猜想，就所有的这些东西它它混在一起，比如说我们现在做的一些事情跟呃当时早期做棋棋的这个expert
system专家系统这些都有关系。
所以就非常有意思，就是所有的这些东西，没有人去尝试把它，嗯，聚焦起来，在一个工业界呃盈利性的公司，也就有更多的充足的资金和算力的情况下。去去去去把这一些从二零二二年开始有一个爆发，一个一个想法的爆发，去把它验证下来，就没有人去做这件事情，我觉得非常可惜。嗯，那这是有结构性原因的。就是二零一六年的时候，Christian
Zagadie还有这个吴宇怀他们在Google开始做，比如说HoList这一些，Ho是一个就是定理证明语言。
二零一六年很就是早期，Christian Zagadie大概在二零一八一九年一直在呃改动的修改自己写的一个他写的一个白皮书，就是这个未来就非常长的一个白皮书。然后在二零二。二零二零年，我想说二零二九二零一九二零二零，OpenAI伊利亚带着人做了这些事情。伊利亚带了他们去做这个GPTF Mini F2F。
当时OpenAI还有跟Jessie Michael韩，然后Stan Poolu这一些，后面都成为了其他的好的公司的呃创业者。呃，当时他们有做在OpenAI做这件事情。二零二一年有这个呃一个呃实习生开始一个人。去在 Google Deep Mind 做这个 Alpha Geometry，他们发现哇，这个做的是真好，所有的资源进来 scale up，做成 Alpha Proof。
然后做，了你看，二零二一到二零二四，这是三年的一个耕耘。二零二四一，呃，一炮而红的这个，呃呃，AlphaProof拿了二十八分，差一分金牌的银牌，这个对我来说是一个是IMO被解决的那一个时刻。他就是那两道组合题解决不出来。二零二五年反正也是就一道组合题，大家都没解决出来。二零二四年的这个DeepMind真的是kudos to them，这是一个跨世纪的一个时刻，就是AI在数学奥赛上。
达到了，达到了好的胜利。这是二零二四年，我们在二零二五年十二月，呃，做的这个普特南的这个满分是这一个他们开启的这一个呃序章的一个一个尾声而已啊。然后我们其实马上希望做的就是呃研究数学，所以呃就是这是这个整个AI for数学的这个发展发展的这个历史。Shubal作为你的第一个员工。对，是什么时候决定的？
联创吧，对，联创，他是，呃，二月份吧，二月份，你融资融好了吗？那个，我当时有了不错的，就是这事儿能做起来了，只要想做。就是已经有了，不是不是最终的价格，但是不错的价格，估值，嗯，就是你出去融资验证了一下这个，对，其实很快就是一月份，呃，一月七号好像，因为因为一月头是这个JMM，就是数学家大会，我当时到这个，我记得是。
哎，应该是西雅图。呃，西雅图是就是那一年，呃，二零二五年，居然美国数学学会说我们今年的主题是AI for数学，这个就是。由于数学是一个相对比较保守的一个一个一个学科，比较这是这是一个非常让人就是雀跃的事情，所以很多人都去了，还有一些计算机学家。我当时和DeepMind的Adam Wagner就聊了很多。
我们发现我们都是呃曾经在某一个这个呃呃一个一个英国的学院就是上上过学，还挺有意思的。然后这个Albert奖也是在这个学院上过学的，挺有意思的。然后，嗯，所以我回来了。回来之后，好像就是第三天就有就开始就有offer了，然后就开始不停的为西门开始开始去去去竞拍。哦，去竞拍对？怎么竞拍的？或者是就是比如说，你给了我一个offer，然后过一周有另外一个人给了我一个offer，然后他们会尝试去把上一家的这个价格，就是呃，超过他。
哦，所以最后从一开始的那一个 offer 到最后的 offer 翻了三倍的故事，翻了三倍。对，你是怎么去 pitch 这些 VC 的？这对你来说难吗？这是一个非常融资的融资之门怎么打开的？因为你是第一次，没有人喜欢融资。没有人喜欢融资。如果说有一天有一个公司能把，如当然我觉得这个很很难，因为毕竟这不是一个技能的问题。
就如果有一个很好的AI融资员，我希望能够让他去融资。你要付他多少薪水？我可以给他percentage，这个真的我可以给。唉，我觉得融资是很难的一个过程。它不是说难结果难，它就是累。嗯，呃，你是一个复读机，你一次一次的说一样的事情。你一次一次的接到一样的问题，真的我就能我我可可以把它录下来，然后我就给你们大家发，对吧？
你们反正问题也是一样的这个。但是呢，就是从这一些大量的比较无聊的这个过程中，有一些让人很激动的谈话。通常这一些谈话是你最终选择的选择的投资人，比如说我印象特别深刻的，我们最后的领投方B Capital，我跟Howard Morgan，呃，就是有一个对话。我当时在赶这个 rebuttal deadline，就是有一篇就是文章的这个deadline，然后我当时跟他在Zoom上对话。
然后就是我发现Howard简直就是一个，他比你更乐观，他比你更觉得你的商业模式有前景。他告诉你这些是你的商业模式。他是文艺复兴的呃co-founder和Jim Simons一起，然后他也是另外一个硅谷老牌的一个VC叫First Round的呃联合创始人，所以他既是他是一个数学家。他住在住在纽约，他现在有时候还去纽约大学上上课，然后，然后当时我就觉得 Howard Morgan 是一个非常让我。
啊，感到就是很跟他聊天，我很激动。就是我当时在MIT的时候，嗯呃，Jim Simon先生还在的时候，有来我们MIT网上有一个两小时的一个围炉谈话。我当时是本科的那个数学社，就是我们那个活动，我就跟他去去聊。然后所以今天见到我不是今天，就是那一天见到Howard，然后他还在那个硅谷的那个TV show里面就是出现过。
对，然后，然后他就给我介绍了另外一个一个人，然后这个人其实是 Jim Simons 的这个呃表哥、表哥或者表表兄弟，反正反正还挺有意思，他们俩长得还一模一样。就是有一些有意思的谈话，你可以见到很多不同视角的人，然后你可以，我其实觉得我不是一个特别厉害的呃 fundraiser，就我不是，我一般就是这个事情是什么我就讲，然后我一般还把很多就是风险啊什么的我全讲出来，然后是什么你讲的风险？
我当时种子轮我就说，这个我们商业模式并不是非常的确定的。这个我自己做过这个量化交易员，我不知道我们这个东西是不是量化交易。我觉得可能不是吧。对我听说这个还有还是有差别的，跟量化，它效果到现在不如量化好了。对对对，我当时就说，我我虽然我自己在量化中做了一些数学，我觉得你就是作为一个商业模式来说，它一定不是一个。
一个最终的商业模式，我拿这个的举一个例子是说，一个数学比较好的一个AI，大部分大概率上是有用的。就这是一个例子，这不是我们要具体要想的第一个市场。我们具体要想的第一个市场，我也不知道是什么。我们现在是一个种子轮，目前的还是希望把这个东西科技给给做出来。当时反正是这样的一个，就我讲的都特别保守。然后我后来才知道，投资人们一般来说他们见到的创业者们讲的比较，毕竟是一个pitch嘛，他讲的都是比较乐观的。
然后，所以他有一个打折。他比如说，你可能讲说，感觉这个东西是十分，他心里就给你讲一个八分。他有一个这个 conversion rate。我如果当时讲的是一个七分，他就给我打折，就可能打没了。所以，就我或者后面才知道的事情。哦，但是他们都跟你 said yes。对你有被拒绝吗？嗯，有被拒绝，拒绝多还是 yes 多？
没有人想拒绝我们，他们就不告就就没有没有没有人回你的消息了，因为他们其实，在希望做的一件事情是说，呃，如果有有别的人要领头你了，就是他不太确定，他不想拒绝，他拒绝你，你可能以后不理他了，他就他就拖着你，拖着你完了之后看，哎，这个人给了你，哎，那我也给你，就是他是一个这样的一个群体 group think 的一个过程，所以他们后来都跟了吗？
很挺多的，就是那一轮其实挺多，挺 over subscribed 的。所以你核心是需要找到一个领头方愿意 say yes。对，我们当时有好几个领头方的竞拍的一个 offer。哦，几个竞拍？三个。你是怎么让他们竞拍的？我没让他们竞拍，我其实。这是几月份？这是一月份到二月份到三月份。嗯，对，差不多一个月一个，一个月一个，对，领头方。
因为就是价格从一倍到两倍到三倍，就持续你都在聊，你聊了多少投资人？嗯，我不知道，大概几十个，几十个。对，我觉得，呃，就有一点就是，可能说以前做数学一个职业习惯，就是总觉得希望有一个很 optimal 的一个 outcome，就总觉得说希望能够把这个，呃，这个轮做的这个结构好一些。对，然后，呃，也不太知道怎么融资。
嗯，对。后面就学会了一些道理，后面就后面的融资就顺利的多。一月份有一个领头说，我愿意，嗯，然后你没有听，你你为什么没有直接接那个offer？然后还在继续聊，因为他要再录掉我百分之五十，哦。我不可能让他带入下我百分之五十。呃，你当时 said yes，呃，said no 吗？我当时说了 no。哦，但是一月份你就确定你这个事情有戏？
对，所以 Shubal 答应加入了。呃，是二月份的那一个更真一点的一个 offer，就是然后那个时候他加入的。就第二个 offer，OK，但是他还不是最终的 offer，你还在聊。我最终对我还在聊，你聊到了。但是我当时二月份那个我是想接了的，于是我后面我就跟所有人说，嗨，这个这个我是想跟他们走的，就是你可以加入我这一轮，但我可能不会去看其他的其他的 offer 了。
哦，然后到三月为什么又变了呢？呃，因为我觉得就是这个Homer Morgan效应，这个完全就是我作为一个呃，就是我我我我对文艺复兴有非常大的一个这种这种就是这种崇拜，然后而且价格也确实很不错，嗯，就是二月你已经觉得有一个不错的offer，但是你还在聊，对。然后聊到了三月份是那个B Capital，对他是怎么Offer你的？
他他他的一个风格就是，你每一天都会接到他的电话。他他就是他，我当时真搞你。我当时在那个做 rebuttal，我没有时间。就这个为什么这个过程中拖了很长，是因为我还在我还在上课，我还在考我法学院的考试，我还在那个我还在上我的数学课。虽然说就是我去的也少一些，但是就是我还在我有事情，我当时还有 x t，就我当时非常的忙。
Big
I月份不就应该准备辍学了吗？嗯，二月对，但是有offer，我我有这个这个offer，然后当时我就开始，我还没我还没incorporate呢。我去找这个律师去去，我去去就是建立一个公司，又有很多很多当时什么都不知道，没有人完全什么都不知道，哦，什么都不知道，我没有任何的这个孵化项目，我也没有，我我真的什么都不知道，就是到最后是说他们说我要给你写这个
term sheet 了，我这个你这个公司我写什么？
我说我还没有一个公司，就是，哦，所以三月份开始成立公司。二月份，其实其实一二月份，你问我还在做一件什么事情？我在招团队啊，就是我大量的时间，比如说就是在吸引一些我非常渴望能够得到的AI for Math的人才。嗯，Shubal肯定是第一个，对吧？对对，然后但Shubal其实他像他是占有的，然后去去再就我们两个再去找一些找一些同学们。
对，嗯，所以你是几月份出去的？我是夏天辍学的，夏天辍学，夏天那三月到六月在干？那个时候我的那个就是我的工作签证下来了，所以我可以我可以辍学了。哦，对，三月六月在干什么？就是你签了一个一个 term sheet 之后，你要做很多的这个法律的 due diligence，然后他才能把这个钱汇到你这里。你要找这个办公室，然后你又去招人。
当时有很多很多的 AI 人才。在流动，同时AI人才市场的这个价格非常的高，我们这个创业公司无法去支付一个一百个million一一这种这种package，所以我们嗯，当时花了很多的时间与精力在，希望能建一个好团队。对那一轮融资是三亿美金的估值，对融了多少钱？融了六十四六十四个million，就是六千四百万美元。
呃，是比预期低的吗？是比预期高的，预期是五十个million，是比预期高的。对，嗯，你觉得作为一个华人女性在硅谷好融资吗？这个身份会给你带来任何加分减分吗？我觉得我倒没觉得华人女性，我觉得就首先我比较年轻，这应该是一个我加分减减分减分年轻做product是加分。年轻做Deep Tech是减分。嗯，我没有，我确实不像说是我们团队里面的除了我之外的所有人，我没有一个带带带带一个Tech队伍的经历。
嗯，我没有这个Track Record。嗯，这是这肯定是减分。然后。呃，我觉得华人女性这个没有什么，我我我没有什么。这不是一个加减分，对，年薪是一个减分，对，嗯。我有时候我我有时候倒是觉得说，呃。我我我有时候觉得就是呃呃，就是年轻这个事情吧，呃，做做产品的话一定是加分的，但是做产品型，比如说consumer这些start，就比如说Facebook这种，对，嗯，对对。
其实我觉得就是真正应该加减分嘛。年轻，就是我觉得作为一个创业者来说，呃，你要你被要求的是长期进行重复的，呃。高就是非常high stake，非常非常重要的决策，而你的每一个决策给到你的时间是非常短的，所以如果你没有一个很好的一个我是一个是一个word
model一个。一个一个就是第一性原则的一个一个体系的话，你这一些决策容易不太不太最最最最直化，所以我觉得还是我还是希望说，我如果再来一次，我希望我能够在。
再再多多多几年，再就我觉得太早了，嗯，没准备好还。对我觉得，就我我我当时听一些，在在课本十九岁，他十九岁开始，他跟谁他融资跟谁聊，他跟Peter Zill聊，Peter Zill跟他在一个餐馆见面，手上拿了一张term sheet，说。这是这个我的 term sheet，然后扎克伯格说好的，谢谢你，我什么时候能就是什么时候给你答复？
他说我们这餐饭不吃完你不签，我这个东西我现在撕掉。就这是一个十九岁的一个创业者，就没有见过这一种大风大浪的事情。他这个故事就是，他就去了洗手间，他去洗手间哭了一场，回来签了。这上面肯定有他不喜欢的terms，他放弃了他去其他竞拍的机会。我觉得就是年轻创业者真的还是挺，就是当然创业者这个事情就难，就是年轻创业者这个事情就是你你大部分时候你并不知道你自己的这一个决定它到底是对还是不对的，你你你可能等一会儿有更多的信息会能够让你对你自己的决定感到更加的自信，但并不一定让你决定更对或者更错，而你去等这个更多的信息这个过程中是一个高风险低收益的一个过程。
所以就是有些时候你还不如就直接跳下去。就是我我记得我们有一个嗯有一个投资人，他拉我们一群女性的一个创业者去一个一个活动，呃找了一个那个森林，然后在那个森林里就是zip lining，就是你你抓上那个东西你就你就你就你就晃过去，就是一个树和一个树中间有个绳索，你知道自己拴在这个绳索上。我当时我第一次我人生从来没有做过这个zip lining。
我就不敢下去，然后呢？但是就特别尴尬，因为我是第一个人，后面有一群就是女性创业者，他们都玩过这个，好像他们以前可能去年就有这个活动，然后呢，他们就有点等得急，然后我就只能就是一闭眼一咬牙我就下去。这个过程后面他们跟我说，我希望你能形成这种肌肉记忆，就这就是你每一天需要去重复的、麻木的这样的一种take the leap of faith。
所以我觉得，呃。对，这是我我希望可能说，我希望我如果说就是再来一次还是这个年龄的话，我希望我以前就是能够把阅读再再抓紧一点。我可能希望能读三倍的书，我可能我所有所有所有我学过的东西都不够用，这是一个非常有挑战性的一个一个事情。其实就是因为这种高压、快速决定呃的的这样的一个一个一个nature。因为不管怎么样，你在那一刻你得跳。
对，你有遇到？你要绳拴的不紧吧？就就完了。嗯，对，你有经历像小扎那样，跟P Peter T有那样的时刻吗？然后自己在卫生间去哭一场。回来签了，我有一些呃，我倒没哭，但我有一些各种各样的感受到比较艰难的，可能我现在做的这个决定，我以后会后悔，但是我也得做这个决定的时刻。比如，呃，比如说，就是大部分的人才的人才的早期，大部分的人才的情况，就是人在手上有六个offer，你你得竞拍，对。
我成了那个，但我又我没有人家有 leverage，你做不了 Peter Dale，对吗？嗯嗯，那你是决定。出还是不出？你你肯定得出呀！你你你你，就这个这个事情，为什么它痛苦？就是你其实只有跳一个选择，你你只要bias toward action，每一次你在执行与不执行、做和不做中选择那个乐观的选项，你就能够有一天走到那个终点。
嗯，这这其实是一个，但是对，这这其实是一个我的一个一个一个一个感受，就是有些时候其实没有办法去想了，有几次这样的情况，很经常，很经常，很经常。对，硅谷的AI人才的价格已经非常高了。对，但也不单指全是人才的这些，就是有很多很多类似的时刻。对，除了人还有什么？除了人还有什么？嗯，我我们又有一轮融资，嗯，在这一轮融资中也有很多的一些故事，对，呃，或者说是，嗯，就是很多很多的情况下，我觉得就是要让利吃亏，嗯。
啊，每每一天的让利吃亏，让利吃亏，让利吃亏，这样才能够做到一个呃一个一家一家伟大的一个公司。让你吃亏，对，就是让你吃亏。嗯，种子轮是二五年的一月到三月，几月close？呃，都七月close。准呃，夏天close。然后与此同时，你辍辍学，当然等那个签证等了，等了会儿。对对对。然后第二轮就是A轮是二五年底开始的吗？
呃，不，A A轮没想融，A轮在圣诞节的时候。呃，我们已经有的一个呃投资人说，我们要preempt。preempt的意思是，我知道你现在不融资，我知道你没有PPT，我知道你什么材料都没有，我要给你一张一张term sheet，然后我希望你能够直接，现在像Peter秀，希望你能够尽快的把它签掉，这样你就不用再去融资，我省掉你这样的一个，这是他们的这种就是first mover advantage。
有这样一个，我有这样一个感知。一月五号，我被叫到了一个呃外地的一个城市，然后我给了一个 pitch，然后。呃，我拿到了，当天晚上拿到了这个这个这个这个这个offer，然后接下来的一个星期之后，还是一个半星期之后，拿到了另外的一个offer，我们最终签了那一个offer，这是我们的A轮，所以是从呃七月十五号到一月十五号，这个差不多是六个月。
嗯，为什么选了第二个？呃，这是一个很好的问题。其实主要的、主要的呃原因，是就是呃。哇，我觉得就是后面我们也让就是第一个让他也投进来，所以并没有一个他没有特别大的一个一个一个取舍。对对对，就我反正也能够得到就是嗯很多非常长期以来支持我们的这个投资人的这个这个支持与帮助。最终有一个boss的一个一个一个一个解法，嗯，就是领领领头方是谁呀？
领头方是Melo。为什么你觉得他和你可能更契合？对，Mello的这一个partner Matt Craining是一个从我们种子轮开始对我们提供非常多帮助的一个一个投资人。然后他也是本来是他是一个呃电气工程的PhD和物理的本科，嗯，然后他是一个非常technical、非常呃有一点nerdy、非常有意思的一个一个operator。
他非常的就是founder spirit。然后，同时，Manlo又是嗯Anthropic的最大的institutional嗯investor。然后，呃，我们是Manlo Ventures。嗯，在这个呃 ventures这一部分，G and Thorpe之后第二大的AI投资，嗯，他们为什么愿意？为什么愿意？
我觉得他们其实种子轮可能就想投，但我们当时种子轮就是认识的时候比较晚，嗯，就是已经差不多是就定下来了。对，然后我觉得我们在六个月里面，这个团队，嗯，执行的快准狠。这个这个团队在这个六个月的执行中，呃，持续表现没有失误，而且他们在呃从零从从什么都没有，就是第一个搭所有的infrastructure，然后完了之后开始去呃train模型搭系统，然后去做这些决定，就是deterministic。
确定性的tooling，而不是写用Lean这个编程语言去写所有的这个东西，是一个非常，我觉得是spectacularly executed的一个非常完美的呈现的一个工程项目。然后在四个月的时候拿到了葡萄牙的满分，然后在六个月的时候去呃做出了许多呃研究呃问题，没有许多呃一批呃三四个研究问题的的解的解决，然后是没有人类干预的第一个呃自动形式化证明系统。
达到这样的一个里程碑，然后又又发现了一些在代码证明中的一些神奇的 transfer learning，就是，呃，原来这样的一个 AI 数学家能够在代码的验证中，嗯，达到一个非常好的一个表现，嗯，在一个 Verina benchmark 中，DeepSeek Prover
达到了百分之十一，当然这是老版的 DeepSeek Prover 了，我们达到了百分之九十八点九三，啊，对，就是原来的这一个呃，解决普通的这个数学系统。
嗯，所以他是主动pitch的你，完了。呃，我们就是大家都经常有时候会呃定期会见面，毕竟他们是我们种子轮的一个小的一个，他们种子轮放了，他们他们是我们的种子轮百分之一的投资人投资人，嗯，然后现在是呃作为当然作为领投，整个过程整个过程当然会更加的更加的多多几步。对这一轮融资的估值是十六亿美金，对，已经达到了一个独角兽的标准。
嗯，呃，融了多少钱？啊，我们融了呃，有至少是两亿美金，两亿美金，嗯。这个过程中，其实你们团队很多人都就是看起来经验都比你丰富很多，对。然后包括也有非常知名的数学家的加入，为什么他们都愿意让你来做CEO？你刚才也说你是一个就最年轻的一个，然后也没有任何的Tech Leader的背景，他们为什么对此没有顾虑？
我也不知道呀，我也每天在想这件事情，就是，可能，可能他们也没有意识到，我也没有意识到，反正就是大家就一起在执行，然后现在的一个设定就是所有所有的嗯。所有的一些比较 strategic 的一些事情，其实就会就是 route 到我和 Shugo
这里。对，所以我们其实嗯，能够使得研究者和工程师们有很好的一个环境，可以去就是在没有任何 politics、没有任何人事纠纷的情况下去，嗯，纯心的去，就是纯纯粹的去，呃，最新在技术上，然后就是去执行。
所以我觉得这是一个很好的一个 frontier lab 的一个环境。然后，嗯，我觉得还有一个就是这个这个问题，它是一个非常有意思的问题，它非常的宏大，它也非常的困难。然后这个事情又有很多很明显的，一二三四五，为什么这些技术上会难做？但为什么这些通过好的就是 engineering 都能够去解决？所以，呃，我觉得大家其实是被这一个问题，这个北极星去吸引。
嗯，对我只是那个递水的人。嗯，对，你们也算是现在的一个 new lab 对吗？我们是在那个 TBPN 和这个滴滴的这个 new lab 名单上，确实是。嗯，对，你怎么理解？也就是在相同类似时间内成立的这一波 new lab 对？我当时融资的时候还没有 New Lab 这个概念，所以第一轮融资的时候，对对对，所以就是他们就觉得我疯了，就是疯了，投资人哦，就是他们，他们就是可能就是觉得。
这这是什么呢？就是当时，而且还有一件事情，二月份的时候，DeepSeek出来了，当时大家对模型这两个字。就非常的恐慌，大家一听模型啊，不赚钱不要投，就是模型啊，这个感觉模型还不如一个 consumer 产品有 more。但当时大家是这样的一个市场的一个，为什么？因为 DeepSeek 把价格拉得非常的低，对它 commoditized 了模型，所以说大家都不想投模型了。
然后，但是大家没有意识到一件事情，我们不是一个模型公司，我们是一个 deep tech 公司，我们是一个深科技公司，我们做的这件事情有点像 SpaceX。为什么你们不是模型公司？呃，你们我相当于去了一个数学的数学家的大脑啊。对，就是Lean吧，它有一个很古老的一个背景，就是这些做。Program synthesis，我查了一下这个中文怎么说，叫做程序综合。
我也不知道这个对不对。呃，然后呃，program
verification就是程序验证，就是它来自于这样的一个呃古老的一个领域。然后Lean作为一个形式化语言，它目前就是在。呃，公开的这个呃呃的呃domain的的领域的网上的这个这个总的这个tokens这个就是字符串的这个这个这个这个就是不太大，就是它是一个非常小的一个一个数据数据集，所以说就是会遇到很多的问题，比如说你怎么样能够做一个internet
scale一个一个互联网这么大的。
像像有多少Python就有多少Lean这样的一个一个一个数据的这样的一个扩充呢？这是这是一个不太不太清楚的一个问题啊。Lean它作为一个编程语言，又带有自我验证的这样的一个性能，有点像，呃，既是一个呃C，既是一个C这个编程语言，又是GCC compiler和C runtime两者合一，它是一个非常。
Finicky，也就是说非常脆弱的一个语言，它的这个，嗯，它有很多的限制，它有很多的就是。作为里面的这个呃 object，它必须要符合一些种种种种的这个限制，它所以它是在作为一个 lean，它本身又带来了这些挑战。然后呢，Lean里面又比如说，我想去验证一个东西，它真的是在证明，没有给我就是作弊、作弊、作弊。
比如说，我假设公理n加n等于n，证明二加二等于二。你知道二加二等于四，这一定不是一个合法的一个一个一个运算。那么，嗯，我如果要去找一个东西能够去证明它是严丝合缝的，叫verify proof。verify
proof这个东西原来叫做Community里面用的叫做comparator。Comparator这个是比这我们现在我们自己的这个 verify proof 慢一百倍的，也就是说，在我们刚开始的时候，我们必须自己要造一个快的东西，不然我们没法跑。
我们造了大概十二十三个这一些这一些能够辅助这个令能够更好的去去去去执行的呃的，不管是生成还是验证的的的这些工具，然后呃。呃，我们知道说 Alpha Proof 用的是这个蒙 Monte Carlo Tree Search 蒙特卡洛树，呃，搜索，呃，我们觉得这个太贵了，我们看一下我们有多少钱，我们觉得我们做不了这个蒙特卡洛树，我们就得找别的办法。
这个最后其实和呃国内这个字节豆包感觉他们 Seed Prover 做的这个有点相似，这个系统的这个 design，对我没有理解，你为什么说你们公司更像 SpaceX？呃，因为我们有很多的这些技术壁垒，啊，而其实某种程度上，如何去训练一个模型，当然说更高、更快、更强，然后又有很多的一些，嗯，呃，大家的一些secret sauce。
我们这个问题可能在就是他遇到的这个科技挑战上时间会更长。我们至少在种子轮的时候是觉得我们的R&D cycle是会飞的拖得非常长的。我们主要的这一个竞争对手，呃，我们刚刚开始的时候是他们五分之一，只融了他们五分之一的资产，我们的估值也是他们的五分之一。然后他们比我们早开始两年，就是 Tutor 的这个公司，然后他们用了两年的时间才到 IMO 的这个这个呃六道题里做了五道题。
我们觉得至少得花我们很长的一年半、一年，但我们没有想到说四个月我们就往这个普特南冲，我们做出来一个满分，然后接下来冲这个。研究的一些问题，其实都是世界各地的数学教授给这个小野肯老师他发邮件说，就是呃，以色列有一个Technion这个大学的呃L.G. Fell这个老师给。呃嗯，给Ken发了一个邮件，然后这就是Falcon conjecture啊。
然后那个Ken Ribet和Ken又有一些交流，然后有这个Partial van der Waerden。大围城这个波士顿的一个一个一个一个呃代数代数几何学家，他他又有这个一篇文章。反正就是我们其实某种程度上在很大的压缩这个时间，这其实导致我们也有一些Infer上的有些债要还，所以我们现在也有在还一些Infer的债。
小野肯老师对你们团队来说是一个非常有，呃，标志性意义的人。对他像是一个他的性格是一个高中的篮球队教练。哦，他的性格是一个就是他会给所有人就是就加油助威，然后让大家就是非常呃兴致勃勃的呃乐观向上的去去去去去做我们手上的任务的这样的一个人。是你找他还是他找你啊？他是你之前老师对吧？对，他给我发了一封邮件，呃，几月份？
就是你上轮融资已经公布了对吧？但是对，但是十一月呃，我们去年我们我们之前就有邮件的一些就是交流，但是你当时邀请他了吗？没有，不敢对吧？不敢，我也不敢问舒博，我我我不太敢，就是对，呃，因为舒博自己告诉你他要来的。其实我觉得融资也是这样，我不太敢要钱，就是我是我是说你，我没有办法去说服你，你只能自己说服自己。
如果你想做这件事，我也想做这件事，我们可以一起做这件事。哦，对，但我不希望我万一开始引导你，我有可能会误导你。就是这个，大家要大家都是成年人，自己做一些有趣的选择，然后一起去。去去去去承担这个选择的风险，所以你跟舒博的过程更像是我我一直在告诉你我在创业的进展，然后我你等他自己说我要来。呃，我知道他是一个啊工业界元老，毕竟你在director这个level上，我觉得可能也有一很多项目，我怀疑交付的时间会是比较长的，对。
但后面这个费尔，他后面就是这个组织，呃，很多的人都离开了。对对，所以他是自己跟您说他要来。对，他是怎么跟你说的？书包就是在味儿咖啡店说的。他怎么说的呢？他就说好多好的人都走了，感觉这个地方不太像是以前的地方。然后呢？然后就是你要一起做吗？我说好。那个时候你已经融到了啊？对，二月对吧？对，已经有一个 offer 了。
对，嗯，然后他有跟你谈条件吗？就正常吧，就大家就是按照标准的来。你当时什么心情？我挺高兴的，我觉得挺高兴的，因为我觉得感觉一个人做这个事情比较孤单。你有预感到他会来吗？我有预感到，但我我们当时，我当时想，如果他来，应该一年后来。就我们可能，我我总觉得就是，其实我现在对我们的公司现在的一些新加入的一些成员，我总一种我总有一种就是，我感觉我我们就是我们希望我们能够把我们做的做得最好，然后我们能配得上他们的这种价值。
所以我当时想，哎，一年了，这个可能做出来一些小成绩，然后这个叔伯可以来指点江山，把我们就是往往上再做一步。当时是这样一个想法。那你的老师呢？老师对他他给我写了一封邮件，十一月底非常怪的一封邮件。他大概意思说他要来湾区。我说啊，你要来湾区？然后他说，嗯，如果他加入了OpenAI或者是DeepMind，呃的话，我不应就是他他希望我有一个心理准备。
然后我心想，你要加入 OpenAI 和 DeepMind，那你为什么不来我这里？然后我就说，你可以来我这里。然后这个时候，你之前没有跟他说过这话是吗？没有，我我哎我，但是我但我就觉得，你如果能够去加入 OpenAI 和 DeepMind，我觉得你可以来我们这里。我觉得我们他说那句话是在暗示你吗？就是说他是真的，我觉得需要一些建议哦。
他他当时OpenAI可能给了他一个offer。哦，那为什么他说的是你要有心理准备？就是因为我们他我们知道我们知他知道我有这样一个公司嘛，有可能会可能会有一些竞争关系，对吧？OpenAI的AI for
Math的这样的一个division可能和Action会有一个战略竞争关系，他可能作为我们的我们是朋友嘛，他不希望我呃很突然的听到这一个消息，就是他在给一个竞争对手进行工作哦，所以他希望他能告诉我说可能这是他的一个选择，也希望我能够理解。
然后我说那来Action。哎，然后结果就谈的非常快，非常好。他是来完全跟你谈的，还是线上自由谈？没有，就这么谈的。我当时就，嗯，我当时飞飞的乱七八糟，十一月底、十二月。从我是从这儿飞到了，呃，飞到了拉斯维加斯是 reinvent，然后飞到了这个 new reps，呃，我们在那个 new 赞助这个
AI for Math 的 workshop，然后我们有一个就是活动，可以就是招聘的一些活动，我就在 San Diego， San Diego 回来，然后是这个，所以就一堆一堆事儿。
嗯啊，你怎么说服他呢？在你们那个 Zoom 会上？你你说你你对你你对比 OpenAI 你的优势是什么？我我倒没 sell 他，我就说我们非常的就是呃，我们也 Open 你来，然后你可能还是得去 OpenAI 看一看。如果你能有时间来我们这边看一看，结果他没时间来我们这一看，我觉得肯定凉了。你想他来湾区，他就直接去了 OpenAI，然后就飞走了，他没有在我们这儿，那可能说明我们没有什么机会。
结果他来了。哦，他来你公司了。对，他是来你公司跟你谈好的。对啊，没有，他没有来我公司谈好，就是他他在Zoom上，我们就就定了。你你截胡了OpenAI。对。嗯，你怎么说服他的呢？他被什么打动了呢？我觉得首先他觉得我们的嗯，就是这个团队更数学，这是一个事情。嗯，就是我我怀疑发生的事情就是他去了OpenAI之后，可能觉得那边比较呃。
做数学的同学不是特别多，来我们这边的话，可能有更多就是数学的一个氛围。这个这个公司的DNA和专注点就是数学，而不是一个general的AGI。然后数学是其中一个部分，可能更有marketing的成分。小野肯被认为是继承了拉马努金精神的现代数学家之一，而且他之前说他根本不相信AI会超过自己，然后后来他内心发生了变化，可能这是他联系你的一个契机。
我我觉得是对，他有跟你说过他这个。认知是怎么发生变化的吗？他有说对，然后我我其实记得就是我们当时聊的特别的仓促，因为这就是一个截胡哦。对，多长时间？呃，就是两三天内。OK，因为那边那个offer要要要要要爆了，就爆炸explode哦。那我们这边我觉得还有一个很大的原因，看加入是因为 Francois Charton。
Francois Charton 是 AI for 数学的这个嗯的二零一九年 Francois 和 Guilhem Lample Mistral 的这个 Chief Scientist Co-founder，他们一起写了一篇文章，叫做 Transformer 可以在呃微积分上，在在
Integration 上能够比一些像 Mathematica、Mathlab 这些电脑系统要电脑代数系统要做的好，然后。
从那开始，房朔就一篇又一篇的去去做了非常多重要的文文的的工作，去去让这个AI解决各种各样的就是specialized的就是特殊的数学问题。然后，在AI for Math这个领域里面，我觉得就是Can还有Franc，他们肯定是对对方也非常惺惺相惜。然后Franc作为我和Shubal之后第三个来加入我们的，就是我们我们这个团队的，他们就有很多的共同语言。
嗯，然后事实上，现在看加入之后，又有 Evan 呢，Kenny 啊，居建，就是就变成了一个，It's called Math Club，就是我们这里有一个数学俱乐部，大家都有很多可以聊得来的东西。然后他也给了我们这个 Action Power 去解决哪一些问题选择这个问题啊，给了很多很不错的建议。嗯。
我想多问一个关于小约肯的问题啊，他是一个什么样的人？他就是我这那个高中篮球教练，他就是特别特别乐观，特别嗯。特别就是让人你跟他聊，你就会觉得，哎呀，我本来就很想做这件事情，我现在更想做这件事情了。所以他是我们特别好的一个文化上的一个一个一个一个增加。然后他也是，当然是一个非常好的数论学家，他在这个划分函数领域里面就是。
呃，非常年轻的做出来非常好的成就，然后他也是一个很好的研究导师，他带我做了很多文章，然后还有很多其他他这个R E U的同学都成为了呃不错的数学学者。他是个直觉派的数学家吗？这个我倒是不知道，哎，这是一个非常好的问题。我觉得他应该比我更直觉派。嗯，对。但是我比如说，我们就是合作的过程中，像我一个合作者张胜彤，他就是比肯定是比这个我和呃Can我们他比我们两个都要直觉性。
所以就是Can，我觉得在二者之间。看哦，Can的这个我我理解了。Can的这个神奇的能力在于他是理论建造者。数学里面的大概分两种，一种叫解决问题者，一种叫理论建造者。他能够把不同的领域的东西去去去连接起来，然后有一个完全全新的视角看一个问题。他能够去发现很好的问题，并且给其他可能更善于解题的同学们去做。
嗯，他会觉得。他从学校放弃了终身教职，加入一个学生创创业的公司。他会觉得有某种奇怪的感觉吗？我没觉得，我觉得Ken反正和我我们两个都是比较就是呃叛逆的人，对，就是我觉得呃Ken这吧，这个他在数学教授，他同时又是美国这个奥林匹克游泳队的这个教练，去给他们分析这个游泳的数据，怎么样去把表现更好的提升。他又去拍这个好莱坞电影。
拍了拉马努金的那一部，现在又要拍第二部，拍这个米尔扎扎克哈尼的这个这个呃第一位女性菲尔兹奖得主的这个这个电影。然后他同时又呃做很多的呃，就是他有一个慈善基金会，就是以拉马努金命名的，去给一些很年轻的世界各地的。希望能够呃拿一些资金去买数学课本的同学们一些一些一些辅助，同时他又是美国美国数学学会的前前任副主席，然后又是。
呃，在白宫又有一些这个政政政政策上的就是呃呃呃咨询顾问的一些职位，所以就是他是一个非常非常全面的人。他作为一个数学家，然后加入一个AI for Math的公司，建造一个类似于呃AI数学家。会替代自己吗？他倒不觉得会替代自己。他我们其实大家都觉得，就就我觉得他就是思想非常开明。作为一个数学家，有一些数学家可能真觉得，就是AI去代替自己不是一件好事情。
但是我们见到的越来越多的，比如说Cam，比如说Andrew
Granville，那也是另外的一个很好的加拿大的一个数论数论家。呃，也啊，这这个Andrew也是我们，就是他也是著作等身的一个数论学家。他们其实一个想法就是，随着AI的进步，人类数学家会学习在不同的抽象层面上进行逻辑推理。这是一个非常有意思的一个点，就是嗯，我们某种程度上在呃编程这一块儿，以前编程我记得，如果你去这个计算机博物馆，就在这附近，嗯。
以前就是电脑计算机，就是有那个小卡片儿，然后在那里打洞，就是那个那是很很早以前的一个呃 computer science 的一个雏形。后面有一些更呃 low level 更低层的这些编译器语言，然后一直后面到 Python，现在到可以拿自然语言进行 web coding 编程。然后数学其实某种程度上，数学家也会学会有更更高高层的这个抽象的这个思维。
比如说我刚才讲的，有可能他们就是去说这些问题是值得去探索的，让然后让这个AI去帮他们探索。我们希望，我们真心的希望，我们的AI能够有具备一定程度上的猜想能力，能够让这个猜想的这个部分与证明的这个部分进行某种向上螺旋。就是我希望它能够随着这个 action improver
能证明的东西越来越多，我们每一天证明的东西都会进入到明天的呃明天的这个这个这个这个这个应用中，不管是作为一个 skill 一个技能，就像 lego improver 的 skill library 这个这个这个这个设计。
或者是去呃作为未来的这个训练数据，我希望它一定是self-improving的。某种程度上，self-improvement甚至说你可以叫它continuous learning。当然，这是一个最近很火的一个词，一个buzzword。在一个能够有呃验证signal的验证信号的一个领域，像数学来说是可以去试验的。
这些很好的、很前沿的，呃的A I的一些一些东西，包括sub agents skills M C
P这些东西，全部可以在我们现在的这个呃数学作为一个操场一个playground上可以去实验，嗯。你们在普特南的那个呃对对那个故事可以给大家讲一下。好，就是大概就是在二零二五年十二月六号这一天早上，我们收到了呃就是普特南大学生数学竞赛当天的考卷，然后我们是拿到那个考卷之后，就我们要做的第一件事情就是我们需要把它呃变成形式化的这个题目，让这个Action
Prover我们的这个AI系统去去做。
那我们这个呃。题目当时其实挺有意思的，早上六道题，下午六道题。如果这个题目本身是一个证明题的话，那么就可以直接就是把它变成形式化；如果是他说要求解的话，那还需要求解。所以其实还是一个挺有意思的一个过程。我们所有人都在这个办公室的一个庞克瑞庞加莱这个会议会议室是我们的这个war room我们的战争战争室，我们就是在他们数学家有些人就在解题。
所以，其实就是解解解题的这个过程还挺有意思的。就是我们我们可以看到说，嗯，有人类的解法和就是我们最终这个 X Improver
产生的这个完全是不一样的一个思路。我们在呃大概当天下午三点五十八分的时候，我们是发现我们有八道题。然后我们有八道题的话，呃，就是呃八十分，八十分是一个什么水平？八十分一共一百二十分，去年的八十分是世界前五，然后呃，但是往年他八十分可能不是世界前五，前前十、前二十差不多这样，然后我们。
然后我们就希望能够拿到一个九十分，因为我们当时就有一个选择：我们是否告诉世界我们做，还是我们再等一等？然后我们最终确实是有，就是十二道题，就是全部满分。然后这个过程还挺有意思。当天我记得就在解题的时候，就是呃，小野肯教授他有在有一些非常有意思的精彩语录。然后我和舒博我们两个人就是笑的，就是前前仰后合。
他说：“嗯，不要在现在不是说数学纯粹之美的时刻，不要去精确的去搞这些东西。现在是战争状态，就是在大家在求解的时候，他就说能怎么快捷的去去。”去做就怎么快捷的去做，就得到那个数之后喂进这个 action provider，也其实是和呃 IMO 的这个其他的这个标准是一样的。就是说，如果有需要求这个解法的题，把这个数就是一块的喂进去。
因为Lean只能做证明嘛，它不能够帮你说是去求解，所以求解是人做的，是吗？求解这个东西是人做的，求解在IMO的那一个就是IMO的那个考试中，甚至是二零二四年，其实这是Alpha Proof它给的先例，就是有六道IMO题，然后有一些题要求有一个得数，这个得数的话，就是要把它一块放进去变成一个证明。但是后面我们发现一件事情，就是我们其实可以不求解。
就我们其实，因为我们这个系统里面也有一些就是 informal 的这个
model，其实我们是可以直接让它就是做出这个解法的。最后其实我们发现，我们的每一道普通难的题，其实我们并不需要做人类求解那一步，但我们以为我们要求解，所以还挺有意思的。小小野很教授，为什么说现在是战时状态啊？因为就是时间紧，就是我们大概估计说，一般早上六道题，下午六道题，加在一块儿十二道题，最多不超过三道题需要求解，因为确实是少数的，大部分还是证明题。
早上那道试卷下来就是六道题，四道题要求解。然后我们当时只有就是能做得动这个数学题的人，呃，就是基本上就是我普通男成绩也不怎么样，反正基本上就只有安文晨。然后艾文陈就一个人在那里，就是一道又一道题的做，还是非常非常有意思的。我们其他其他同学有些人就是在就是把这个数学题变成Lean，然后啊呃看他自己其实也没有做出来多少道就是putnam的题，因为就是研究型数学家和就是这种打竞赛在一个最最短时间内的还是很不一样的一个数学家的一个一个一个特性。
你们公司为什么叫原理啊？啊，我觉得 axiom 是非常美的词。就是我自己很小的时候有一本书，就是叫《数学天书中的证明》，就是说，呃，如果说上帝有一本书，这本书里面会有哪一些题？数学天书中的证明，就是说，呃，有一些这样非常好的数学结果。呃，我觉得就是公理给我的感受就是。首先，把它跟Lean这个形式化语言它是呼应的，就是从一些有限的一些公理中可以推导出新的一些结果，就像是有地基，然后你再往上建高楼。
呃，另外一个我觉得就是，呃，action这个词就我觉得很美，它很数学，它很它很克制，它很理性，嗯，它又很sharp，它就。反正我我非常喜欢 axiom 这个词，他就感觉来自那本天书。对，然后我们公司里名字开头是 A 的人也特别多，我们 Alex、Alberto、Arum，反正一堆，这名字开头是 A 的，我们是 axiom。
你觉得 AI 会把数学的历史推向一个新的阶段吗？会，我觉得会，我觉得这是非常的让人激动人心的一件事情。就是我随着这个我们以前的这个世界能够做到，呃，比较顶尖的数学思维的人是很少的。我们现在会成从一个math poor到math rich的社会，我们会从一个数学呃数学的匮乏到数学的的丰富的的的的这个这个这个这个supply这个供给会会爆炸，这是一个让我个人来说非常激动的一个。
一个野心就是：你想一下，所有没有被解决的理论问题，所有可能说是应用科学家们他们遇到的，希望有一个数学家帮他们解决的问题，全部可以解决，就是一个一个一个一个。一个一个一个时代的，一个时代的，我觉得一个可以被定义就是说，指数级的数学发现的增长，这个我觉得一定一定会发生。然后数学家们会扮演一个什么样的角色？
数学家们我觉得会扮演的角色就是他们能够提供最好的直觉，他们会是能够提供那百分之零点零一的直觉，说哪一些数学问题比起哪一些数学问题更值得我们去集中算力去解决。就这，我我我我可能会讲一个。这个这部分会听起来显得会非常激进，我觉得这个就好像说是很多不同领域的数学家，他们比如说三四十个人，或者说是十几二十个人会聚起来去谈论说我们的wish
list，我们未来希望的这一些问题被解决，然后这些问题的重要性，这些问题的连接性，也就是说，如果你解决了这个，你应该能够把这一些都解决。
这样的这一个过程可能会是他们的主要的数学工作，然后实际上是由这个AI数学家去解决这一些问题。嗯，比如说，如果我们这当然是两种情况，我们人类有可能有有限的算力能够去我们人类决定花在数学的发现探索上。另外一种情况是我们其实某种程度上能有很多很多的算力，我们可以花无限的算力在在在这个数学探索上。这个当然也包括说，呃，比如说现在我们可能能够用更少的算力做更好的事情。
如果是有限的话，数学家其实他们某种程度上就是这个资源分配者。他们的直觉告诉我们说，我们应该比如说两百个 H2 单值花在这道题上，八千个 H2
单值花在这个题上。某种程度上，算力就会成为呃去去与这个数学家对于这个数学题的重要性，某种程度上画一个画一个等号。这是个资源分配问题。如果我们现在在一个无限算力的这样的一个一个情境下的话，那就是呃，像是那个Demis Hassabis那个Thinking
Game思考游戏那个纪录片里面有一刻，他在一个这样的一个会议室里面，他说。
AlphaFold已经就是做出来了，他们刚拿了那个奖。现在下一步是什么呢？他的手下的一个一个科学家就说：“我们做一个平台吧，让这些结构性生物学家可以去，呃呃，去提交他们希望被折叠的这个蛋白。我们折完了，我们给他发回去。”德米斯坐在这个桌子上，就问说：“有多少个蛋白？”然后人家说有两百个million，两亿个蛋白。
然后，德米就把笔扔在桌子上，然后就说：“结束会议吧，就是 fold everything。That was a stupid
idea。那个平台为什么你去做一个平台呢？你可以把所有东西都折了。如果我们在一个无限的算力上的情况下，我们就要做这件事情，我们要把所有能够人类想到的好奇的数学问题全部解决。”所有与应用科学家、物理学家他们就是嗯在意的一些问题，比如说很有意思的一件事情，中国剩余定理现在被MIT的这个Elafeet去用在研究这个有多少个神经元能够叠起来，这个neural
capacity。
你是这个空间里能够有多少个神经元？这样的一系列的研究中，我们做梦也不会想到数论会与初等数论会与会与这个计算机神经科学、理论神经科学产生关系。另外一个例子，比如现在整个的这个法律与经济这个这个文献都是啊，两个人，一个是斯坦福法学院的这个 Mitchell Polansky，我当时上了他的 Law and Economic 法律经济 seminar。
然后，另外的一个是Steven，他是在这个MIT，我忘了他的last name。但他们两个人就有非常多的，就是关于法律与经济怎么样去想。比如说，我有一个刑法，有多少是呃用来呃让这个社会不要犯罪，有多少是实际上是对这个人他个体的某种程度上的修正与惩罚。这个过程可以拿就是微微分方程去，它就是有非常非常多的。
我在法学院的时候，就是还帮他算了挺多微分方程，就是能够去去去去解。就是数学其实可以被应用在这个呃Ten Gowers菲尔兹奖，它有一个非常著名的一个。一个一个话就是为什么我们国家基金委什么的需要去继续给，呃呃纯数学去提供这个经费呢？是因为数学是一个生态系统，你有纯数学，你就有应用数学。你这个纯数学如果死了，你应应用数学也就没了。
你你可能确实觉得你作为一个呃一个政策上呃这些应用数学更与实际的这个市场啊与社会更有关系。但是如果你不去做这些基础科学的这个，当然这个也与其他就是学科，比如说生物的基础科学也是一样的一个一个一个一个一个一个一个一个论点嘛。就是说，你一定要去进行通过理论层面上的发现。我认为，从数学 math，然后到 code，到这个这个编程去。
在软件层面上去做一些，甚至就可以到 real world testing 实际世界上的一些验证。数学和代码某种程度上是孪生兄弟，math is coding，code is math，math is code，因为有一个叫做呃，Curry Howard。呃，对应就是它是一个Lean，就是基于这个，我每一个数学证明可以变成一个一个计算机程序。
Code is math，为什么？因为Code现在我们发现，为什么Backend甚至是整个Distributed System的Web Coding没有办法做到像就是嗯做一个网站这样这么好？其实就是因为它有很多的一些。啊，没有办法 backtrack，没有办法做很好的，呃，就是 hierarchical，就是分分级的这种拆解，对这些能力，其实某种程度上数学能够给到。
然后数学和编码的这一对儿孪生兄弟是一个你能够在这我们现在这个人类世界上有这个验证的验证信号的一个一个一个一个一个方面。另外一个部分其实就是呃实际世界里的这个呃实验，对吧？比如我扔一个鸡蛋，它的重力会到这个地上，鸡蛋会碎，就是这些实际世界里给我的 reward。所以我觉得我们的 AGI 的这个 worldview 就是数学。
然后编程，然后呃实际的这些是 rule testing，然后 everything else。嗯，对。你觉得在 AI for Math 领域会诞生类似于 ChatGPT 时刻吗？啊，我觉得会。然后我觉得就是如果有这样的一个 ChatGPT 时刻，它呃不单只是数学，它一定还会有一个嗯就是 coding 代码的这样一个部分。
嗯，其实其实这个事情其实挺有意思，就是我们做的这个东西，很多人觉得是，嗯，它对就是验证它有很大的这个意义，然后对另外一些人觉得这个对超级智能或者说就是数学推理有很大的意义，它其实某种程度上这两者是是合一的，嗯，这个我觉得比较。就是这是一个可能不太明显的一个一个点，就是我们我们是在做一个就是AI的一个数学家，但是我们又同时是通过形式化证明，就是加入进传统的，比如说就是L
M推理这里面去去做的，所以我们产生的这个输出是可以，比如说几几千行就是Lean的这个代码，然后这个东西它完全可以就是自我验证。
呃，如果我觉得有这样的一个 ChatGPT 时刻的话，它某种程度上产品一定要加进来。就就这是一个，我觉得我们时时刻警醒自己，就是作为一个，就是在把这个系统就是能力建到越好的时刻，其实要要记住，就是说某一天这个东西一定是要尽快的去产品推出和落地，这是一个点。然后我其实觉得。就是有一个Chat G P T时刻，然后前年可能一般有一个，比如说，有点像当时早期的时候，大家说就是Alpha Go时刻。
其实我觉得Alpha Go时刻对我来说是两个时刻。第一个时刻其实可能是这个，嗯，Google Deep Mind在二零二四年拿到的这个二十八分银牌。另外，对我自己个人的一个Alpha Go时刻，其实是在。嗯，今年的就一月份的时候，Axiom它去能够Axiom Prover证明像Falcon
Conjecture、Van der Waer Partial Van der Waer Conjecture这些，包括同时I think就是就是Deep Mind有一个Alita，那是一个非形式化的，那是一个就是自然语言的一个，它也证明了一些研究问题。
其实我觉得是这。这两个时刻吧，一个是奥赛数学，一个是研究数学。你觉得 AI for Math
它会沿用就是大语言模型的这一套整个的技术范式吗？还是会在下面上面做新的创新？呃，我觉得就是它是一个很好的你想试什么试什么的一个环境，就是我们环境，它是一个。它它是一个，就是它是一个很好的一个设置，就是你可以在上面去试你认为一些会成功的一些事情，然后这个可能在别的一些没有那么呃 clean 的一个
domain 上不好做，就是在我们这里，我觉得我们可以做。
然后比如说，我觉得差不多 AI for Math 有一套范式。对吧？就是从 draft sketch improve 开始，二零二二年的一篇文章。首先呢，你让这个 informal 的模型给你列个提纲；其次呢，你把这个提纲变成 formal 的，变成 Lean 的；然后呢，你再把这一些中间 sorry sorry 是 Lean 里面的一个一个一个 tactic，一个一个一个语法。
它这个 sorry 的意思就是说我这一块。我不给你证，但是你你知道，就是它一定是对的，相当于是让让让你把它 take it for granted 的这样的一个，就是第一步就是 draft 提纲 informal，第二步 sketch，啊这个提纲 formal，第三步 proof 把中间的 story 全填上。
其实填sorry有好几种方式可以填，你可以拿这个AI去填，你可以你你可以拿一个就是有neural network的，你也可以通过一些就是原来ATP的那一些纯规则的，没有这个没有这个rule based的，没有这个AI的这个。去拿这些东西去填，就是让它自动的。比如说，Hammer Lean里面有一个东西叫做Hammer，就是Hammer，就是顾名思义一个一个斧头。
斧头就是我一斧头下去，这个Story就没有了。这个Lean这个Hammer的这个历史其实特别有意思。很早以前，其实有。其他语言像 Isabelle 是另外的一个定理证明的语言，然后另外一个定理证明的语言叫做呃 Coq，后面改名叫 Rocq Rock。他们就是有 Hammer 了，就是说有一篇非常呃
Max New Hammer，他是我如果记得没有错的话，他是 Isabelle 的一个一个一个 Hammer。
Lean 里面一直没有一个 Hammer，直到我记得去年六月有一篇文章，就是 CMU 的几个人出来一个 Lean Hammer，但是 Lean 的 Hammer 它并不足够。它的这个就是功能并不够涵盖所有其他的 Hammer 的尝试，所以大家就是我们当时就有跟 Lin 呃的这个创始人 Leo
Demora，我们说 Axium 希望能够就是做一个就是我们给你 basically 我们给你赞助，你你能帮我们找人做一个全部开源的给所有社区的一个 Lean Hammer 吗？
后来这个他们可能是人力上就是不够人，他们不是说没有这个资金，所以这个事情没有做成。但是到就是今年的时候，有一个新的一个东西出来了，叫做Grind G R I N D。Grind这个其实某种程度上，它能够解决很多的数学的问题。我曾经见过一些其他的AI for Math数学公司，它有做一些demo。其实那些题，呃，你如果Grind一下，甚至它都能直接给你做出来。
这里面没有任何AI的一个成分。我们觉得的这个世界是。AI和这个 formal verification 两边就是就是就是两两股力量，就是合在一起去解决一道题，就是能够用 deterministic 不上这种这种这种 probabilistic 概率性系统的，我们就就就是拿这些东西把它解决，然后另里面自己能够做出什么样的抽象层，能解决一些，也能尽量解决一些它。
就是我觉得一个很好的一种系统设置，就是说先是最简单的、最便宜的，能解决就就解决掉，不然后剩下的再去上这一些，呃，这比较大块的这些、这些、这些，就是啊，大语言模型系统有某种让你觉得非常啊哈 moment 的时刻吗？对我，我觉得我们每天都是啊哈 moment。我觉得这个这个团队还是挺快的，他们就是。其实我觉得有几个呃东西，我觉得可能是比较比较前沿，可能就是其他人没有。
就是第一个，就是你如果觉得呃呃呃Monte Carlo Tree Search这个蒙蒙地卡罗树搜索。太太太费钱了，就是太效率太低了的话，你有什么别的办法？你我们希望能够 scale inference，把 inference 这里就是去呃做做做大，嗯，这个的一个一个我们觉得可以尝试的一个办法，就是可以看一下 Anthropic，它有最近讲的一些 sub agents 这样的一些方向。
其实我们觉得 sub agents 送来做 AI for Math，其实做的很好，这个是一个。然后，呃，David Silver 和这个 Richard Sutton 他们写过这篇文章，就是 AI 后半场这个，呃， learning from experience，从经历中进行学习，嗯。这个东西其实某种程度上，在一个数学题里，什么是一个经历？
这个经历就是一个数据的trail，一个一段到达你最终解决这个题目的这一个部分，这个过程全部可以作为你的这个experience经历。然后，呃，随着你能够让你的这一些 sub agents 能够应用的 skill，而 skill 就是 learning to use
tool，学会使用工具。那随着这些种类选择种类变多，你可以去做 scaling learning from experience 这一些东西，我觉得我们做的比较前沿。
这是这是一个一个我自己个人的一个aha moment。所以一个数从比如说四十个四十个node四十个顶点的一个一个一个数一个一个一个一个证明就可以把它转化成一个数。这个数从四十个我们已经现在scale到四千个，就是它是一个更深更广的一个。就是，这是，这是第一个，我觉得我们可能做的不错的一个点。第二个，我觉得，嗯，有一个我们的aha aha moment。
其实是就是我们发现这个数学的这个定理证明的很好的一个AI theorem prover能够转化到它很强的代码验证能力，对，有一个。我觉得就是在这个 Verina Benchmark 上的分儿，是我们看到了一个让我们都很惊讶的一个一个事情，然后同时可以生成代码和这个证明。其实这是一个很有意思的事儿。如果你想就是正常的一个代码是Python，然后证明是英语，就是自然语言。
那如果你去做就是强化学习的话，你相当于它指指着你往两个地方走，你你到底是Python做的好还是自然语言做的好？但那你如果说是你把这两个目标函数把它就是聚拢起来，你让你的这个代码和这个这个代码的证明，它都是Lean，或者说甚至代码不是Lean吧，它是Rust，它也是一个呃，它也是一个就是Lean是Dependency
Type Theory，这个Rust是一个Strongly Typed Language。
它可能就能够让它这个收拢，反而能够能有更好的一个 verify generation，就是验一边验证一边生成的这样的一个一个时刻，这是我觉得第二个，我我觉得我自己觉得比较美的一个东西。对，为了更好的理解 AI for Math，能不能给大家讲讲，就是在你的心目中，AI for Math 它在整个 AI 的大地图上，它应该画在哪个地方？
能够给大家一个 mapping 好。呃，AI for Math，我觉得现在就是convert收敛到大家差不多，其实是一个做法，就是我先拿一个。Open source 的一个开源的一个一个一个几呃一个先训好的一个母一个模型，比如说我拿这个 Quan 或者我拿这个这个这个 Quan
的一个模型，然后我在上面去做就是啊做后训练，然后做后训练大家做法不一样，有些人就直接上 R L，有些人是 S F P 然后 R L，然后最后做好了这样的一个一个 model 之后。
把它就是去可以说是呃放到一个系统里面去，然后这个系统里面有各种各种各样的。model有一些model还可以做一些就是非常specialized的一些东西，然后这一个系统差不多它去call一些tools，然后这些tools一些tool其实还蛮难做的，就是要做很多一些Lean的meta
programming，然后这整个的这一个这一个系统的这个设计有不同的不同的方法，我觉得差不多是是现在是这样的一个，大家其实都是差不多这么做。
然后我觉得还是有一点点不同，可能我觉得我们和，呃，像Seat Prover、Hyper Prover的做法都比较类似。然后我觉得好像是，呃，比如说Aristotle，它和这个Alpha
Prove以前的那个做法有点类似。其实大概分两派。然后呃呃，基本上我们比如说呃，就是邀请加入我们的同学的这个AI的这个过往的的工作都是呃后训练呀，就是强化学习呀，然后就是做reasoning做推理呀，然后也有招一些做agents甚至 swarm of agents的一些同学，然后嗯就是。
非常 full stack 的这个 engineering skill 也非常需要，差不多是这样的一个一个东西。我看了很多研究资料，我会觉得，如果 AI for Math 突破了，对它应该不会是指解决 math 的问题，它应该是具有泛化性的。这个观点对吗？对，呃。这是一个很有很有意思的点。我觉得A I for Math大家其实讲的一般讲一个核心科技叫做Proving，就是证明。
其实我觉得A I for Math它能做的东西。也就是说，能达到一个更更多用处的，其实是一整套一整套东西。我觉得你需要有一个非常好的一个prover，一个证明的系统；你需要有非常好的一个conjecturer，提出猜想，能够提出数学问题的这样的一个一个AI。然后，其实某种程度上，这一个能够证明的AI是你能够提出猜想的这个AI的reward。
就是我能够拿它去拿这个证明这个 prover 去去做这个 conjecture 的这个这个 reverse signal。其实有一篇文章叫 self-play theorem prover，就是自我自对弈自对弈对自对弈。然后这个其实是呃董克凡，然后马腾宇他们就是这篇文章斯坦福的一篇文章。然后呢，它其实这是其实是所有人开始想就是 conjecture 怎么做猜想的模型的这样的一个一个起步点。
呃，猜想模型的难点是。我不像证明模型，我证明出来了就是一，没证明出来就是零，我没有这个reward了，我怎么去说我这个猜想是好还是不好？然后除了说拿这个能够证明的这个东西去做一个grounding，去做一个。呃呃呃，去给他这个这个信号之外啊，还需要加一些其他的东西，比如说怎么知道你这个猜想是否在数学上是非常无意义的？
比如说你完全猜想出来了一个不是那么重要的东西，就是。一点儿也不重要，我我也不知道为什么你会让你的prover去证明这个结论，那就可能会有一些东西叫elegance filter，elegance filter叫做去去判断这个东西是否优雅。然后在这个STP这篇文章里面的这个优雅，这个优雅不优雅是靠长度决定的，就一个东西它的题目与比起它的这个证明来说是长还是短，这个是优雅不优雅。
然后，但是这个感觉上就很粗糙，因为他们其实他们的那个数据集是叫 Lean Workbook，是一个呃比较是高中数学的一个一个一个数据集。呃，完全这个东西如果做到更高级的，比如说本科或者说是就是博士研究的的话，你没有办法去靠就是长度来就是绝对作为一个唯一的一个优雅的一个过滤，所以没有没有没有什么就是没有特别。
没有特别强的延展，延展就是难难度提高的时候，这篇文章不不足够，嗯嗯，所以就是怎么去做这个这个这个猜想，目前是一个我觉得比较就是前沿的一个研究问题。然后这个猜想的这个呃猜想家和这个证明家，他们俩就是要聊天儿，他们俩就是通过通过就可以self improving就可以自我提升。然后呢，他们他们还有一个很重要的一个部分是叫做由于尤尤其是我们在做形式化呃数学证明，叫做就是啊知识库。
这个知识库为什么很重要？是因为大部分就是存在的数学，在英语里面存在的数学，或者在中文里面存在的数学，它都不存在Lean里面，它连定义都不在Lean里面。所以说，我需要一个很好的去，嗯。我需要两件事情。第一个，我需要能够很好的搜索我什么是已知的、已经被证明的，什么是需要被证明的。然后或者说，甚至说，如果你让我证明一个东西，我在已知的里面找到一个反例，那我就直接可以证伪，对吗？
然后另外一个需要的就是说，把这一些浩如烟海的数学转化为形式化的数据。转化为形式化的数据的话，这个过程就是我说的第二个核心科技，叫做 Auto Formalization。它就不是证明了，它是转化。嗯，它这个转化其实某种程度上，一是被忽略了，因为大家，比如说你如果证明了很多普特南的问题或者IMO的问题，你就可以到Twitter上，你就会说，嗨，我证明了，我是一个非常伟大的AI数学家。
但是如果你只是把这个人类已经就是发现了的、写好了的数学转化为了这个形式化的，你会得到更少的这个赞美，但是这个科技它其实比这个证明要更难。至少是一样的难度。我其实觉得是更难。为什么更难？就是，呃，如果说我要求比较严格，我的输入是一个 archive 上的数学文章，而我的输出要求是把这个数学文章里面所有的定理证明的这个对儿，这一对儿东西变成 Lean 的这个代码，成为了我的一个 Lean 的这个输出。
那我需要几步？我第一步，我需要把这个呃文章变成拆分，我要拆分出什么是啊什么是呃就是单个的定理和这个证明。有一些文章它结构性的比较好拆，但有一些文章一个大的证明里面可能能拆出好多东西。这个东西如果拆的不够细的话，拆的非常细的这个东西叫做什么？叫blueprint蓝图。呃，陶哲轩呀，还有说是嗯，就是呃，Kevin
Buzzard呀，Alex Kontorovich这一些数学家们，他们用他们用人手写出过蓝图，嗯，他们曾经就是在PolyMath，还有就是后面的一些呃大型的形式化的这个这个项目上，他们人手写了这个蓝图之后，去丢出去给全世界的本科的一些数学的这些学生去。
每个人领一个小任务，然后所有这些人小任务加起来，星星之火可以燎原。就整个的这个东西就形式化，就就就就就就就就就写好了，嗯。然后，如果你需要让一个一个一个计算机，不管是AI还是一个就是Robust的一个电脑系统，去进行把一个从一个PDF一个Archive
PDF到这一个非常细的蓝图拆分，譬如说二十页的一个文章变成一个两百页五百页的这样的一个蓝图拆分，使得我能够把这一些蓝图非常细化的东西转化为Lean的话，这一步是非常难做的。
嗯，这个需要很强的这种。呃，就是分解这种分解推理能力，然后，呃，所以这其实是一个难点。然后，所以我其实讲的这整个在AI for Math这个岛屿上，是一个证明家、一个猜想家、一个知识库，然后这个转化的能力就是贯穿着他们的始终。这是我们认为的这个这个这个科技愿景。然后，其实你就会问一个问题，说这其实不就是翻译嘛？
把英语翻译成这个Lean，但事实上它是不是的？因为比如说，我把英语翻译成法语，英语和法语它们多抽象，其实是很类似的，有多结构性或者多不结构性，多松散。多严谨，它都是很类似的。但是，呃，就是Lean作为一个跟Python更类似的一种一种计算机代码语言，这个转化的过程，尤其由于AI没有见过多少Lean，现在全世界的Lean加起来没有多少的呃tokens，所以这是非常困难的。
转化回去叫 auto informalization，就是就是呃反方向的这个转化，从 Lean 到到英语，这个反而是简单一些，因为这个它见到了很多的英语。但是这个的话比较难的难点就是你如何确定你转化回去的这个数学完全是正确的？你如何就是是就是确定它没有错误？这个我们一般就是让它再转化成 Lean
一遍，就是做这种呃就是转化去转化回来再转化去看一不一样，这个叫 cycle consistency，用这个方法来去来去做。
形式化语言和语言是什么关系啊？形式化语言其实就像是呃，像是比如说 Python、爬虫，然后它它某种程度上你可以把它理解为它有就是执行能力，对吗？它可以就是我可以跑它，然后我跑它完之后，我就会看到一个勾，那个勾就说我这个证明是对的，或者我看到一个报错，就告诉我第几行出了一个问题。呃，如果说在哲学层面上一点的话，其实我觉得，呃，数学作为英语的一个子集。
数学是英语，比比如说数学这些里面的词吧，比如说数学，我表示一个定理，我有这些英语的词汇，它这些词汇所出现的 distribution 概率分布与英语语义里的是不一样的。嗯，比如说在这个代数几何里面有一个词叫做 germ g e r m，这个 germ 在英语里面的意思是细菌。我记得当时特别有意思，在疫情的时候我学这个代数几何。
所以就是大家就开这个 germ 的玩笑，就是这个 germ 它出现的这个概率，呃，分布它一定与英语里面的是不一样的。所以，某种程度上，如果你希望AI在英语里面做数学，这不是一个非常好的，至少它绝对不是事情的全貌。而如果你把这个数学转化为了代码的话，其实我觉得就是它由于刚才我们讲的一些可验证性啊，它其实我觉得更更更更有道理，嗯。
我举一个举一个例子，比如说就是在这个Lean里面，你如果去看它这个怎么一个程序是怎么写出来的，其实还蛮有逻辑性的。它这个它对一些逻辑推理的一些处理还比较好啊。Lean它作为一个就是呃自动化。呃，自动化形式化证明语言，它有一些兄弟姐妹，它又有一些其他的这些语言，比如说 Hoare、Rock、Isabelle，甚至原来更老的一些 SMT、SAT，对吗？
这些都是就是基于逻辑的这些呃，就是证明语言。然后我们现在这个世界上，我们所有的芯片的一些验证，基本上要用Cadence这个公司的Jasper。Jasper是一个基于SMT的一个一个一个语言。然后这Jasper就有很多的局限性，就会有一个很有意思的问题，或者说我们可以头脑风暴：如果全世界的SMT挣扎着的struggle的S SMT全部可以被被另代替。
我们会是一个什么样的世界？然后又另外的一一层问题是，Lean和Python之间的关系是什么样的？其实，我们就回到刚才的那一个点，就是Lean可以去作为去可以作为一些Python程序的验证。其实还是还是挺有挺有挺有意思的。我听下来我会有一个问题，因为现在 coding 也很火，对，那用 math 作为手段和用 coding 作为手段去执行任务的区别会是什么呢？
对，其实这是一个很好的问题。他们某种程度上是互补。就是coding的话，它可以帮我计算出一个output，可以帮我计算出一个输出。然后，呃，数学的话，某种程度上它可以帮我验证一个性质，验证一个property。呃，我比如说你给我一个问题，这个问题我可以拿一个呃编码的这个这个coding去去给你解决，我就给了你一个这电脑程序。
然后呢？但是，然后我就需要去知道这个程序写的对不对，是否解决了你的问题。我现在需要很多输入输出，对吧？这些我的 test cases。如果这些 test cases 都可以不需要了，直接我可以验证，在我写的时候同时验证你的这个电脑程序真正解决了你要的这一个问题，通过 Lean，那我觉得是一个非常非常全新的世界。
但是这里就会出现一个难点，这个难点其实我我喜欢拿正面的事情去讲。呃，我们相信的一件事情就是，任何你能定义的，你都能证明。嗯，任何你能写出的，或者是任何你能specify，specify就是英语里面program specification，任何你能表达的，你都能执行。这是我们对于 coding 未来的一个愿景，就是这个事情的难点在于，比如你告诉我你的这个问题，我无法确定我是否能把它写成一个。
比较严丝合缝的一道，呃，在这个形式化语言里面的这一个这个题，嗯，所以我其实其实这个可能讲的我我我不知道观众，我可能讲的也不是特别好，就是可能再再去orient观众朋友们一点，就是呃，我觉得这个software
verification是如下的一个一个布局，你有一个。啊，program这个program就是你的这个电脑程序，乘以这个specification，specification就是你要达到的这个目的，你的这个目标，映射到verification condition，就是验证条件。
乘以 proof，也就是这个证明。而 action 做的是这个 proof 的这个部分，然后能够就是就是，所以其实但是你你要看就是 program 有对吧？就是我们可以现在很多 AI 可以写很多的这些就是电脑程序，这个 specification 反而变成了难点。verification
condition 这个东西就是做这些形式化语言的这些，他们给我们提供，我们解决 proof，这中间差的就是这个 specification。
任何你能，所以这个这个梦想就是像数学一样。我举一个数学的例子：任何我能写成一个数学问题的问题，都会被证明。嗯，在这个coding里面，就是呃，任何能够定义的。都能够被被执行被做出来，对被执行。如果难点是specification，嗯，他应该怎么解决？哎，这这这就是为什么说，在这个数学里面，这个猜想很难，就是做这个conjecture猜想家这一块很难。
就这就是这其实是难点，定义与猜想是难点。就是定义，比如说我，比如说我们之前有一个很火的叫 First Proof 的一个一个一个一个挑战，对吧？有一些数学家他们跟还上了《纽约时报》，就是讲说，嗯，给 AI 出十道题，这个 OpenAI 做了，好像做了五道，也不知道对不对。然后这个 DeepMind 做了六道，好像是对的。
他们当然都是拿这个自然语言做的。为什么？比如说我们 Action 就没有办法去参加这个挑战呢？因为这十道题，我甚至都没有办法把它转化成 Lean。的这个就题目我我放不到链里面，为什么我题目放不到链里面？题目涉及了很多定义，这些定义完全不在不在这一些就是library不在这个mathlib里面。然后我如果要去定义这些的话，这一步目前机器很难做，所以由于我无法定义，导致我无法证明。
所以这是这是我目前觉得的第一个第一个难点。对，然后在在这个定义之上，当然也就是这个这个这个这个命题，对吧？所以。嗯，我我们还是希望的一个未来是，当然一定是有局限性。比如说，我们知道就是从我们那两道没做出来的题，比如 floating point 这个这个非常难做。这有一些就是计算机程序的这个任务非常难难难去拿我们的这个 Lean 去进行验证。
但现在大家都有尝试去呃各种各样的方法，让就是不能够验证的那一些那一些情况变得越来越少。嗯。嗯，其实我问这个问题是想说，AI for Math 它是一个更垂直领域的一个 AI 的事情，是的，还是说它能够泛化成一种通用的智能？它泛化会泛化的比你这个垂直感受到的效果更慢，也更更不那么戏剧化。我觉得在在在垂直领域上，我觉得你就是是有可能有一个cursor-like moment的。
是你能够感到，就是bang，就是你能有那种感受。然后某种程度上，呃，它和就是通用的智能有一些关系，但在某一些情况下，肯定是某种程度上他们还是在在在战斗的。比如说，我们发现就是数学做得好的AI，这个跟人谈话就听起来非常傻，就是好像。呃，这个这些这些这些这些性能是在互相互相相斥的。但是，比如说从数学到到到到代码生成，从数学到这些就是代码芯片验证，这些很明显是是转转化的。
你说的这个 cursor like moment，它会是一种更产品化的 moment 吗？呃，数学这个它其实某种程度上，我觉得是一个概念。我觉得好的产品其实它是来源于一个比较深的一个概念，就是一九八零年的时候，我们知道一九八零年代Donald
Knuth这一个计算机学家，他提出的是什么事情？他提出的就是，我希望让所有能够，呃，我希望让所有计算机科学家都能够，呃呃，Web Code的整个所有的事情，我能够在像数学家一样，在自然语言里面去做做做推理，然后这个电脑就直接执行。
但不单只是我们现在讲的这个Web Coding，因为我们现在还有Code Review，他希望能够把这一些，呃呃，直接代码直接到这个Deployment，直接可以Ship。然后我们目前可以在前端做，但我们后端做不了整个的这个系统，我们也很难 web code。比如说，我怎么 web code 一个 control flow，我很难去很难去做这件事情。
嗯，这是这是一个一个一个梦想。然后，比如说，你可以猜一猜，第一个提出形式化证明的这个人是谁？其实比这个Donald Knuth还要更早，就是就是艾伦图灵，他就是讲说，我我就是希望我能够一边编程，这个编程完全背后的这个逻辑，不单只是。就是这个逻辑和就是它完全能够与我的这一个呃想解决的问题完美的这个这个这个契合，而不是依赖于有限个呃测试的这个输入输出对儿。
但是我这有限个输入输出对儿，它其实是有它的有它的好处的。你知道它能帮我什么吗？它能够帮我去 specification，它可以帮我去做这个定义。就是我，比如说小俊，你给了我一道一道题，让我去就是去编一个成，比如你让我做一个排序，我把这个排序的题怎么样从一个英语的题转化成一个呃，在我这个Lean里面的这样的一道题。
就是这个过程，由于我还没有去解决出，也没有去证明出这个Lean的这个这个命题，我需要这些输入输出的东西来帮我去做一个验证的信号。嗯嗯，我在想，因为Chrissy他这个moment，他是让很多。不会编程的人也能够做了。那你说的这个math领域的crisis moment是不是会让更多不会做这么高等数学的人也会做数学了呢？
呃，我们可以用它做什么呢？呃，我们可以拿它，比如说我们公司，呃，虽然呃有有一些同学他们以前做过芯片硬件，大部分同学没有做过芯片硬件。呃，我们现在可以去用Lean去呃证明芯片的性质。所以，他还是一个非常专业化的，有一个专专业门槛的人去做这个事情。呃，不是，不是，不是，我们我们公司的就是呃呃，一般的软件工程师可以去拿Lean去去知道一个芯片是对的。
对，我觉得我表达有问题，是我想说的是，它还是一个非常有专业需求的一个事情，对吧？因为这每个人都需要，就可能更多人需要编编程，嗯，但是并不是每个人都需都需要去证明一个芯片的性能。呃，我觉得就是在这些芯片的领域上，由于可能说之前做不到，可能之前的解法是这个SMT这个就是基于SMT的解法做不到，嗯。我我觉得就是在呃，我们比如说每一天，就是更consumer、更更day
to day或者prosumer的这样的这个市场上，可以就是以下的一个想法，就是你一边编程的时候，你一边就是他告诉你整个编程不需要任何test case。
已经完完全解决了这一个 coding 问题，这个我觉得会是有意义的。嗯，我只是觉得在这些芯片这些领域上，它目前就是感觉这个痛点更大。比如说，这个亚马逊在过去的它有一个世界上最好的呃呃自动自动推理 automated reasoning 自动推理团队之一，呃，没有没有 AI 的，就是那个那个纯就是人人，它有很多的这个呃形式化语言的这些专家。
呃，他们花了三到五年去写了呃二十六万行呃定理证明的这个代码，去验证他们的。这个我实在不知道怎么说。一个呃，用于去最适化CPU处理的一个hypervisor，一个工程工程的一个东西，它的一个一个一个component memory记忆。Memory isolation component，我我不太会说这个中文。
他他去确定这个东西写的是对的，他花了三年，人写了二十六万行，这个完全这个这个AI没有改善这些工程师的生活，AI没有改改善那一些必须要手把手教着这个呃这些几千多个license的去验证芯片的这些人的生活。呃，我觉得呃，就是可以在这些领域上，你会有更好的pricing power，你会有更好的，呃，定价格的这个这个这个空间，作为我们这一个呃呃我们的公司这个这个这个提供方，科技提供方。
呃，但是我们觉得就是在更广广泛的每一个人都要coding的这个这个情况下，我们会意识到verify generation的重要性。就你会希望某一天，在我我要一个 call action，要一个函数的时候，他给你是百分之百不需要验证的函数？嗯，对。所以这也算是你们之后可能会探索的商业模式。嗯，我们觉得就是验证是我们最好的第一个市场。
嗯，这个市场会在什么时候打开呀？你预计就什么时候？你是你们。要做商业的时候，呃，我觉得我们，呃，就是我们还是比较坚信说，就是一个是专注，就是说这一些比较呃顶尖的这些科技人才要继续把我们的这个系统的这个能力往前变强。但我们同时又觉得说，可以去开始进行这些小的探索尝试。其实某种程度上，就是你如果就是有更多的资源，然后能够有更多的人在这个团队里，能做的事情就可以越多。
嗯，所以我们其实我们还比较，呃，某种程度上有点好奇心驱动的去想这个商业模式。我们其实还挺好奇这个东西，它能证明哪一些芯片性质、电路性质，它不能够证明哪一些。他能够去呃呃去去证明哪一些程序不能够证明哪一些，我们我们其实更更更关注就是他不能做的这件事情。然后其实我们觉得去解决一个有意义的失败，比很多个肤浅的成功来的更有价值。
嗯，对。有时候在我们讨论大语言模型的时候，我们会说语言是呃模型的一个拐杖，对数学是吗？数学式，然后没有之前大家把数学当语言了，就是把数学当语言来做拐杖，这个我觉得不对。我觉得就是真的是要把数学变成另这个，它就能够成为一个更更更更嗯，就是更另外的这样的一个很重要的一个拐杖。嗯，所以它是独立于语言之外的关数，数学跟语言应该是平行的关系。
嗯，某种程度上是的。我们可以看到，甚至在我们的系统里面，就是更偏呃有一些问题更适合偏语言的解决。比如说，你列出这个提纲就是很大的一个一个一个部分的胜利，那进度条就到了很多。嗯，另外的，比如说适合就纯粹的在这个形式化空间里面去证明。嗯，它肯定是相辅相成的。我们其实觉得挺有意思的一个点是一个就是一个形式化做的很好的一个。
一个一个模型系统啊，它它能够比如说在这个芯片验证上做的比一个更多语言一点的要做的更好，但是在一些其他的比如说这个通用的这个代码生成的这样的一个一个一个情况下，嗯，是我需要我也需要这个就是语言这一块的，因为我需要理解这个用户他可能无法自我表述的很清楚的需求。我们觉得把这个语言的这个部分和这个Lean的这部分放在一块最有意思。
哎，你们是基于大语言模型的吗？我们这个系统里面有不同的模型，这些模型他们一般就是经过了大语言模型之后的后训练。然后是以数学为主，啊，Lean为主，以Lean为主，嗯，就是输出都是Lean，他的目标是输出就是Lean代码，然后Lean代码他自己带了这个程序语言，自己带了这个验证的这个性质。嗯，所以就是这个有意思的点就是，假设我我什么都不懂，密钥学我完全不知道密钥学是什么。
然后你写了一篇密钥学的文章，然后你把这个密钥学的文章，就是呃就是你写的英语的这个文章里面包括一些数学符号，你你打印了，然后你给我看，我我是看不懂，我也不知道你写的对不对。但是呢，你这个密钥学的文章可以通过 Action Prover 把它变成 Lean，然后我不需要看得懂，我只要把它一跑，我看到一个勾，我就知道你这个密钥学的文章是对的。
嗯嗯，这是一个很有意思的点，就是它是一个很好的验证过程。对我们，我们我们接受了，我们盲目的接受了这个非常强大的AI会犯错误，但是我们相信在一些领域上，这些错误将极度的昂贵。我们相信能够去做一个尽量perfect的AI。所以，它能相对于就是在现有的A I之下，它可以帮助解决幻觉的问题吗？它对是帮帮助解决幻觉的问题，解决那所有的幻觉问题，还是只能解决一部分？
会有两种情况：，它要么就说这个事儿太难了，我做不到；，要么他会给你一个正确的东西。所以可能是语言是突破边际的那个，数学是在把它往回收的那个约束。对，其实其某种程度上，这个呃，我其实觉得人类，比如说好的直觉是什么？好的直觉其实就是一个配比，配比其实就是幻觉和这个呃这个呃规律规律推导的这个 pattern matching 和这个呃这个幻觉的一个配比，这个配比要合适。
其实某种程度上，语言能够呃做很好的 conjecture，这个猜想家，我觉得其实跟语言他会有一些很很，他会很需要借助一个很好的语言系统，它可以帮你去突突破这个边界。然后这个某种程度上 generation 就是生成，然后 verification 验证这两个就是一个来回的这样的一个一个一个过程。嗯，对。
但我们又有其他的方式可以去突破边界，并不一定非是要语言模型。比如说，像Francesco Tart和Alberto Averino他们这一个数学发现AI for Math Discovery的这些工作，他们是通过去找有意思的数学物品，呃，物品object数学。数学的东西，嗯，呃，去例子，去去去去尝试，呃，去找到一些直觉，然后去把它变成一个猜想的。
比如说，我有很多很多的图，我可以让它在做一些，就是呃呃呃，local本地和global整个图全图的这些这些这些，嗯，扰扰动，我可以用这些方式去突破边界。然后我甚至比如说另外一些方式做猜想，我可以去，呃，我可以去看一下，嗯，怎么样去做一个，嗯。可以做embedding，然后可以去做呃一些其他的方式，也可以去根据这个语言的这些相似性去，反正有很多东西可以做，但它确实是跟语言更相关，然后而证明是跟。
证明其实跟两者都有关系。嗯，对。你们接下来的一些呃，就是想要达到的目标会是什么样的呀？对，呃，我们现在在还当它成阶梯式对向前推进的时候，我们希望能够我们也解决了一些研究问题，我们解决了交换代数的代数几何的，然后呃。呃，代数数论的，然后还有是，呃，一个比较更离散数学，比如组合概率意味的。我们解决了这些问题，我们希望能够选一些，就是目前Lean没有多少这个定义的这些领域，比如我们希望能够看一下动力系统，我们希望能看一下这种。
嗯，概率和随机曲面，我们希望看一下没有这个基础建设的这一些地方，我们能不能去解决一些问题？我们想知道这个前沿到底在哪里？我们本来不知道，我们大概两两个月，我们就把高中的那个基准级，mini f to f，这个也确实是一个比较。古老也被打的千疮百孔，估计不知道多少人训练在它上面训练的一个基准集，就把它就是饱和了，然后接下来饱和了普特南。
然后接下来就饱和了这个呃呃呃这个这个代码，就是验证了这个这个基准集。然后我们在研究层面上比较缺基准集，说实话，因为没有多少就是研究级数学的这个benchmark题不好找。然后，所以我们只能说找一些未解决的这些问题，在每个领域找那么两三个试一试。现在希望能找一些完全看起来没什么希望的领域，这个可能花的时间会长一些。
我觉得接下来就是就是这个A轮之后，就是我觉得希望嗯。我们可能会更多的往工程、往研究上这里去去转换，可能解决一些光是工程没有办法、不足以就是摘起来的这一些这一些low hanging fruit。嗯，对。数学家的意义是不是在出题上？他要数学家的意义，很大程度很多很大程度，我们的数学家的意义在在出题上。
嗯，对，我觉得他们我因为尤其是你现在机器出题出的不怎么样，刚才讲这个猜想家非常非常糟糕，目前的表现，嗯，所以就是确实需要人出题，但出题非常难。我们现在比如说我们要到哪里去找，比如说八百道就是未解的啊研究研究题呢？你你你一个教授有这个题，你你是给给我们还是给他的这个学生呢？就是。这这是一个非常复杂的一个过程，所以我们呃也是希望能够去通过我们的数学家的网络去大家去看有没有提愿意给这个AI试一试吧。
嗯，你们想把它往哪个方向引导呀？作为初提的这呃，我觉得它一定是要就是满足一个以下的这个性质，就是呃，它一定要就是robust to distribution shift，就是说不管你是哪一个领域的。呃，这个它都能做一点，它不能是一个只做，因为你要是比如说只做欧式几何，那你就是一个几何几何几何引擎，对吧？
但是你你希望它能够做更多的领域，尤其是那一些目前没有基础定义的领域的的数学。比如，我想让这个东西去做一个代数数论，代数数论里面的很多的东西，其实都在这个 Mathlib 这个这个图书馆里面已经这个定义已经搭好了，我只要就是我就很容易的就可以去写出我的命题。如果你连定义都没有，譬如说在这个动力系统，或者说是一些比较高级的组合，它就没有这个定义。
我连这个题写都写不出来，这就是这个 first proof 这十道题的这个挑战，我们很难去甚至尝试的这样的一个问题。嗯，目前这个这个能力，那那你可以说，为什么就像你拿 AI 做猜想，你能不能让 AI 去写定义呢？呃，AI写定义的能力，他们这个这个这个社区管它叫library learning，就是图书馆学习。
图书馆学习能力大概的意思就是说，让这个机器能够去搭出一个图书馆。也就是说，从定义，包括上面的定理，包括上面的去证明这些定理，然后去延伸出新的定理，加更多的定义，这个过程是一个建筑理论的这个过程，这个蛮难的。就是呃，所以说 library learning 是一个大家目前可能卡在卡在这里的一个地方，因为我也不知道这个定义，我首先我很难给它验证性好，我没有办法说这个定义是对还是错，像我一个证明。
对，这是一个一个点。然后另外一个点就是是否是 faithful 的 faithful
的意思就是说是否与我这个人类给出的、人类在数学里面已经创造出来的定义相同的。如果未来这些人类的定义都已经被假设，我们全世界的人类就是无穷猴子定理。无限猴子定理，我们什么都不干了，我们就把人类的数学全部打成这些定义，全部打进了假设，就是上帝给了所有的已经存在的这个定义，做在在Lean里面了，就会出现一个问题，就是当这个。
当这个系统要做新的猜想与新的证明的时候，他会发现我可能引入一些新的定义，能够让我的生活变得更容易。但是在这样的一个情况下，如果那个定义是一个人类没有没有写过的一个定义的话，我怎么样能够保证这个系统的这些定义不相违背？嗯，因为我我我我对吧？我可以定义一个图是好图，然后过了一会儿之后就会发现这个东西可能会呈现一个悖论。
在这样的一个情形下，其实是是比较棘手的。嗯，对，就是这些都是比较，就是呃比较远的的研究问题。但是我们最近我们会在想的事情。如果AI for Math实现了AGI，嗯，你觉得它的标准是什么？它能实现什么？哎，这个Demis他有一个非常Demis Hassabis他有一个非常著名的，就是说你把这个AI训练到一九一一九一零一九一啊，看他能不能就是去发发明发现广义相对论。
呃，这这是一个很有意思的一个定义。首先，我觉得我不太喜欢AGI这个词。我觉得我们可能更是做ASI，就是确实这个我们不能够去声称我们做的数学是general的。数学它并不一定是那么general的，它不一定能带来放。我我是这样想的，就是我我是这样想的，就是在这个盘子，我们当时还真在一个中餐馆。这个这个盘子的外外外缘是，比如说证明黎曼猜想、找出治疗癌症的秘方、呃，这个的方的方法，然后呃，写出一个像莎士比亚一样的，或者说像能够拿诺贝尔文学奖的著作，所有的这些就是人类的超人类的任务，嗯。
就是有一些呃，frontier就是前沿的这些这些实验室，像OpenAI他们，他们想法说，我一点一点的，我要做AGI，AGI什么意思？就是我我一点一点的把这个圆环撑大撑大，最终我到我我我我接触到了所有的这个边界。嗯，我们不是，我们是，我们从这儿然后往这个证明黎曼猜想这儿打，我们就往数学这个代表数学的这一个超人类任务打。
打完了之后，我们觉得他会发散出一个扇形，就是可能说这儿有个代码验证，这儿有个物理，我是发散出一个四扇形，我绝对不会覆盖到这个拿诺贝尔文学奖这里。但是我会有一个比较大的善行，而我这个大的善行，在我这个B to B的这个市场上是有意义的。嗯，这是我们的一个想法，所以我们觉得它是一个ASI。其实人类的智能AGI和ASI，ASI就是。
呃，区别A A I我觉得是specialized superintelligent，OK，对对对，然后H G I就是general，当然S一般大家意思是superintelligent，我觉得我觉得superintelligent就应该是specialized，这是我的一个hot tip，那为什么呀？
听起来还呃，A A S三应该在A G I之上。那比如说我我讲一个例子，比如说就是我可能我数学还可以吧，我我自己都不会做饭洗衣服，就是就是这这是这就是人类的这个智能也也不一定多general。OK，嗯嗯，那有没有可能A G I实现的非常好，他把你这个给取代了？这有可能，那我觉得我会更快。嗯，我觉得就我们现在看到，比如说拿这个强化学习做到这个 coding 上，我们看到了就是 take off。
我们看到，因为你拿强化学习能把 coding 做出来，我觉得 code verification 我们在做的是很重要的一环。所有这些东西做好之后，就是你有这个基于你有既有这个数学去做这些 algorithm 的能力，又有呃，如果把猜想能做出来，你就能够达到一件事情叫做 recursive self improvement。
recursive self improvement 是一个我们包括很多其他人都非常相信的一件事情。我相信这个大家也很熟悉，就是说你就可以持续螺旋上升。就是我希望一个世界就是AI AI scientist，AI AI engineer engineer。对，然后这个过程中，我觉得action一定是其中的一环。
嗯。但他他肯定是，但他不是整个的生态系统，它是其中一环。嗯，所以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。可能未来还会有一个市场是最实化，就是opt呃最最最实化optimization。就是某种程度上，以我们经常讲一个词叫就是 diminishing return，就是说我花了很多的力气，我最后就只有那么一点的收益，所以不值当。
但这个世界其实很多程度上，并是是 diminishing return 的反面，是这种沉默性付出，沉默性。沉默性付出成本的反面是你最后花的，你花了很多很多的力气，你能够带来非常大的最后那一个 mile 会有非常大的一个收益。某种程度上，比如说能够去把所有的 edge case 边缘性情况都都覆盖的搜索引擎，比如说像 Google，它它就会赢得这个搜索的这个市场。
然后比如说像呃呃我们这个呃一些文艺工作者们，他们能够就是好和非常好的这个区别是天差地别的。所以在某种程度上，我觉得，呃，像像像验证一个这种边缘情况，很很耗费很多的钱和人力和很多这些资源，和这种比如说最最直化，我需要目前大家花了很多的的的工业界的资源去探索这个小数点后一千位是什么，比起小数点后第三位是什么。
虽然在一些其他的情境下，小数点第三位比小数点第以前位要有要有意义，但某种程度上，我们既需要呃，我们是需要既需要这个median，又需要这个outlier。数学我觉得给了这样一种一种DNA。我很好奇啊，嗯，你们公司就是有数学家的公司，和你那个竞争对手，他不要数学家的公司，他DNA区别会是什么？呃，我觉得我们公司既要数学家，我们还要一个他们不要的，就我们我们要很多就是代码生成的人，就我们有很多就是编译器代码生成的这些同学。
我们其实我们相信多元产生智能，其实其实有有两句话是，呃，我多元产生智多元产生智能就两句话，我比较相信一个就是呃降维打击，另一个是多元智能，就是嗯，我们觉得就是。这是为什么？我们比如说，你刚才说AI for Math的意义是什么？AI for
Math它其实在探索推理的一些非常难的问题，它某种程度上能够，呃，与其说是泛化，不如说是，比如说你现在有你你有一个吹脸一照的这个这个这个呃字符串的这个这个爬虫爬虫的数据，然后你很明显很难就是。
你你你你你你你基本上通过就是嗯pattern就是就是这个规律的这个找寻能够做很多的事情了，你很难撞墙，你很难碰壁。但如果在数学这一个就是目前lean data非常少的一个情况下，你动不动就能够遇到一些就是拦路虎，所以你你你hit这些roadblock是更快的。所以呃，某种程度上我觉得我们做一个更难的事情，希望能够垂直下来给其他的一些领域，就是某种程度上能够去去去去。
去降维打击。呃，我讲这件事情的原因是，比如说我们现在Actimprove能够生成一个二十页的一个数学证明，对吗？但我然后我可以非常快的去验证一个目前在芯片验证领域是一个比较复杂的一个一个puzzle，因为那一些需要的是一些比较可能说高中数学家，呃，高中数学学生或者初中数学学生会的枚举法、分类讨论，而不是什么like。
呃，我想想啊，不是什么numerical呃numerical like semi
group对，然后嗯，这是这是这是我的一个想法，嗯嗯哦，我刚才说三个，不好意思，我我就说我说忘了一个，就是三个这三。三三个背景的人，他们联联联合起来，其实能有很多想法。比如说AI和这个就是有这种compiler背景的人，他们可以用一些方法去做很多的synthetic data
generation，去做这个呃合成呃不是合成不叫合成数据，就是拿AI去生成这个lean data，而不是靠人去去打这个lean。
因为你想，就是我去找一个数据提供家，比如说McCoreturing这一些。做这个数据商，他们可能就整个平台二十五个专家，然后可能擂台打得不怎么样。那我这个东西是没有办法去大规模的去做的，所以我必须要拿AI去做。那怎么样拿去去做？需要代码生成，我可以用forcing，我可以用repair，我可以用就是failure categorize，我可以有很多很多的方式，是这些人能够给我们的不同的视角。
AI和数学这里当然也有很多，我可以想，就是呃正向推理、反向推理叫 forward and backward conjecturing，我可以去想很多一个数学家如何去呃有点像当时就是早期棋类的 expert system，所有这些东西可以连在一起。我觉得我们是一个 idea rich
的一个公司，就我们有很多很多很好的想法，嗯，然后我们人不够去执行它，我所以我们现在在，我我们十二月份的时候，当时 Ken 加入他是第十五号员工，现在已经三十人了。
嗯，竞争对手当然了，不知道，好像五十到七十五吧，还是比我们大。好的，对，怎么理解数学是现实世界的沙盒？数学是现实世界的沙盒，因为你既有验证的这个信号，又能够有更规律性的描述，更结构性的数据。对某种程度上，我我比如说，我们要在生活里，咱们俩现在来想个猜想，嗯，然后咱们俩再把这个猜想证明。我好像只能想到一个数学猜想和数学证明，不然的话，我们可以说猜想一些生物的东西，然后来一个实验室去做一些动物实验。
这个任何与现实世界更有关的这一些验证的过程，其实可能会比数学的这一个比较简简简简明的这个沙盒要要困难和复杂的多。也就是我为什么非常就是呃 respect 呃我的一些朋友们，他们在做就是 AI for 科学的公司，比如说 Periodic Labs、Lean Feeders，他们在做。然后原来是叫 Future House，现在叫 Edison。
这个 Sam Rodriguez 是我们 MIT 的这个校友，他们在做就是一个一个一个 AI scientist。嗯，很多很多人在做各种各样的这些这一些尝试，但是就是如果你想要很快的一个验证，然后你又希望又能计算又有逻辑，我觉得数学和代码是好的选项。嗯，对。AI for science和AI for math它不是一个overlap的赛道，对吗？
不太是，我们呃，我们能AI for science，他们其实很多在比的是这个iteration circle这个有多快，因为你想，如果他们出现了white lab，出现了实验室。这个我我我身边很多朋友有不同不同样不各种各样的实验室。我的这个呃知道这个Lila这个Lila Science这个公司，Jeff他们还有George Church在的那个公司，他们有个什么Robot实验室机器人实验室。
这个听起来非常的对，非常的非常的非常的自动化，但是他们所需要做的前期的。投入是很多的，Lean Feders他们最近这个实验室又搞起来，又有其他的一些实验室，像Madra、Michelle他们都有很多的这些，他们是一个赛道。我们某种程度上，如果他们有想要我们解解决的一些理论上的一些一些问题，我们希望能够帮他们解决。
但我们某种程度上只停留在一个数字世界，我们不走到他们这个实际世界去。嗯，但是你可以帮助AI for Math，对你也可以帮助大语言模型，就其实你们是一个拐杖，是一个工具。对，对我们我们觉得。呃，也不能算是拐，呃，我们是拐杖和工具。比如说，我们可以去验证他们生成的代码，来帮他们减少幻觉，这个蛮重要的。
我们可以去，我希望的一个世界是，每一个就是物理学家，他们都有能够找到他们的理论物理学家。就是我我我，他们都能够每一个每一个神经呃神经科学，就是做一些真正是动物实验的的人都能够找到他们的呃呃ILF这些理论的这些计算神经科学学家。而这些这些，嗯，过去数学家们他们停留在比如说自己的学术圈子里面，他们可能去呃很很少的一些合作，呃，他们很少去与这些这些应用科学家进行合作。
我觉得未来就是希望能够Axium的AI数学家能够去帮这些AI for science的这一些呃呃科学的这一些探索去解决一些理论上的问题，嗯，然后他们可以去进在实际的生活中去做去做验证。你刚才说了很多AI for Math，它的验证能作为验证的手段。对，那它能有一天像一个天才。如果你走形式化证明，你就有验证；如果你不走形式化证明，就没有验证。
你们现在走的是形式化，我们走形式化。嗯，那如果不走形式化证明，它通往的是哪里呢？不走形式化证明，它可能是我觉得可以去尝试。呃呃，我觉得就是他可以尝试尝试一些怎么样做通用的推理吧。我觉得，呃，AI for Math有可能有一天像一个天才型的数学家一样提出非常好的问题，有非常好的直觉，他能成为那个创造的人吗？
这就是这个最最难做的这个部分，但是我觉得可能我们和那个竞争对手的一个区别是我们打算做这件事儿，他们不太打算。哦，对他们好像直接要落地了。对，他们落地成什么？就是就是他们打算直接做这些商业的这个东西，他们觉得IMO金牌可能就是就是这个终局了，就是可以。就我们还是希望，我们真的能希望把猜想做出来。嗯，这个我觉得我们目前也有很多的一些试验和探索，然后也碰了碰了不少，碰了一鼻子灰。
对，但是我觉得这个碰什么一鼻子灰，就是就是有做不出来的情况。比如说就失败了，你这个失败到底是当时我记得这个失败发生的时候，我们的这个证明家这个还做的不太好，所以我们分不清到底是哪一块出了出了问题。呃，有很多的这些想法都可以去做，但是我觉得我们要做这个猜想之前，希望能够把我刚才说的这个核心科技二，也就是。
把这个转化能够做好，这个 auto formalization，把这个自然语言到 Lean 这个转化，我们希望能做好。我们觉得能做好这个的话，能够有更大的，既是一个能拿更多数据的手段，又本身能够对证明做做一个很好的一个一个帮助，然后我们才会去做这个猜想。嗯，啊，当然，当然，我们现在可能也在做一点儿，但是就没有完全的 run bump。
没有说整个公司打猜想，嗯，对，猜想其实是数学最有魅力的地方，是吗？猜想其实是就比如我作为一个数学的一个一个学者，我我是很难，我很难去提一个好的猜想。然后比如说给到，比如说假设说现在有一个 reading course，有一个本科的一个大一的同学，希望能拿一道题，对吧？作为一个 reading course 最终的一个，我觉得我很难给到这样一个题，就是我觉得需要呃猜想所需要的数学能力是是蛮难的。
所以我们特别高兴，就是 Ken 能够加入我们。其实他是他是非常他是猜想家，他他他是高产的猜想家。他跟拉马努金的关系是什么？呃，我我听说的故事是这样的，就是首先故事一就是他的父亲是呃，当时一群要就是筹钱众筹给拉马努金修这个在印度修这个雕像的数学家之一，他的父亲是一个非常呃。呃，非常非常出名的著著名的一个一个杰出的一个数数学家，也是做数论。
然后，嗯，当时是印度政府说是要给这个拉马努金立一个雕像，但最终没有实现。于是，这个拉马努金的遗孀，这个女士，她就给这个拉马努金的合作者，世界各地数学家写信。于是他们就是一起去做的。然后他还回了信，就是建成这个雕像之后。所以Ken的办公室里现在还有一个他父亲给他的这个这个呃留下来的就是拉马努金呃呃呃的一双写的这一封信。
然后另外的故事二就是当Ken他是一个我印象中当他是一个本科生，他好像是在芝加哥大学。他当时呃，就是也有很多的社团活动，然后可能课业呢也没有特别占住占据他所有的时间，所以他的绩点也不是特别好。然后他好像高中也没有毕业，反正就是呃，是吗？对，反正就他就是一个非常叛逆的一个少年。然后他的父亲就是拿拉马努金的故事勉励他，就任何时候开始也不算晚。
你不需要像你的这些已经上了多少数学课的同学一样，你才能够做数学，你完全可以自己现在去去追赶上来。于是他进入了他的这个数学博士项目之后，就呃非开始非常非常努力，然后就是做了很多非常好的数论研究。对，看的父亲也是前不久，今年年头，去年年底去世了，所以也是非常值得纪念的一个一个数学数学泰斗之一。他的他的兄弟们都非常的都非常的就是，他来自一个数学世家。
他他来自他的他的两个兄弟，一个是著名的小提琴还是中提琴某个提琴提琴家，另外一个原来是呃密歇根大学的校长。对，对他和拉马努金都被认为是那种直觉型的数学家，对不对？我觉得就是拉马努金是更更尖锐的直觉型解题型，然后而Ken我觉得他是擅长他提出猜想的方式是连接很多不同的视角，呃，是一个发散型，但他他不是那种。
嘿，这就是一个公式，这个东西一定是对的哦。那那是拉马努金哦。就所以我在想，如果A I做的是验证的这个事情，是形式化数学，那。他其实训练的是一个更能验证的人，嗯，而像拉马努金这样的天才，他能够被AI训练出来吗？他会不会是两种类型的？这是一个很好的问题。大家说拉马努金为什么就是essential
AI，也就是当时这个呃transformer paper，呃attention is all you all you
need，你需要的只是注意力，这个这个注意力机制，这个篇文章的这个作者叫Ashish，他有一个公司叫Essential，Essential是做啊，pretraining先训练那个公司，他们先训练了一个模型，就叫拉马努金。
人家说拉马努金的那种浑然天成那种直觉，其实是有可能是预训练的产物。所以我们现在您并没有做预预训预训练，我们现在主要做的是后训练。我们有一天可能会做中训练，但我们可能很确实，你说的对，就是拉马努金并不一定是一个能够通过后训练诞生的一个一个一个一个数学家。他是怎么预训练的？他他就是我不知道他不是他好像是有很多他的这个宗教仪式，然后他呃原来是会计，然后他在喜欢电电影里面反正是拍他有时候祈祷的时候能够看到一些数学的这个，其实我觉得对对对，这个这个感觉没有办法。
就不是说我们能够后训练一个AI能够做做到这样的，但是但是拉马努金到了这个剑桥之后，他接触了就是证明，他知道如何写证明了，然后他就使得他的这个数学的这个影响有有更指数级的爆炸，他有更多的呃更多的他想到的直觉，他可以进行证明，然后变成了新的直觉，我们可以训练这个AI去证明，所以说还是会对这个东西有帮助的。
嗯嗯，哎，小野肯是后训练、中训练还是预训练的产物？他有说过这个，这个不知道。我肯定不是预训练的产物，而且你看他的预训练好像不只是数学。对，就我们现在大家的预训练也都是什么都有。目前其实预训练，我觉得能够去往下去就是做的能做很多东西。我觉得预训练有大量的可以基于数据能够去走的研究方向，但是只是某种程度上也也没有大家没有在做。
比如说，你觉得有哪些可能呢？呃，我觉得就是在就是你这个就是其实就是一些数据的一些本，我我知道的就是怎么做的，可能涉及一些其他公司的一些这个这个这个秘密，所以可能不太能讲。但我们也没有去很深的去想先训练的事儿，比如我不做预训练对吧？我们不做，以后也不做。我们我们没目前没有做的打算。为什么不做预训练呢？
太费钱，嗯嗯，然后我们也觉得大部分的Lean的这个东西可以从后训练，甚至是我们会做一些，我可能会做一些pre training。那有一些人可能就把中训练划到这个预训练里面了，对，嗯，对，其实我们确实是认同说是有一些基本的这个能力是需要通过预训练、中训练来来来来来来来提出的。那我能理解你们是一个创业公司，你们要做的是AI for Math。
那那些大厂，OpenAI、DeepMind，包括DeepSeek，对，呃，自己他们为什么要做AI？我听说的就是，比如说Gemini就花了非常非常多的的的想法在这个预训练，在预训练上面。然后他们的这个，甚至说他们的呃，甚至说有些有些公司会希望从Lean Data里面去把，希望能够买Lean Data去做一些一些预训练。
嗯，就我们现在的这些形式化的数据，甚至可以更多的在预训练。他们要去做什么呢？他们为什么要做？他们他们是要做一个垂直的专家，还是要做一个？他们可能他们就是AGI啊，他们是general的。就AI for Math是一部分，AI for
Math并不是每个公司有些公司没有对。对，目前我觉得，比如说Open A I走的是informal这一个，它其实是Kevin Wild他的个人的科学雄心啊，就是要做啊科学发现。
然后，嗯，我好像就是Deep Mind里面有几个队伍同时在竞争做A I for Math，有一个formal的队伍，有一个informal的队伍。嗯，X A
I我不太确定有，然后Anthropic我觉得他们有，但是呃，只是作为。只是作为帮助他们提高推推理推理效效果的，就是说，他比如说，我有一道题吧，一道数学题，他先把它informal变成formal，然后在Lean里面验证完之后再回来提升他的推理分数，但是并没有把这个作为一个一个专注点。
其实我觉得，作为这一个。如果我是这些就是玩家之一的话，并不一定会去做我们现在做的这件事情的原因是，我一样的人才的这种这种高高密度人才的队伍，我可以把他们再继续在代码生成或者说在一些更红海的一些目前竞争咬的比较紧的呃的领域去去去去去做的更深，去把他们的护城河筑起来。然后完全可以，就是和我们或者是我们竞争对手这一些做的还可以的这些创业公司去进行呃去去去成为去去合作。
然后这有点像，比如说 OpenAI 他们就是会在在搜索这一块会 Call Exa 或者是 Call Parallel 这些搜索做的比较好的公司。嗯嗯。所以你们这个行业现在目前是蓝海。并不是蓝海，我觉得这个东西是，嗯，比较难，嗯嗯，比较难，不太像蓝海。其实也大，比如说就像是机器人的foundation
model，一般比如说派和skill的两家，然后我觉得现在就是创业上就是我们和我们竞争对手两家，就是估值也差不多，总共融的也差不多，一个新一点儿，一个就是比我们两年前差不多是这样的一个状态。
嗯，对你来说挑战是什么呀？呃，执行的速度，我们呃，执行的速度与学习的速度，我们现在会有一个。对我个人来说，我执行的越多，我学习时间越少，这是一个非常痛苦的一个过程。就是你，我以前可能说我每一天有多少的时间能够用来阅读，我现在可能少了这一些时间，但我又有又有那么多的事情需要执行，所以某种程度上这是一个呃挣扎。
然后这个挣扎容易就是会呃。呃，我相信就是我们其他的一些呃很好的科技人才，他们有类似的 research 和 engineering ratio 的一些挣扎，就是一些 trade off。我们希望能够执行速度很快，我们也希望探索商业模式的这一些，从一个技术的角度去探索，从技术和好奇心的角度去探索商业模式。
但同时，我们要做的这些事情确实是挺多，然后也也也困难还挺大的，所以我们就是担心这个速度。我这是我觉得最大的一个苦恼，因为我们现在是。我们现在是呃七个月成立七个月的一家公司，我觉得期待也由于这个A轮吧，可能也期待比较大。我们还是希望能够呃还是能够做长期主义的事情。我们有点怕说是一个是怕执行的不够快，另外一个是怕由于要执行的快导致焦虑，导致这些就是方向上出一些战略错误。
嗯，对。对你来说，实现A I for Math的终点更重要，还是说成为一个更成功的商业公司更重要？我觉得，作为一个就是founder来说，你对你的这个员工和早期创业团队，你负有责任，所以这不是一个某种程度上，我觉得这不是一个。这不是一个纯科学项目，就是我们必须要嗯成为一个一个一个一个能比较长的一个一个一个企业一个公司。
但与此同时，我觉得这个公司的DNA就是登月。其实我我非常温舍，对我非常喜欢温舍他们这个名字。天哪，这个名字简直是太好了！这是这个公司的DNA。如果我们就是太去逐利商业化的话，我们会其实是一个平衡。然后，嗯，我们可以看一下我们竞争对手这个公司，他们公司的起源其实是因为，呃，Robinhood的这个呃founder
CEO他可能呃现在还全职在Robinhood，他可能希望有另外的一个让他感到比较呃有激情的生活，有有热情的这样的一个项目，所以他们可能在早期的时候更讲这种科学雄心。
嗯，我们认为是我们认为是科学雄心，然后，但是我们我觉得理想的。现实主义者和现实的理想主义者，两种都是不错的、不错的、不错的这个这个这个落点，但是不能是太远，就不能是。对，有一天你们公司如果创业失败了，你觉得可能会是什么样呢？是因为什么？嗯，呃，我觉得这个事情其实挺有意思的。就这个事情，它的结果一定是极好或极坏。
嗯，就这个公司其实没有一个在中间的一个一个可能性。当然，要么登月成功了，要么登月失败。对，就是登月成功，登月失败。某种程度上，为什么说像Space
X呢？要么火箭发上去了，要么火箭坠毁了。可能坠火箭要坠毁几次才发上去，可能每次都差那么一点。就其实这是为什么？我觉得就是像伊隆马斯克，他他作为一个就是企业家，尤其你看他早期的时候，呃呃，还是一个非常锐意进取的一个值得学习的这样的一个企业家的一个一个模式。
嗯，比如说好几次就是拼死对吗？他的公司也只能两个留一个，但是就是他很坚定的说，both永远是鱼与熊掌都要兼得。这样，比如Redwall在Principle里面也是这样，我自己也是这样的一个一个认同。呃，我觉得这个公司是一个 binary outcome。然后，我觉得如果我们是呃失败了，或者我们很成功，其实都是有可能发生的事情。
对，嗯。如果失败了，你去干嘛？这是一个非常好的问题。我我自己有，我自己有一些个人的雄心。对我看吧，呃，当数学家。呃，我觉得我可能会去希望看一看。我觉得我那一年的神经科学的学习的一个呃心得就是，我们基本不理解人脑，我们完全不理解人脑。我可能会希望做一些跟人脑相关的事情。啊，不不是跟人脑，就是跟跟神经科学相关的事情，可能是动物脑。
就是我可能会，我可能会希望看一下这些。嗯，我觉得就是呃，brain and machine interface的这个vision，目前的implementation都不太足够。就是人机交互的这个目前的选项，我觉得太太不理想了。嗯嗯，你今天怎么看待硅谷这些模型公司的竞争啊？不管是这些大的模型公司，还是这些New Lab，我我前几天还在跟一个就是呃我的一个XI的朋友在讲，就是。
其实，为什么说呃，为什么说我最后不想去做一个呃，就是金融或者说是一个量化交易员呢？你会出现一个问题，就是你的。啊，你的你的赢与输是一个短期内能够决定的一件事情。我觉得这个事情是，就像Peter就讲的，就是垄了哇。这个我是个比较激进，垄断导致创新，竞争导致平庸。嗯，这种竞争会导致平庸，会导致没有一些长有一些很有长远想法的人，他就要自己出来做做New Line。
这就这其实这New Lab的产生，就是因为好奇心与创造力是我们人类的基本需求。这就是因为可能说是在一些呃前沿的一些呃大的公司里面，无法去做这一些满足他的burning passion的事情，他就要出来，然后。我觉得可能是一个很有意思的点，就是刚才说到这个好奇心为什么是人类的基本的需求。可以，我们可以假设一件事情，就是Action Pure非常的成功，呃，或者说是我们竞争对手的这个他们的非常成功。
反正就我们中有一有一方非常成功，然后呃，所有的数学题，你给我一个千禧年问题，我这个AI就把它全部解决了。这个时候还会有数学家吗？这是一个这是一个非常值得去思考的一件事情。我答案就一定会有，就是你给我一个一百万行Lean代码的一个，我一定要去看里面是怎么做出来的。你你不让我去看，我都会去看。这就是人类的这个好奇心的体验体现。
由于这个证明最后被产生的方式，这些去看懂了他的数学家们又会有新的猜想、新的想法。这就是整个这个发明发现的这一个这一个循环，其实就是。就是，然后就是AI做了，可能AI做了这个发现，让数学家更好的发明，然后，然后这种好奇心和这种探索的这种愿望、意念，是一个我觉得人类无法被压制住的一件事情。所以说，不管是现在是呃呃one
hundred million一亿美元的大包，也无法去压制住这些青年研究者的这个这个好奇心，所以他们就会。
呃，去做出来，我们看到做出来多么多么有意思的东西，比如说 Stefano Arman 他们做了这个 diffusion model 更快更好的这个推理模型，我们可以看到就是，嗯。比如说，就是periodic，我们第一次把这些顶尖的这些AI人才，就是去在一个就是现实世界，他们要做这个materials science，这是一个非常有意思的一个一个一个方向。
他们不怕这些messy的这些data，然后他们其实呃，就是然后比如说我们看到有recursive，他要做AI与这个这个硬件之间的这个AI提升硬件，硬件提提升AI。这这是非常有意思的一些方向，我觉得，嗯，这其实是一个，这背后是一个基本作用力，这个基本作用力就是人类的好奇心。然后，我觉得可能最有意思的点就是，有些人说现在是一个泡沫吗？
还是说现在是登月？就是。你有一些公司，它成了，它就登月了；然后有一些公司登月了，人家真的试了，很努力，大家真的是每一天九九六一块去朝那个梦想努力，结果没成，那就是泡沫。其实我觉得，就是我特别希望的一个一个环境，有点像我我也知道说有一些好的学府的一个环境，就是不怕失败。MIT有一门课就是Learning to Fail，你如何更好的失败？
就是，但当然，这个每一个这种登月项目的失败，它都会在资本市场上会掀起涟漪，对吗？我们会从这个就是私有市场一直到这个公公开的这个市场，会有会有连锁的反应。你有你有可能说这是非常不负责任的，就是为什么这个呃一些可能说 pension fund 一些大家的退休资金，最终通过好几层的投资到了这个私有市场，去给这一些有想法的研究者去满足他们的好奇心呢？
这这是一个这是一个很我觉得很公平的一个问题。但是，就是如果说这一些好的有想法的研究者，不是由于他们自己的这种虚荣心，或者说是我自己要占山为王，不是由于 ego 而驱动的，而是由于使命而驱动的，所以导致他们不是碎片化的，好几个，比如同样的一个问题吧，就是八个尝试，他们真的就是在一块了，他们从不同的背景、不同的技能、不同的这种。
不同的对于这同一个理想的解读聚起来了，去炒这个东西，我觉得这就是一个比较比较legit的、比较比较靠谱的一个。尝试，我能理解这一波的New Lab，嗯，他们都有different的信仰，也有不一样的facts，对，那。呃，当有一天他需要跟这些大的 frontier lab 竞争的时候，怎么应对这个竞争呢？
刚才我们说了。你们A I for Math之间的竞争，对吧？对。那当你要遇到Open I，你的竞争对手是Deep Mind的时候，你怎么竞争？对。呃，我觉得这是一个非常好的问题。我觉得首先第一个就是会有一些结构性的问题，会导致呃，如果说他们需要呃一个单位的创新是需要有多少单位的资源的，而这个比例的话，在一个早期的创业公司是非常高效率的，这是第一点。
我觉得我们公司就是在做的一些事情，我觉得可能在另外的一个环境会更难的去达成，也就是为什么许多人从脸书来到了我们这个公司的原因。然后，呃，这是一个点。然后第二个点就是，其实吧，你作为一个underdog这个黑马，你好像除了这个效率之外，还有这个人才这个之外。人才是人才密度，因为毕竟他们会有更多的人才，你没有什么资源能够和这些大的这些玩家抗衡。
但同时，这更有意思的一件事情上是，OpenAI曾经也是对着Google的那匹黑马，它也是那个就是在Google要把Ilya就是最后Counter Offer抢走的时候焦头烂额不知道怎么办的，也是那个曾经一度发不出工资的这样的一个一个小玩家。所以这其实是一个很有意思的一个点，就是我觉得历史的钟摆来回摆动，它。
就是大家大家螺旋上升，但是又有很很local的这种扰动，某种程度上是有。There is always a way。就这这个这这个东西，我没有办法证明。There is always a way，就是你你得信，嗯，对。然后信的可能就是喜欢加入早期创业公司的这一批人，譬如说 Humans and
这个公司最近融了很大的，呃，他们的这个 co-founder 是 Google 的第七号员工，嗯嗯，他到了现在的这样的一个人生阶段，仍然认为好奇心是他就是所拥有的最珍贵的东西，嗯。
值得他倾家荡产。嗯，你这么说，我能理解。嗯，很多，包括我去跟赛宁聊，他们其实有different，但他们甚至是一个anti硅谷的，收收集了一波anti硅谷的这个派别，他们也非常反感这种剧烈的红海竞争，然后觉得也阉割了对研究员的创造性。对，嗯，其实是我是这样想的，就是嗯。可可以可以，就是就是在一段，在所有的这些就是local的扰动之后，你看到的整个的这个呃宏观的这个局面是什么样的？
一个竞争的结果就是能力在飞速的上涨，另外的一个结果就是嗯好的且快速，不只是好的，好的且能快速验证是好的的东西被。就是被做到最 scale up 的一个状态，但是完全有一些可能可以时间长一点的东西没有被实现，这是一个机会成本。对，但所以说竞争它也不能说不好，它就是确实它这个让我们人人类在这个AI的这个进步，在非常短的时间内达到了一个一个非常高的一个一个一个进步速度。
嗯嗯，你刚才会说到你的自己的自我奖励机制，从从团队里面获取这种能量，变成了从事情中获得能量。现在呢，你是从事情中还是从团队中？现在现在我是从事情中，呃。现在的我是从事情中，然后但是我觉得团队是一个很好的一种，他会给你一种安全感，他会给你一种就是你有一个你有一个你有一个你有一个能落地，你你的脚还在地上，他让你觉得grounded。
但是你事实上能够让你。就是break out的那种那种冲动的那种能量，有可能是愤怒，有可能是有可能是悲伤，有可能是就这种卯着一口劲儿，我就要去达到一个一个让我们这个队伍达到一个什么样的一个一个力一个一个目标的这种的这个能量，它不由团队中来，它由事情的本身来。嗯，对，那个让你最burning的是对终点是什么？
我觉得就是呃，这个事情就讲起来就是有一个莱布尼茨，他有一个想法，它叫做universal representation theory，就是说所有你能够表示的，哇，这句话听起来很怪，所有所有所有大部分你觉得能表示的东西，你都能表示。就是我觉得我目前非常期待一个。让推理能力成为最顶尖的推理能力，成为一个默认状态的一个这样的一个一个情况。
然后，且是能够自我验证的推理能力。嗯，这是我目前个人的一个一个理想。嗯，对。然后，其实就是有些时候，就可能说，人人人一辈子他能剩下什么？有一些数学家，他一辈子解决了一个非常困难的问题，他被这个问题就人人们因为这个问题记住他，他可能这个墓碑上就写着他解决了这个问题。这一个人一生这一个问题，你你想这个高伽罗瓦二十一岁他就觉得就就挂了，然后呃拉马努金他是因为这个营养不良，还有各种各样的身体疾病，也早也三十几岁就挂了。
就人人类要多少人出一个伽罗瓦，多少人出一个拉马努金？然后你如果说是能够去用AI去复现这样的一种数学家。然后你又有那么多已经存在的数学家能够与他互动，然后去有新的这个这个这个就是呃Jevons Paradox对吧？就是就是Jevons我也不知道中文怎么说，他的意思就是说，当你把一个呃一个工具变得能够你做出来让它更便利、更普遍的时候，就会有更多的用处。
比如说，我最近我们公司好久就是第一次找了一个找了一个能够帮我去处理一些呃每一天就是杂事的这样的一个一个一个一个同事。他来了之后，我们就是一块做的杂事反而变得更多了。就是这其实就是Jobs Paradox，就是这些科学家、这些物理的、生物的、化学的，他们能够与这个AI。伽洛瓦，或者说是所有的这些数学家总和，他们能够有多少的科学的理论能够被被被被被发明发现？
就数学家们和这些AI数学家能有多少数学的，就是基础数学的这东西被发明发现？这其实我觉得，这是我的一个一个。你想从算盘到会计师，就是当时是呃商商务贸易，从这个微积分到这个物理各种各样什么力学，然后是thermodynamics，就是然后呃然后到到到工业革命，对吧？然后从这个。嗯，就当时一个叫
Babage 查理斯巴巴布巴巴巴贝奇，他这个能够去算这个 log 对数算得更快的一个 Babage Engine，这是电脑的前身。
嗯，当时叫哈代写我作为一个数学呃数是一个数学家的道歉，这个呃 mathematician's apology 好像不是这么翻译，一个数学家的独白。嗯，他就说我这个东西反正也没有任何的实际价值，后面就有。就密码学就有，对吗？我们看Victor Miller，他是一个呃呃，他也是Shubo当时的同事，也跟Axion很多的互动。
这个呃，椭圆曲线基基于椭圆曲线的密密密码学、密码学的就是就是泰斗之一的这样的一个人物，他是一个纯数学的一个背景。然后就是在在C S看了一眼，然后就看出来了这样的一个一个理论。这对于很多就是纯计算机的这些同学们有非常大的一个价值。这这这是终局，对。但是有有些人说，这个终局之后怎么办呢？这个就不知道。终局之后，我觉得还是要，我觉得其实就是钟摆的摆动又会卡。
但我觉得AI for Math没有像AI模型被scale up一样被scale
up，而我们希望能做这样的一个人，这样我们能知道天花板在哪，我们可能又能回到research，然后又能这样，就是钟摆的来回摆动，嗯。我见过很多的七零后、八零后和九零后的CEO，嗯，你应该是第一个零零后的CEO，是吗？我不想就是画这种代际，但是我还是很好奇，就是一个零零后，而且是女生，嗯的公司会和之前的这些公司或者是就有任何的不一样吗？
你觉得特点会是什么呢？我我这个对我这个其实是非常好好的一个，因为我自己最快乐的一个状态，绝对不是CEO的状态。我自己最快乐的状态，就是我能够当一个research scientist enter。为什么是inter呢？就是这个我说的话，如果比较愚蠢，这个大家认为是是是正常的。我这是我最最快乐的一个状态。
我是真的想做这件事儿。然后我如果能够有另外的一个很明显我可以加入的一个一个地方，我就会去加入它，而不会把这个事情单独做起来。所以，我这是我的一个舒适的一个状态。嗯，所以我。我不太因为事情本身而创业，而并不是说你想当一个创业者而创业。我我特别不想当一个创业，嗯，这个能理解。对对，我反正就是，所以我不太CEO，这个可能大部分对。
所以就但但也有时候有一次闹一个笑话，就是我有一天特别就是想做这个呃benchmark，我想做一个就是。好，我我不是说嘛，那个基准级就是到博士级别就很难搞。我当时就把我们办公室有那个数学背景的同学们，我就是说，哎，我想搞这么一个东西，我也不知道就是现在搞这个是不是优先序上是对的。你们都是搞数学的，你们要不跟我一块儿，我们分一下，就是你负责这个领域，你负责这个领域，每人找个二三十题。
然后完了之后，我们这个之后，我就后面就被我们那个一个比较元老的工程师就说了，说你你让这些这个实习生的同学们，就是还有这些比较年轻的工程师，觉得这是一个非常重要的一个任务，这和优先序是。是相斥的。我说为什么是重要的任务呢？我说这不就是一个side、一个hobby的一个project吗？他们说，但是你是一个CEO，所以你跟他们讲的时候，他们就会觉得这是一个正儿八经的一件事儿。
我真的要去把这个当做我的前几件事情去做。从那以后，我就我就更hands off了。所以，就是这是一个非常非常有意思的一个一个一个事情。嗯，还有什么不同吗？你觉得可能和呃，我觉得就是呃呃，我觉得我我觉得我做这个CEO的一个好处就是。这是一个呃，technocrats
rule的一个公司，就是我们的技术人员，他们是整个公司的主干且且和丁香和锚点，就是他们有可能由于我并没有一些strongly held beliefs。
所以导致我觉得我们就是很多 ideas 都可以被，由于我没有一个特别我自己，我其实我有，我有一些特别坚信的方向，但是很多其他的一些就是很 low level 的一些东西，啊，就是一个 bottoms up 的 culture。所以我觉得这个公司的文化是一个是一个比较比较有意思的一个，就像一个呃比较呃 Pixar 梦工厂。
对你们公司的会议室好像都是用数学家来命名的，有什么有特别的？就就，如果你想，如果这个梦工厂这个或者迪士尼的这一个C E O是一个已经假设O K一个梦工厂的C E O已经是一个就是拍过多少个这个好好莱坞或者迪士尼的一个导演的这样的一个人做C E O，这个地方就成为不了梦工厂，为什么？因为他们会觉得这个人是对的，应该听他的。
所以我觉得，反而是这种bottoms up的这种这种culture对创新来说是最好的。需要一个intern，对我觉得intern挺好的。我非常愿意给Action当intern。嗯，你们的会议室有任何有意思的吗？有，对，就不同的名字，他们就是叫做高斯，对吧？高斯、庞加莱、希尔伯特、Loveless，还有啊，图图灵。
这个中中间大家差点打起来，因为怎么命名啊？为什么差点打起来？就大家喜欢的数学家不一样。嗯，大家说你你有了你有了这个你有了图灵，你没有Church，哎，这个不行。然后你有了这个Loveless，你没有Noether，不行。就是反正我们还接受到世界各地的邮件，说为什么不把Emily Noether作为一个一个会议室？
我们说我们不好意思，我们目前只有五个会议室。后来是怎么选择的取舍的？呃，好像是先就是。我也不知道最后是怎么取舍。大家反正就是还是在Slack里面经过激烈的争辩，大家认为庞加莱、希尔伯特、高斯这些都是poly math，他们在数学里面不只会一个领域，他们会好多好多领域。所以，所以拉马努金就是这么落选的，他只会数论。
呃，所以，所以说就是大家要找这种，就是我们觉得要是做一个AI数学家，希望他什么领域都会，没有distribution。Shift这样的一个问题，所以要找这些Polymath。图图灵是跨世纪的啊，当然这个Shugo他也lie his body on the table，说如果你不给其中一个叫图灵，我就走了。
我说行行行，那就是图灵。然后完了之后，我们希望能够有有有一个女数学家。然后这个女数学家，我们觉得Loveless其实就是在Village Engine这里也也不错，嗯。这其中有你的偶像吗？我的偶像是高斯，他嗯他在也对对他在对对。然后庞加莱其实庞加莱和François Arton他们家里是是就是法他们都是法国人，然后他们家里那个族谱还是连接。
为什么高斯是你的偶像？为什么高斯是我偶像？就是他是就是解题里面的天才，对吗？他这种他这些故事，什么正十七呃尺规画图、正十七边形，然后包括就是我喜欢数论，然后高斯在数论里面的这个都是非常基本的方，就是fundamental的一些贡献啊。高斯比如二次互反律，然后。各各种各样，反正高斯在初等数论，他是他有点像是我学数论刚开始的时候，初等数论里面就好多高斯，所以然后又他又是一个年轻数学小王子，然后反正就整个我我还是挺喜欢高斯的，对。
如果可以穿越时空和历史上的任何一个数学家共进晚餐，你希望选择谁？你想问他什么问题啊？我觉得就是去跟 Erdos 共进晚餐的话，他给你讲的那些描述，毕竟是组合学，你晚餐这个就是 table 上能听懂。然后 Erdos 是有又是那么一个就是 peculiar 非常古怪的一个一个有趣有趣呃有趣又古怪的一个性格，古灵精怪的。
我觉得跟 Erdos 会共进晚餐会比较有意思。嗯，另外一个我觉得。我觉得跟Grothendieck共进晚餐的话，如果不是我的话，就是说另外一个人他跟Grothendieck共进晚餐应该意义会很大，因为但是我这个代数几何学的不是特别好，所以就是跟Grothendieck就容易浪费这个宝贵的机会。嗯嗯。
你看，你当你说到这些数学家的时候，他们都是这么有趣的人。对，那如果有一天AI for Math能做到所有数学家能做的事情，会不会是一件很无聊的事情？我有想过这个点，我觉得我其实我一开始觉得是一个非常就是呃非常非常。我当时觉得是可能会是一个，我不希望让这个局面是一个非常遗憾的局面，因为就是呃，是可以说数学家们他们之间的这种。
友谊，他们的合作的这个关系，他们的文化社区是一个非常有意思的一个一个文化。就是比如说，有一个数学家生日，大家会给他办一个生日的一个峰会，然后所有他的学生、他的合作者们去轮流去。去去讲一个呃，这个人所做出来的数学的贡献，或者是一个跟他们合作的一篇一篇文章。我曾经就是作为一个呃呃硕士生，在这个牛津去过这个啊。
Heisbrow Roger Heisbrow的生日峰会，然后像Ben Green、James
Maynard他们都在那里，然后当时就觉得是非常的感动，就是这是一个非常好的一个一种传统，然后所以这人的这一个元素，我觉得在数学中它永远不会被磨灭。我觉得AI会把就是数学的很多嗯证明可能能够帮帮数学家们去很快速的解决，但是这个猜想，然后以及直觉以及构造以及嗯这些方面，我觉得数学家们仍然会呃有非常多的乐趣，然后他他仍然是会他们会成为智力的灯塔，嗯对。
所以，我们刚才说的那个，当然这个也不一定我们能解决。这个当然是，有的时候你做做梦想着自己能能把它解决了，会不会反而是一个呃不太好的一个一个一个一个一个一个添加？因为比如说这一些数学家们非常珍贵的这一些legacy，他们的他们的他们的对对，但是呃后来觉得哎。他们他们就是会有更多的问题，他们会难倒AI，像他们已经在难倒AI一样做基准级，他们他们会永远永远是智力上的挑战，以及大家这种互动应该会很有意思。
就我们刚才说的那个问题，拉马努金和。做一个验证的AI，对他其实还是偏这边，对吧？偏验证，偏他并不是那个天才型的选手。对这个，我觉得直觉就太难做了。我觉得直直觉可能五到十年。有可能对，但是我有一个很，我有一个比较又有一个比较激进的一个一个想法，就是我觉得大家现在如果看有多少解析数论里面的问题是被一遍又一遍的在一包很标准的证明方法里面去抽抽抽这个证明牌儿，就是就就一一个牌一个卡牌一个一个卡牌一个卡牌。
就这么重复的、熟练的去运用，比如说，我看这个啊，major arc、minor arc、Hardy-Littlewood圆法。这个这个circle method就能解决一些一些呃一些就是bounding的，就是上线下限这些这些方式解决一些呃一些概率法解决一些，然后比如说你去上sieve theory sieve筛法又能解决一些筛法也在被就是有一些人他们不解决任何问题，在提升筛法能做的。
筛法作为一个工具，我觉得就是已经能有的这一些工具能解决很多很多的问题。然后我们会说一个人直觉很好，可能是他很快的能够想到怎么样去重复的。我们现在讲的这种直觉，我可能讲的是说说给大家一个完全不同的一种一种一种一种方法和机制。这个我觉得是五到十年。嗯，你有过一个说法，就是说热爱数学就是看到了上帝的面容。
为什么会说这句话呀？啊？我是这么觉得的，就是我很小的时候就觉得说有一些呃有一些基本的这些这些真理，然后我觉得数学家科学家他们存在的这个呃意义之一，当然就是去把这一些东西进行发现和探索。嗯，其实我我这是我十六岁我曾经写过一篇文章，我当时是这么至少是这么想的。然后后面就是林要开这个，就是创立这个Action的时候，就是不是说老跑步嘛？
早上斯坦福他有一个那个就是教堂叫Memorial Church。这是就是纪念教堂。然后，如果你去从那个就是我们 Palo Alto 这边往那儿跑，然后如果平常我都绕着跑，因为就是特别晒。那一天就是往这个草坪底下去跑，然后就是突然我就在那个教堂的下面了。然后当时那个阳光也特别好，然后那个教堂上有壁画，有天使、十字架。
其实有那么一点spiritual的一种感觉，一点灵魂的这个感觉，就是觉得可能说，如果那个就是一个人的这个墓志碑上，可能印了一个他曾经证明出来的这个事情是他的智力遗产，那么如果能够让这个东西乘以。一亿，你会不做吗？可能不会，所以当时有这么一个想法。当然，这个我觉得也自己就这是一个出于ego的一个想法，就是说我我可能说想我这个公司能够去作为这样的一个AI
for Math的一个unlock，这个想就是我希望登月，也希望登月的是我们，这个肯定是出自于一点这种这种ego或者是就是的自私的雄心壮志。
但是总体上，这个事情我是非常希望它会它会实现的。对，就算我们是失败了，可能要谁其他人登上去了也是一件好事。嗯嗯，虽然你现在还很小，问你这个问题好像不太好，但是还是想问，你希望你的墓志碑上写的是什么呢？哎呀，你是希望你是一个数学家还是一个？就别写，就是。其实我是一个比较就是觉得体验比较重要的人，就是我反正要活过了，我也有体验，这个就无所谓。
我都不知道我要有什么墓志碑，不重要，那就不重要。对，你会希望你自己是一个数学家吗？呃，也不重要，不重要。我觉得我我曾经是觉得很重要的，这是这是这是这是我曾经觉得就是我一想到我可能我就没有办法成为一个数学家，我有时候一开始我有时候还哭，就是我我还是一个比较比较比较 emotional，有时候会有这种。
最近创业的时候是吧？对对对，那个时候是是这么觉得啊。然后后来觉得其实就是我想当学徒，对我其实哎对，其实就是你要非写一个什么就写学徒，就是我想去呃在尽量多的一些智力领域上能尽量多的去学一些东西，比如说这为什么你看我跳来跳去就是数学，然后跳物理，为什么又跳物理？因为我高中初中物理可差呢，我想着怎么着学一下吧，然后嗯。
去去学点神经科学，也学的生物那一块学的不怎么样，但是我觉得哎跳这个计算神经科学学的挺有意思，然后AI挺有意思，然后学学这个量化交易前沿在XTX真的是很感谢那段经历，然后又去学学法律，然后法律喜欢各种各样的像从反垄断，by the way反反垄断是一个非常就是。Antitrust是一个非常就是像树状的一个逻辑的一个一个非常非常像数学的一个学科，合同法也是。
然后又有那种完全不像数学的，比如宪法，就是。哎，宪法其实这个这个，或者说是这种民事诉讼这一些，就是庭审这个最初级的庭审，这些都是讲故事的一些一些这个这个这个领域。然后呢，嗯，就是所以，我还是希望能去学很多的东西。就我觉得AI for
Math其实对我来说，我人生最快乐的时候是我拿到那个我找到那个GitHub的那个link，然后我把这里面的那个文章的abstract全读过一遍，那是我人生最快乐的几个月。
然后那个时候最快乐的几个月，那个时候舒博就跟我一块儿在读，然后现在跟舒博一起做。然后当时最快乐几个月，那些作者他们陆续加入了Action。我们现在有，如果你说前三十篇AI for Math的文章，我们就是大部分都是作者都在我们的Action这里，所以又他们就是每一天和你就是一块儿去去去冲这些目标的战友，又觉得非常的快乐。
其实我觉得就是这这可能是不错的一个一个定律。你现在是什么的学徒？我现在是怎么能够让一个呃一般来说创业公司都会死掉，怎么样不死的一个学徒，一个创业者的学徒，一一个一个呃创业者这个词听起来太好了，就是就是创业公司百分之九十九他都会死掉，所以就是怎么我现在是呃就是 don't die 这个 Brian
Johnson 有一个好玩的 don't die movement，我现在是 don't die 的学徒。
你看，你的第一个自我奖励的方式是通过人来获得的，第二个是通过事情来获得的。你说你今像今天钟白已经到了事情这一边，对，但是人能给你提供一个安全垫，让你觉得grounded，对。那有一天，你作为CEO，嗯，当这两个事情发生冲突了，对，冲突过呀。这个这个冲突过，我们也开，我们也那个也开过实习生，对，就是我们我们我们也冲突过，但就是，嗯。
这个事情，我觉得就是你任何的乐观主义收起来，你要谨慎的做决定，你要想很久，就是因为毕竟是要对，呃，就是可能人就是要负责。然后，但是同同时，我有另外一边，就是很多时候你觉得为什么要想很久，是很多时候你觉得人与事冲突了的时候，其实是你自己不够好。就是你可能这个人可能都跟你关系很远，但是你总是有一些由于你自己技能点和能力的问题，是能够让这两个事情不发生冲突的。
就是他到走到冲突的那一刻，一定是因为你自己本身曾经有做过一些错误的决定。就算这个人可能是一个你不认识的，如果公司很大，这是不认识的员工，他一定是有一些管理层的一个决策，他一步一步的尽头 trickle down 到出现了这样的一个问题。嗯，所以，我我还是比较相信一个词叫 authorship，就是
authorship，就是作者，就是你是你自己人生篇章的书写者和作者，所以你你不能够有嗯，觉得是呃，可能不能够觉得说，就是一个情境它就能够决定你的一个决定，是你决定让这个情境决定你的决定的，所以你也可以决定用其他一些方法去使这个情境不要这么走，我是这么想，嗯。
那我们最后还有一些小问题哈，嗯，我们会让每个呃嘉宾给我们观众呃推荐一本人生之书，你会推荐哪一本？它要真的对你人生产生过很重要的影响，不能是数学书。你也可以说是数学。呃，我数学书的话，我如果是年龄年龄比较小的观众，我我推荐《数初等数论》，里面对数论讲的真的是很好。如果是呃数学书，其他数学书，我觉得呃Devanpur的那本分析数论我觉得很好。
然后，呃，对我还是比较喜欢数论。如果不是数学书的话。我是那个，我挺喜欢《红楼梦》的，就是我确实是挺喜欢《红楼梦》的，甚至是《红楼梦》很多学者他们去研究《红楼梦》，这个是一个曾经在我小时候对我比较有震动的一本书。然后刚才也讲到大阿宝互动奖二号，对我人生产生影响比较大的，其实有呃呃挺多关于一些企业家的一些故事，比如说呃伊隆马斯克的故事，就是。
说还是他之前的一个人太太，他讲的是，他晚上睡不着，翻来覆去，然后就痛苦的。咆叫马斯克，痛苦的咆叫，然后包括说是一些其他的，说是。黄仁勋说：“嗯，就是 pain and suffering，这这些东西，我觉得就是由于就是可能看到过他们的这一些故事，会让你有些时候比较难的一些感觉，像嚼玻璃的日子里面，会觉得，哎，这就是一个正常的一件事情。
你觉得现在训AI跟你当年训自己有什么不一样？这是一个很好的问题。”对我，我觉得有时候你会觉得有点像，啊，比如说就是看到他这个表现刚刚好了一点，马上给他更难的题，这种 curriculum sampling，对吧？这这是一个很有意思的一个事情。比如说，呃，让他能够去，嗯，给他给他哦，比如说看到他做
brute force 的时候，又觉得是跟跟跟自己曾经的那个数学家的那个那个感受有点像，呃，没有说特别。
应应该有区别，但我目前没有特别能够想得起来的点。就是你感感觉你看到相似的时候，你就会特别有这个，你的大脑里的神经元就在fire。对，假设axiom的AI在未来证明某个重大的猜想，但在证明过程中使用了一个新的公理，这个公理不是现有数学的一部分，但是看起来非常的合理，你会接受这个证明吗？能想想象到所有的数学家们就是感觉就是世界末日了一个一个思想思想实验。
呃，我们看到了AI在尝试用各种各样奇怪的公理去帮他作弊，这个事情已经发生了，对吗？就是我刚才讲的，其实这个事情，呃，DeepSeek还为此受害。他当时说DeepSeek Prover，我忘了是哪一个version，说做出来了Pentagon上的当时六百多道Pentagon上的题，就是SOTA在很在个位数。
然后那个 DeepSeek 说我们做出来了四十九道，事实上只做出来四十七道，有两道题其实就是这个这个呃呃 AI 在在在在作弊，呃，我觉得如果这个公理大家觉得是自然的，大家就会接受它。但是这个事情，我觉得就可能是一个大家以前没有探索的很足够的数学领域。不然的话，你可能会认为存在即合理，或者不存在即不合理。
这个公理可能已经被被假设了，它可能是到了一个有点像我们看代数几何混这个组合，除了均贺的这个代数组合学。这个我们可能未来有一个，我瞎说啊，probabilistic analytic，呃，这个这个真的是瞎说。可能我们未来有一些就是混的混了好几个领域的这样的一个东西，大家再往里面加东西。我觉得就是是可以按照接受和不接受两个世界照样去运作的。
当然，你这个 branching factor 现在是二，你如果继续这样，你就会有无限多个世界，然后就会一团混乱。然后有一天，大家可能就会说回收，我们把它 tighten。但这个其实是数学某种程度上是一个是一个人类文明的一些构造，所以我觉得大家是可以的。就比起比如说物理，你要加一个什么定律，这个可能大家会觉得其实还就更不可接受一些。
其实这挺有趣的。嗯，刚才我们其实也谈到了 DeepSeek，嗯，你会怎么看中国 AI 现在的发展呀？嗯，包括 DeepSeek，包括自己，包括 Kimi、MiniMax 等等公司，你觉得在未来的 AI 宇宙里，中美会是什么样的关系和角色？我很 respect 就是这些中国的这个 AI 游玩家，就是比如说，呃，我我很我很诚实的说，我觉得就是豆包 Seed 他们做 AI 方面做的非常的好。
非常的好，然后他们也是非常短的时间，非常执行力强的一个团队。跟他们的一些同学，比如说袁正，跟他们聊过，就是非常好的一个团队。我觉得就是他们，然后他们可能会呃选择或者选择不发发一些文章。然后我觉得就是这些 ideas 可以就是流通，还是挺挺好的。嗯，对。但是当然，大家可能最核心的一些东西还是会可能不在文章里写，然后可能会做一些他们没写什么的 discover。
但是就就我还是觉得，如果是要做纯粹的科学与创新的话，就是呃稍微往学术一点，就是少一点就那种。商业的一些顾忌多一点，学术的就是信任与纯真，我觉得是好的一个，希望大家一起啊，是一个好的，就是工业界的一个practice。对，中美呢？中美的话，我也不知道。就是我觉得好多，反正人才不分世界，对吧？但大家可能有，就是有些同学愿意在中国生活，有些同学愿意在美国生活之类的，就不知道。
嗯，你觉得二零二六年你对A I发展会有哪些预期？二零二六年，我觉得大家应该能把这个会看到很快。我觉得我们能看到第一个 continual learning 的一个小模型，啊，我觉得我们很快能够去呃看到一个非常好的 multimodal reasoning model。我们很快所有的这些就是什么 agent economy 全部会被 scale up。
呃，我觉得我有一些个人大胆的预测，我觉得很好值得做的一个 orchestrator 是很好值得做的。然后我觉得 sub agents，刚才讲过是很好继续做的。哦，我觉得 formal verification tooling 应该作为 RL reward 完全是 under explored。这个和我们做的也很有关系。
嗯，对你刚才说的第一个和第二个分别，你说的是被谁做出来？第一个，呃，continual learning持续学习，我我知道有一些不错的团队，我感觉他们很快就能出苗的。那是小公司还是大公司？呃，小公司，全是小公司。哦，都是牛 lab，都是牛 lab。multi model 也是吗？啊，multi model 也是牛 lab。
他们应该很快就会，就是很快就会问世了。还在Sales的一个公司，也是我的好朋友。哦，对，当时也希望他能来加入Action。最后，也祝福他。嗯，一些快问快答。嗯，一个全球范围内你喜欢的食物？全球范围内喜欢的食物，呃，喜欢就是寿司，任何的寿司。一个全球范围内你喜欢的地点？啊，喜欢地点悉尼。为什么？我小时候第一次出国是去悉尼。
一个少有人知道，但是必须知道的知识点，可能是一个冷知识。你可以自己打CPU。你最近对于生活的一个非常新鲜的。鲜活的认知是什么或者体验？我可能我最近过的也不是特别鲜活。我每天早上就是几点钟起来，然后一直工作到晚上几点。哦，鲜活的认知和体验就是，我觉得还是呃，每一次我去就是在跟就是新希望能加入Action的同学聊的时候，就会觉得呃，未来无限好，未来无限希望，然后觉得。
感觉到那种自己曾经做这件事情的初心，并没有因为就是反复日复一日的执行，感觉被打磨掉，就是觉得非常的快乐，感觉像是两只鲸鱼又在找到了彼此的这个聊天频率，这个这个还是挺好的。所以招人是一个我非常快乐的事情。鲸鱼找到了自己的聊天，就是对，就是有些鲸鱼它那个就是频率跟别的鲸鱼不一样。然后如果说你遇到一个人，然后你们都以前是学数学的，然后可能你们现在都对AI
for Math有一些理解，但你们又同时有一些新的理解，然后你们聊一些东西的时候还挺有意思的。
另外一个我觉得比较鲜活的体验是我们就是发现非常多了。古老的一些技巧，对我们现在的这个比较前沿的研究有这个有这个有指导价值。然后这个有点像这个二十四视频，它有一个叫呃“如江不进，与古为新”，还是挺有意思的。每一次有这种 callback，我觉得特别有意思。像世界是一个世界是一个圆，我们又回到了原点。你心目中影响 AI 进存的几篇论文？
呃，我觉得第第一篇，我觉得是啊，就是啊，其实是啊，Christian Zaglidi的那个白皮书，Christian Zaglidi的那个白皮书呃，第三篇主要 sketch and proof 这个讲过了。第四篇其实我就是一堆 bundle，就是从 Kiemena Prover 到 Deep Sea
Prover、 Google Prover、一和二、Seed Prover、Hilbert Prover，所有的这些就是真的在拿 RL 它做起来了的。
因为我们刚开始的时候连就是从来没有一个 RL 做的 formal prover，我们刚开始的时候连这个都没有。我们在融资和这个呃做这个法律，使得这个钱到账的这个过程中出现了。基于当下的认知，一个你最关键重要的大词是什么？啊，我bet system，我不bet model。呃，我bet就是这个system有非常多的事情可以做，然后包括orchestrator。
然后我另外的一个基于与这个又相关的一个bet，就是我完全相信recursive self improvement是很快就能够做出来的。然后有一个问题就是，如果你做出来之后，就是然后呢？你是然后做什么？这个东西就是能否就是？我觉得可能会出现一个呃，这个需要一些 forward deployment 的一些东西。
我觉得 forward deployment 的东西还没有在 AI 的时代得到一个革新，让我觉得传统下次会死。我们工作室叫做语言及世界工作室。当你第一次看到这个名字的时候，你会想些什么？我第一次看到这个的时候，我想的就是说，我觉得数学家们他们在几千年和或者几千年几百年，他们都是在拿英语写代码，或者说拿中文写，就拿他们的那个本国语言写代码。
就是，他们在进行的是逻辑的推理，但是他们是在自然语言里面去进行的逻辑推理。这是一个让我觉得非常神奇的一件事情。然后，由于这个特质，现在我们可以看到，说是，比如说，呃，就是就是做这个计算机的同学们，可以拿自然语言去写。写代码，但数学家已经做了，就是几千年了。所以数学它所有带来的这一些结构啊，这一些逻辑，为什么说和这个代码验证它有帮助？
其实是有这样一个特性。这是我当时在想的一件事情。然后另外我在想的一件事情就是说，如果你去把嗯。这个世界想象成一个 manifold 的一个比较高维的这样的一个几何拓扑的一个流形，你这个语言它这个带来的，或者说是基于 text-based 的就是 next token prediction 这个 AI，它到底在这个上面。
有有多少探索了多少，然后又 flattened了哪些呢？我反正就在我曾经有段时间在想这个，因为我在想怎么调 loss function，但是呃，就是这是这是我就是的一些感受，对。We'll explore the new world from here.好了，今天的节目就是这样。这里是商业访谈录，是一档由语言及世界工作室出品的深度访谈节目。
你可以到公众号关注我们的工作室，获取更多的信息。我们的公众号是语言及世界（Language is World）。我们希望和你一起从这里探索新的世界。xyz:zxj 137. 对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的