A 4-hour Interview with Carina Hong: AI for Math, Lean, Proofs from The Book, and Intuition

哈喽 大家好 我是小珺 今天我们来到了美国硅谷 此刻 正在扎克伯格最早的创业所在地 Facebook House 这是一栋外表为淡蓝色的 可爱的小房子 而今天也将迎来《商业访谈录》 最年轻的一位嘉宾 她是一位00后的华人女孩 名字叫洪乐潼 她的探索方向是AI for Math 所创办的公司Axiom 刚刚完成了

估值为16亿美元的A轮融资 而她引起了很多人的关注 则来自于这样一条新闻 57岁的美国终身教授突然辞职 去给24岁的华人女孩打工 那接下来就是我对洪乐潼的访谈 因为我确实在每一个时期 都觉得是 自己是那个环境里面最愚蠢的那一个 最怎么样努力都看不到结果的那一个

就是在你的心目中 AI for Math它在整个AI的大地图上 它应该画在哪个地方 我觉得大部分我知道的就是 嗯 founder就是创业公司的创始人 他们都对 就是苦难上瘾 我听下来 我会有一个问题 因为现在coding也很火对 那用math作为手段 和用coding作为手段去执行任务的区别 会是什么呢 没有人喜欢融资

没有人喜欢融资 它不是说难 结果难 它就是累 呃 你是一个复读机 你一次一次的说一样的事情 你一次一次的接到一样的问题 真的我就能 我可以可以把它录下来 然后我就给你们大家发 对吧 你们反正问题也是一样的 但是呢 就是从这一些大量的

比较无聊的这个过程中 有一些让人很激动的谈话 通常这一些谈话是你最终选择的 选择的投资人 比如我印象特别深刻的 我们最后的领投方B capital 我跟Howard Morgan 就是有一个对话 hello 乐潼 还是先给观众朋友们打个招呼 并且做一个简单的自我介绍 好 hello 小珺 谢谢你邀请我 我是洪乐潼

Axiom的创始人和CEO 嗯 我想 我们的聊天可以从一个故事开始 就很多数学家在说 自己被数学打动的那个时刻 都叫做 被数学击中的时刻 比如说高斯（数学家）就说像闪电一样 你自己有过这样的时刻吗 我就是自己解题的过程中 这个稍微就是低频率一些 但是我经常在看别人结果的时候 有一种 哇

这个东西怎么这么美的一个感受 我印象中特别深 其中一个例子就是说 第一次看到这个 模形式与椭圆曲线的对应 就是说每一个这种模形式 它都对应着一个椭圆曲线 相当于是把 一个比较代数性的一些 一个表达式 和一个更几何性的一种几何

几何物体 就是联系起来 然后我觉得 数学中这种 两个领域 然后 他们相当于中间有一个交集的 这样的一个例子 还是每一次 我都是觉得非常非常非常优美的 然后啊 我印象中就是还有另外的比如说概率 然后物理 那里面又有一堆的可以 就是 啊

让我觉得非常就是有意思的结果 然后我自己解题的话 还是就是小的时候可能见的不太多 就是 觉得数学还能还能这么玩 就是当时从初等数论的时候一直推 推到这个二次互反率 我当时在美国的一个叫罗斯夏令营 然后它每一天就给你 每一天给你一个题集 然后你要把它全部做完 还挺多题呢 全部做完才能拿第二天的题集

像游戏打怪一样 然后 如果你做不完所有的题 它就不给你下一个题集 然后你就看你隔壁的那个同学 已经就比你就是多了3个题集 有更多有意思的 可能是正确的东西 但是由于你的证明能力还没有跟上 你一直到不了 然后到最后到二次互反率的时候 就是它给你呈现了很多的证明 我在这个过程中 一定是觉得有被数学击中的时刻 然后

就是觉得非常表达非常简洁的东西 它后面的这个证明可以很深 然后也可以有很创造力的一些解法 我有一个问题啊 它可能会很好回答 也可能会很不好回答 就是有一天我跟AI在谈论数学的时候 它提到数学是一种结构的语言 所以我想知道 从你的视角来定义数学到底是什么 对 啊 这个确实不太好回答

我觉得 数学它有一点像是说是人类 我们决定说去创造一个文明的体系 然后在这个文明的体系里面 由于一些就是我们愿意去说是 我们认为是 是对的一些公理 然后往上去搭建 就是我们 它其实某种程度上是数学家 它有一个契约

就是说哪一些东西我们是愿意接受 是 呃 理所当然的 然后在这些东西上面 最少的理所当然 或者说不一定是最少 看你从哪一个角度去看 有一些人 他会去从compression压缩这里去去看 他希望是最少的公理 有一些人是去希望 能找最有意思的 或者说就是搭配 最合理的一套公理系统

然后往上再搭建 然后往上搭建的这个过程中 其实我觉得这个过程是 很多人觉得数学是解题 就是我有一道题 然后我把它做出来 但就是往上搭理论的这个过程 其实很有意思 一般是先从一些数学的一些例子出发 一些它就是 呃 比如说是一个序列 或者说是一个集合 然后你去发现一些规律

然后这个时候你觉得很自然而然的 下面的一个题应该是怎么样的 然后再去证明它 所以这个过程其实有一点点像艺术 我觉得数学是一个 介于艺术与科学之间的一个存在 所以数学到底是一个被发现的过程 还是一个被创造的过程 这是一个 千古的难题的辩论辩论点 嗯 你是哪一派 我觉得就是 呃 如果就是一些数学家

他们有一套比较相似的训练背景 或者说他们在同一个领域里面 他们阅读了同样的一批代表作 他们会有一个某种程度上 比较大的一个默契 去说 我们认为这个很自然而然的 它应该是是什么样的 然后如果说出现了一个 比如说最有意思的 就是当拉马努金（印度著名数学家）

他从印度来到了英国 他遇到了这个哈代（英国数学家）和Littlewood（英国数学家） 他们就是哈代（英国数学家）和Littlewood（英国数学家） 他们两个人 就是一直就他们两个写paper 他们写了很多很多的文章 然后拉马努金来到这里 就是像一个外星人一样 他说 嘿 这是我的这个草稿本 上面这些东西 全都是对的 我从来没有接受过数学的这个训练 我不知道怎么去证明它 然后哈代和Littlewood 我就会觉得

这些东西看起来很有意思 他们很新 然后他们和我们之前做的东西 又感觉是 又感觉这个东西是对的 但是 所以他们就开始用证明 所以某种程度上 证明是一个 与原来的这一群数学家 所不太一样的 一些人 他们可以用证明来说服他们证明 其实某种程度上它是影响力

就是我只要能够去把这个东西 严丝合缝的逻辑证明出来 我这个数学的发现就是可以被接受的 然后在它被接受的这个情况下 当然了 就是又会说 你这个证明是美还是不美 是自然还是不自然 这个 我们之前看到很多国际的数论学家 去看 张益唐先生的这个数论证明 他们就觉得

这个证明是和他们熟悉的一些学派 非常不一样的一种证明方式 但是在 呃 就是非常著名的那一个 那个结果就是 素数的这个固定的这个差 这个他们觉得又是正确的 所以他们又接受了这件事情 于是就是又开始去互相的去 去学习和整理他们的证明方式

比如说James Maynard 2022年的菲尔兹奖 他有另外的 他的一套的证明的这个技巧 然后他的学生们去继承 他的证明的技巧 然后他 他和这个张益唐先生的这些 就可以进行 大家可以进行比较 也可以进行简化 这个过程其实是非常非常有意思的 一个智力过程 你是哪一派啊 是那种直觉派 天才派 还是证明派

我一直就是非常希望能当直觉派 天才派 然后这其实是我很小 痛苦的一个根源 就是我一直发现 我自己没有什么特别大的数学天赋 就我是一个蛮力型选手 对 我是蛮力型选手 就是你给我 我小时候在打数学奥赛的时候 我记得他们说 就是每个卷子的第一道题 几何题 欧式几何题 欧式几何题是必拿的分

你如果不拿欧式几何题 你连这个三等奖你都拿不到 然后我就一直做不出来欧式几何题 我倒是可能 能做代数不等式 我的大脑可能更偏代数的符号的表达 然后几何和拓扑实在是差 所以我一般就是去把每一个点 然后每一条线就用这个复数法 就是大力出奇迹 最后我不需要去理解这个几何题

它背后的几何意义 我就把它完全是就是照本宣科的 去拿一个套非常复杂的复数法 去把它就是解决出来 我可能会需要比别人多2到3倍的时间 导致我可能其他题目的时间分配不均 但是这是我做这个几何题的唯一方式 其实最有意思的是 2021年开始 就是Google DeepMind 他们很秘密的开始 一个这个AlphaGeometry（DeepMind开发的AI数学推理系统）的

这个项目 就是说 如果我们这个拿AI去证明欧式几何题 非常困难 感到困难 能否把它变成符号表达 它这个不是复数法 跟我说的这个人类 我这个人类做的方式是不一样 但它这个背后的哲学 是一样的 我把几何的图形变成这个符号表达式 于是这就是 他们就能够通过这个东西去解决 好像81%的 就是AI的

呃 就是AI能够解决81% 历史上IMO的几何题 嗯 这是一个很有意思 这是一个我不是天赋型选手的 这个解释 解释一 我有一个解释二 就是我在MIT的时候 我身边所有人他们都是天赋型选手 所以你只要就是看看左边 看看右边 就知道自己不是天赋型选手 但是呢 我不放弃 我是打不死的小强 就是你给我一道题 我三个月我做不出来 我继续想

我记得当时Henry Cohn教授 他给了我一道Sphere packing（球堆积问题） 让我去想一些关于28维的 这个Sphere packing的一些小的问题 这个东西当然不可能 就是期待一个本科生完全解决 然后我6个月我什么都没有想出来 但是我每一周我就去说 哎 我这是我试过的 我没有成功 然后我又试了一周 我又没有成功 所以但这个这种蛮力型 其实某种程度上

会和一些天赋型选手存在一个互补 就是说 他们可能有一些脏活累活不愿意干的 我可以把它去干完 所以你的这个过程 有点类似于AI的过程 AI是这种蛮力型选手吗 AI是直觉派吗 现在AI里面 它也分了这个比较天赋型聪明型的AI 和这个 和这个比较蛮力型的AI 比如说我们现在这个 我们公司的这个AI系统

它里面就是 它是一个系统 所以它中间 有很多的模型 它有一些模型就是能够很快的去 认定这个题目 应该是被1 2 3 4 5 6 7步这么大概证明出来 然后就是 偏形式化 见到了很多很多Lean这种形式化语言的AI 它就会说 哎 反正我就是一个Tactic（策略） 一个一个 Tactic（策略）（策略）

是Lean里面的一个步骤 或者说是策略 它能够让你就是从 把你的一个很复杂的问题 一步一步的去把它解决 它更是这种严丝合缝 就是小步小步走 然后不是之前刚才讲的 那一个能够列提纲的AI 所以其实AI这系统里面 两种就是类型的AI数学家 它也能相辅相成 某种情况下

其实最有意思的是 呃 当看到一道题 就是我们发现 在我们最近 呃 我们公司 在这个普特南大学生数学竞赛中 就是这个AxiomProver AI拿了满分 嗯 呃 然后是呃 人类历史上有5个满分 呃 过去的98年 1927年开始第一第一次普特南数学竞赛 然后这是第六个满分

是一个AI拿到的 然后我们就有看这个AI的解法 有一道题我印象特别深刻 我们队伍中有这么一个同学 他叫做Evan Chen 他是美国就是IMO 数学竞赛队的这个教练 所以他是非常天赋型的一个选手 他看到这道题 他画了一个图 然后我们所有人当时在那个会议室 一看到这个图 我们就说 哦 那你是把它做出来了 就一个图的一个解法

这个AI果然就没有找到 这个图的解法 我们看到 就是几千行的这个Lean代码 他是就是硬生生的 把它 某种类似枚举 类似分类讨论 然后呃就是一步一步一步核实去 把它就是干出来的 所以就是这是一个大力出奇迹的AI 它可以看到这个机器 它会去就算是一道

很明显 可以去做创造力解法的一道题目 它可以去通过它自己擅长的东西 去给出 给出一个完全不一样的解法 其实我觉得去比较人类与AI 就是得到的这个证明解法背后的数学 是一个非常有意思的过程 嗯 所以数学不是人类的特权 对吗 嗯 现在感觉上

这个自动定理证明这个领域啊 发展的很好 嗯 其实这个领域 它 呃 不能够叫是AI的胜利 它在 呃 没有AI 没有这个深度神经网络的时候 就有一群电脑计算机科学家 他们就是去希望能够使得 呃 基于规则的电脑系统

能够去帮助人类 去解决 呃 能够解决的数学问题 然后这就是叫做 自动定理证明ATP 然后ITP就是交互性定理证明 互动性定理证明 就是毕竟有一些ATP无法解决的 就是过去 会有一些人类 他们是数学家 他们也会去呃写这种Lean 这种特定的这种啊程序编程语言

他们就会去与这个电脑系统 一起去合作 证明这件事情 现在其实我们只是把这个ITP中的 这个人类 换成了一个AI而已 它这个古老的这个学科 其实某种程度上是ATP与AI的 这样的一个 交集 我相信很多人都还是会对你很好奇 嗯 你虽然一直在说你不是天赋型选手 你是一个蛮力型选手

但是你的过往的背景非常的强 嗯 所以还是想聊聊你自己 你在广州长大 广州是一座非常有烟火气的城市 所以 你的小时候的成长环境是什么样的呀 对 呃 广州是一个非常非常有烟火气的城市 呃 其中我最深刻的一个童年记忆就是 确实有很多好吃的 就是感觉 呃 到了后面长大就是留学

感觉就是食物上比较匮乏 尤其是和家乡的美食比起来 呃 我爸爸妈妈 我们是在广州呃 我在广州出生长大 然后我们住在就是离学校很近 所以就是每天可以走路去上学 然后有些时候 上学的时候就也会想想数学题 然后也走到不知道哪里去 就是这种 呃呃

说是就是想数学的同学们经常犯的 这样的这个习惯 我也有啊 走路到学校多多远啊 就10分钟 然后就是有时候会会开始游荡 因为就是 有时候脑子会想想别的事情 其实 我觉得这是一个非常快乐的一个状态 啊后面就是我最近创业啊 我有一个这个导师 他讲到一个概念

就叫做 bounded attention和free attention bounded attention的意思是说啊 被框架住的注意力啊 然后free attention是说自由注意力 比如说我们 呃 每一天早上起来 我们会看到很多邮件 然后我们会有很多 我必须要执行的事情 因为我不执行这些事情 可能说有一个 期限性 你必须要把它执行掉 这个时候你的大脑是在一个

被框架住的注意力的 这样的一个情况下 对 然后呃 很多很成功的企业家 他们是非常有纪律性的执行家 他们就是每一天日复一日的去compound 复利他的这个执行呃 呃 这个很好 然后所以我一开始就是创业的时候 非常希望我每一天能做多少事情 做多少事情

但是 就是后面这一个自由注意力 其实是能够区分 一个平均的一个创业者 和一个很很好的 一个很有呃 策略性和决策性的一个创业者 的一个区别 其实是在自由注意力这里 或者说一个数学家 自由注意力这里 是可以把人与人之间的这个差距 拉开了点 所以当你所有的时间呃 自愿的去

由于说我要做一个像 呃 就是像军训一样 我每一天就是要干掉多少活 你可能会使得你这个自由注意力 这一块 呃 反而是欠缺了 你丧失了很多的机会成本 所以我就是特别有时候怀念小时候 就是走路上学的时候 就是有很多这种自由注意力 某种程度上 呃 就是就是人家说爱因斯坦的洗澡时间 这个过程中

其实能够 呃 有很多很有意思的一些 就是大脑能到一些很有意思的地方去 这可能是灵感和直觉 来到你的大脑里的时候 对 但是呃这个事情是它不是一个线性的 不是说你投入多少自由注意力的时间 呃其实也有可能自由注意时间 你什么都没有想到 然后在后面的你可能

在被逼迫做一些任务的时候 在中间你会就是有一个callback 就是回到了你 其实自由注意力 给你大脑里面 打下的这样的一个基础 你反而会在那一刻 可能 可能你大脑也不想做那些无聊的事情 它就说唉 我想到了这样的一个呃 比较有创造性的一个想法 所以自由注意力和bounded attention 和限制性的注意力 它应该是结合的

它有配比吗 不知道 我觉得大家的配比不一样 人家说有三种创业者 第一种叫visionary 就是有前瞻性的野心家 第二种叫做execution 呃 executor就是执行 他就是能够呃 其实扎克伯格 我们在这个Facebook小屋 今天特别特别有意思的一个场地 呃 扎克伯格 他就是一个执行狂 就是 他是一个执行执行执行 执行执行的一个人

然后你可以看到他嗯 每隔一段时间会有一些啊行动去弥补 可能前瞻性的决策落后 所以他是一个非常就是执行的 执行派的一个企业家 然后第三种就是销售派 就是它 呃 能够呃 销售派其实并不是一个负面的词 就是他有非常好的沟通能力 他有非常强的

与不同的这个受众沟通能力 然后他能够去影响别人 引领别人 然后把一个队伍就是这么建起来 呃 我一直从来不觉得我是销售派 这个是肯定肯定不是的 呃 然后我 呃 也不是一个多好的执行派 其实我也 我可能就是也不能叫做前瞻性 这个前瞻性是说是对的 我就是想做 一些事情 然后我想做一些事情会极度乐观

然后我极度乐观的情况下 呃 就算是往下就是跌一点 它好像也也还 也还行也还达成了一个KPI 所以你觉得你是第一种visionary 我觉得我是visionary 我反正肯定不是salesman或者是executor 你刚才说扎克伯格是属于第二类 属于是第二类 对 然后你觉得像其他的一些企业家呢 在美国这边一些知名的企业家 知名的企业家啊

马斯克是visionary 这个是绝对的 然后Sam Altman是salesman啊 然后啊 我觉得一定要互补 就是嗯 比如说扎克伯格 他身边全是梦想家 看Mike Schroepfer（Meta前CTO）这个CTO 梦想家嗯 他也有其他很好的执行的 其他执行的人 就是我觉得光互补也不行 你要有一些是你的同类

然后有一些是互补 呃呃 桑德伯格做了很长时间的 很好的执行家呃 稳健的去呃 把0-3,000人的情况下 这个文化都把持的很好 其实我觉得Facebook非常强的一个点是 就是每一个Facebook的人 他们都bleed purple 就是他们的血液里面就是紫色 就是就是Facebook的这个颜色 他们紫色 紫色代表什么

呃 紫色就是Facebook的办公室有很多呃 很疯狂的颜色 其中有一个很明显的是紫色 其实这个是因为扎克伯格 他是他是呃 color blind他是 呃 有一些颜色光谱无法区分 所以说他的那个就是办公室 有非常大胆的 大胆的颜色和 其实去看那个Facebook的这个园区 像是一个梦工厂

它有24小时的这个雪糕店 就冰淇淋店 然后有地方让啊 就是大家去玩鼓玩吉他玩乐队啊 我们公司大部分的人 其实之前都是在Facebook的 所以你很了解他们 对 他们有一个非常强的 一个叫做bottoms up的culture 就是由下往上 嗯而不是往 而不是上行下效 它是这不是top down 就是top down非常Google 然后bottoms up 非常的Facebook

所以我们公司其实某种程度上 并没有一个定义文化的机会 我们某种程度上沿袭了 呃 我们大部分的早期创始员工 他们本来的文化 好的 关于Facebook 我们后面还会聊到 我们先回来 你在广州那个城市是怎么长大的 对 就是 嗯 打打数学竞赛 然后呃 我看看百家讲坛 我是非常喜欢这个百家讲坛

对 我非常喜欢 就是所有的 就是 呃 中国的这个文学与历史啊 我喜欢就是看那些历史故事 我当时记得就是易中天讲三国 然后 诸子百家 然后就是还是非常快乐的一段时间 我特别喜欢文学 就是黄永玉 他有一本书叫 大雅宝胡同甲2号 比我老的老头 就是那本书的书名 然后其中讲到了这个啊

中国的这个文艺界啊 就是画家 然后作家 然后他们呃 各种各样的画家 版画家雕塑家 然后呃他们都住在这样的 一个北京的一个胡同里面 我妈妈她是 她是北京人 所以说我们家某种程度上 我们虽然住在广州 然后又有受很多这种 京城文化的这个影响对 所以我发现 你小时候自由注意力是很旺盛的啊

很旺盛的自由注意力 因为你并没有把所有的时间 都集中在数学上 我 对 我也被数学教练小时候就批批评 说不是最刻苦的那一个 OK 但是我如果遇到一道题 这个题就是要跟这道题去死磕 我就这是某种程度上 你如果看我花了多少时间在那道题上 你会说这个小孩很刻苦

但这个过程中像玩一样 不 它不像work 嗯 就我觉得区分说是呃这个框 框住了的 这种呃 限制性注意力和自由注意力的 这个其实是一个主体感知 就是你到底觉得你是在玩还是在工作 然后我觉得呃 我小时候大部分的事情都感觉是像玩 然后就是那些学校的作业 就是一般课间就写完 然后我放学之后就所有的时间

我就是可以做一些其他的其他的事情 呃后来就是大概是初一的时候呃 发现就是可以去可以发现了 一个一个事情 就我可以去找一些 就是更高等的数学书看 就小时候是呃 意识到说我一直要做数学竞赛嘛 所以我要 比如说3年级做5年级的数学竞赛题集 就是一直是做数学竞赛 更高级的

但是到初中的时候就开始 我为什么不去学学高等数学呢 所以就是开始看 就是呃微积分啊 就是 当然 实分析复分析 哇 然后就觉得非常有意思 因为它不像是一个零和游戏了 就是做数学竞赛的时候 总觉得 其其实比如说在这个呃 广东省的这种奥数这种 这个训练环境下 嗯比较痛苦的一点 就是你的同学们

他们要跟你考同一场试 所以对于一个小孩来说 这种友谊的这种概念也比较复杂 就是竞争 它就是特别存在 但是你如果是看高等数学这个 你这 它没有 它不是一个零和游戏 它是一个正和游戏 你 你可以自己就是到你想到的这个深度 广度然后你可以找一些 你们班里

就是对这个比较感兴趣的同学们 一块去讲 然后你们不需要某一天 同时去参加某一个考试 所以那 但是你还是要回来打这场零和游戏 啊 对 我还是要打这个零和游戏 然后这个就是零和游戏上 就非常吃亏了 有些时候看到一个卷子吧 就是4道题 最后一道你就发现是数论啊 数论多美啊 你 你可能刚最近看了这个高等高等数学

里面去学了更多就是数论的 呃呃 这种这种高级的这个这个概念 然后你就一套卷子 你如果你的理智会告诉你 你要在这个零和游戏中取得高分 你应该先把第一道欧式几何题 把它做出来 接着你做第二道代数不等式 然后最后这道数论题 大概率你是做不出来的 你要是做出来你就进省队了 然后所以 呃

你不应该拿到这个卷子的第一课 先从最后这道题开始 但是我当时由于我 呃 就是课外的这种非常浓厚的兴趣 加上我非常的喜欢数论 我长大也是 就是做数论 我觉得我 非常非常的爱数论 于是我就会先从这道题开始 然后一般来说这个时间就开始流逝 然后在一个呃一个 一个固定的一个比赛时长中 这是一个不是最优的策略

你是一个竞争欲很强的人吗 因为你刚才也提到啊 就是在打比赛的过程中 这是一场零和游戏 也会影响一些友谊 你是一个竞争也很强的人 我觉得我在呃拒绝被驯化 成为一个竞争力很强的人 你在拒绝 对 我在拒绝被驯化的时候 意识到的 我意识到的 对 我当时你很难不意识到 你小学数学

奥林匹克学校的时候 我记得四年级到六年级对吧 每一个月考一次试 然后每一个学期之后 他把你1班到24班全部重新排列 就是说你如果22 23 24班是重点班 然后就是1班在这个楼底 24班在楼顶 然后 你每每学期之后 就是把你这个

就是同学们 就是换换教室 24班的下去了 下到19班了 不是重点班 你楼梯也往下走 你这个心情肯定也不是特别好 你一般在哪 1班在楼底 我当时进去的时候我是4班 然后我记得就是就在这个洗手间旁边 这个感觉就是说明这个 我入学考试考的是真差 对 不是天赋型选手 就牟足了劲 想上这个22 23 24的那个楼顶

听说楼顶这个风景也好 对吧 就 就 一个四年级的一个小朋友 她肯定是会呃有这种就是争强好胜心 就是在一个比较 呃 呃 大家就会有这种压力的感受 然后我后面是觉得就是这个不好玩 我不想玩这个 后面是什么时候 呃 初中吧 初一初二 就我开始看这个呃 高等数学书的时候

我就开始不太想玩这个游戏了 嗯 那你做出了什么样的改变呢 在你不想玩这个游戏之后 嗯 就客观条件上 你还是要去参加那些考试 你还是要去排名 你还是要去竞赛 我不是那么在意了 就是我一直不到初三 我没有 就是初三要打初中数学联赛了 然后 我就是 呃 开始初一到 临初中数学联赛

我才开始准备初中数学联赛 最后好像也考得非常好 这个初中数学联赛 就是反正我当时还特别就是惊讶 我觉得我肯定是要考砸 但是 呃 初中数学联赛考的挺好 然后到高中的时候 就是更多的时间 就是 呃 当时还学英语 对 高中的时候又更多的去学英语 毕竟当时也打算是要出国 所以就是更多的时间花在这一些 这一些事情上面

然后 嗯 我其实觉得做出来的改变 其实就是我发现一个有意思的事情 就是你在一个群体里面 你如果发现 大家有一个很清晰定义的一个目标 然后每个人都往这个目标 也就是当时的 不管是下一个季度的什么数学竞赛 开始 呃 准备的时候 然后你自己有一套完全不一样的这个

mental model 世界的这个模型 你就会开始找呃 这个群体里面的一个tribe 一个部落 嗯 你会希望能够去建立一个小的 一个部落 嗯 然后去找 看谁跟你一样 想读这个 跟考试没有关系的书 然后你就会和这些人成为很好的朋友 我记得我初中的时候有一个 有一个游戏 我到现在其实我们也在

有时候闲的无聊也在玩 就是你有一个n乘n的一个格子 你有一个棋盘 比如说8*8的一个棋盘 然后你可以从这个任何的一个格子 开始去走马步棋 就是你只能去走这个跳马 就是2*3 就是的 这个每一步你只能这么走 然后你呃 连续的这样去走 然后你每走到一个格子 你就标1234 就这么开始标 最后你的目标是说

我能够走满每一个格子 不重复 或者说你走不满每一个格子 你希望走到一个更高的一个数 比如说8*8的话 你希望尽量靠近64 你不要在50你就停了 你希望至少到个59 就是这个 这个游戏 我当时我记得 我初中就和好几个好朋友 我们一块玩 然后我们就特别希望呃 呃 我们一开始开始比看谁的数更大

后面我们就希望能够去证明说 任何n至少是5的一个棋盘 你永远有一种 能够走满整个棋盘的方式 我们希望拿 就是我们当时猜测 应该能拿数学归纳法去证明 如果你要去拿数学归纳法去证明 你就需要在n比较小的情况下 去构造一些 比较 有代表性的一些base case基础情况

于是这个是一个非常复杂的工程 然后我们所有的这一些 对这个游戏 比较感兴趣的同学 我们就开始去构造 然后非常难构造 然后所以就是群策群力一起构造 让我有一点想到 我们等会我们应该会聊到的 就是形式化证明 比如说陶哲轩老师 还有就是Alex Konterovich 他们做这个素数

素数定理的这个证明 然后 他们就是把它也是分了很多 不同的项目 让全世界的几百个数学家 和Lean的这个编程 呃呃 这个编程 编程的同学一起去把这个事情搭起来 有点像 就是数学 其实某种程度上 大家强调说这一个人 他是一个天才 他一个人证明了 一个

困扰其他所有人几百年的一个猜想 然后他是一个多么厉害的数学家 他有一种 呃 个体性的一个强调 就是说这一个人他非常厉害 但数学如果你去看啊 软件工程师 他们几百个人 几千个人去做一个project 一个大的一个项目 它是合作性的 合作性

就需要一个比较好的一个结构 和把它就是把这个呃任务去分散 分散成不同的小任务啊 这个过程其实我觉得是很有意思的 然后某种程度上 在玩这个马步棋的时候 我们当时就是 我反正一个人 肯定是不可能把所有的这个 这个例子找出来的 我需要我的这些同学们 这个小部落的这个帮助 多少人啊

这个小部落一般是3-5个人 3-5个人对对对 是数学很好的人啊 我们当时是那个数学班 就我们整个班都是数学很好的人 然后就是上课就 听课了就是就是传纸条那个 纸条上就画着这个格子 就是说这个 你看我又找出来这样的一个 就是n等于 比如说9的时候已经被我q掉了 就是非常快乐的一一段时间 在这个这么快乐的时候 你的成绩是什么样的

呃 就我反正要不到大考 我也不太 我还还行吧 我反正也到了 那个 反正你的最终的目标就是你初中 好像我们是九十个人 你要进到一个20 25 27个人的 一个数学组 高中这个数学组 所以我也进去了 我记得我们当时是啊 7个女同学好像 初中

然后啊 到这个高中 好像就是 25 27个人 三四个女同学 反正就是也那么进去了 但是这就很奇怪 因为你说你不是天赋型 你是蛮力型 可是你实际上花的时间没有那么多 对这就是一个很有意思的一个点 就是我认为 你在学这些高等数学的时候 某种程度上 你的竞赛的这个数学啊 也在得到这个潜移默化的提升

这其实是很有意思的 就是 我们等会应该可以讲到 就是 我们发现 最近有一个AI的一个发现 就是说我感觉我像是 这真的是我每天在想的事情 我不是在打硬广 就是一个数学非常好的一个模型 它在编码能力上也非常好 就是它会有这种东西叫做transfer learning 就是转移技能的转移 嗯呃 我觉得肯定有这么一定的程度 反正我当时我记得那个考试吗

就是从初中考到高中的那一个考试 我是觉得 我肯定要完了 然后我的爸爸妈妈说你应该没事 你就去那里坐一坐 你看一下 就是结果怎么样 反正觉得应该你能考好 然后结果 我觉得我应该是拿了满分那一次 然后我觉得我我连几何题我做出来了 我十几个

大的考试中 没有做出来过一次几何 所以那次也可能是运气比较好 噢 这个很神奇 就是从学习上 对于你来说 突飞猛进 是来自于你其实变得更发散了 而不是更聚焦了 你不是更努力的去做题了 而是变得你可能兴趣爱好更广泛了 你更想玩 去做这件事情了 对 嗯 我当时是这么觉得的 但是这个事情到后面 我在大学的时候

在MIT的时候又觉得还是要学会聚焦 哦 就我 我觉得可能就是数学好这件事情 它没有公式 然后我一直也不是数学最好的那一批 就是每一次大家可能说啊 你以前打数学竞赛 然后 可能现在在计算机的这些同学里面 我有一定的这个数学背景 但是我在麻省理工的时候 我身边的每一个人他都比我聪明

每一个 我是整个数学系里面最愚蠢的 是你自己这么觉得 但是别人也觉得 自己才是最蠢的那一个 我觉得 他们应该是意识到他们是很聪明的 他们意识到自己是天赋型选手的 哦 为什么呢 为什么你会有这种感觉 你觉得自己没有他们聪明 就是你的背景 在别人看来就已经是天才型的 选手了 但是我当时我的同学们 比如说任秋宇

张盛桐 高继扬就是这些人 每一个人都是在这个 我小时候看着他们的新闻长大的 我看着他们的新闻长大 看到他们去了北大数院 看到他们转学到了MIT 见到了真人 我每一天就是在 就是顶礼膜拜这些大神 就是我当时在MIT的时候这种 这其实是一个非常有意思的 一个点

其实甚至是有一些其他的小国的 这个IMO的选手 比如说我有一个好朋友 他是这个 比利时的这个 这个IMO来到MIT 看到美国和中国的IMO们 然后也知道大家的IMO分数 他也会有一个心理落差 我这个其实没有落差 我的期待就是我是最傻的一个

所以我 我其实就是适应的也很好 我反正我就觉得我每天很幸运 我和能能和这些人一起说话 一起上课 一起做作业 我觉得还挺好的 所以 你对你预期没有那么高 我预期没有那么高 我觉得我当时觉得我来到MIT吧 我可能以后就去做这个量化金融了 因为我可能反正你说这个数学博士 为什么他会要我

而不要其他每一个人都是IMO金牌呢 就是他肯定肯定 我觉得我肯定也考不上数学博士 所以我 那我就 反正我记得我大一的暑假 我就是 本来是要去桥水基金去实习啊 啊因为当时就我想着我要做金融了 那我肯定秋天就是校招的时候开始 大一去递简历 然后我记得去

还是挺高兴的 就是能能当时去桥水 然后当时疫情来了 疫情来了的话就 桥水就变成从一个呃 就是线下的 变成一个网上的这个实习了 然后同时当时就有另外的一个机会 就是呃我当时被professor Ken Ono 小野肯（Ken Ono） 我们就是 他现在 也加入了你们 在Axiom

他是 呃 当然他是一个就是神级教授 他有一个就是REU REU的意思是research experience for undergraduate 是在美国是一个名词 就是给本科生的暑期数学研究项目 这些项目他们竞争非常的激烈 他们是美国的这个自然科学委员会 他们去 去赞助的 所以他们的这个经费有限

经费有限 就是能去 录取的同学们也有限 然后我当时就被小野肯教授 扔到了这个waitlist候补名单上 然后他给我发了一个邮件 他说我在候补名单上的名次比较靠前 然后我当时感到非常的激动 因为 当时我身边的朋友们 我刚才讲的这一些大神们 他们都已经被录取了 他们在同一天已经收到了录取函 我看到了一个邮件

说我在居然能够到这个候补名单上 我居然还能够在候补名单上 名次比较靠前 然后我当时就觉得哎 我可能还是想去做数学研究 因为我觉得我如果这个暑假不去 下一个暑假可能就不要我了 我可能连这个候补名单上 我也上不去了 所以我就 最后居然被捞上来了 因为可能疫情吧 可能好多同学他们就暑假不想在

一个数学夏令营 他可能还是想 比如说就是在家里可能隔离啊之类的 所以拒绝他的人那一年比较多 我就被捞上去了 我被捞上去之后我就没有去桥水 我最后是结束了 大学结束的时候 那个暑假去了 去了桥水 你们家里有刻意的引导 你在数学上的发展吗 啊 我觉得有 我觉得我妈妈她有一个这个危机意识

她小时候数学特别不好 然后她 是吗 对 你们家大人有数学基因吗 没有 就是彻底没有 她数学特别不好 她数学就是她其他可能都好 她就是数学不好 她就觉得说 你要不就是先就是学一学数学 因为可能到后面 你数学会是你学科里面 比较落后的一个 她是觉得你可以就是笨鸟先飞一下

你的青少年时期获得了特别多荣誉 这个非常的长 我就不念了 我们到时候可以给大家打出来 小朋友时候的事情了 对 只是小朋友时候的事情 那这些对你来说是轻而易举获得的吗 我们刚才聊天 听见好像都不是 你当时的目标 对不对 啊 它 可能考试前两三个月成为了我的目标 对 我觉得我还是比较

喜欢去做一些有创造性的事情 比如说 我记得当时大部分的时间 确实花在了就是对于数学自己的探索上 嗯 然后你说这些目标 它其实跟这个也有很大的关系 嗯 对 它反正都是数学 它只是类型不一样 你可能说准备奥赛 我也有准备奥赛的时候 我准备奥赛

就是在好像是很短的一段时间里面 就刷了75套卷子 然后就是就是 当时它其实是一个纸的那个杂志 然后就一页一页的 每一天就是做一页 然后做完把它撕掉 然后就是 75 套卷子 75 套卷子做完之后没选上 去打那个比赛 我觉得我的这个 所以一直对荣誉这个事情 我的感受非常复杂 因为我确实在每一个时期 都觉得是

自己是那个环境里面最愚蠢的那一个 最怎么样努力都看不到结果的那一个 然后最绝望 某种程度上就是对它 不是一个在舒适区 持续的不在舒适区 是一个非常 我觉得是对人很有 就是塑造的一个体验 就是 失败 是你的默认项

你是在持续的不在舒适区 对自己的要求比较高 你就会觉得什么都是失败 但是你又很乐观 对 就你没有因为失败很痛苦 没有 就是你 我觉得是 可能是因为你很乐观 所以你经常失败 你每一次就很乐观 觉得自己能够到达一个 希望能够去成就一件事情 然后失败 某种程度上其实自我定义的 并不是说客观定义的

可能客观看来不是 不是失败 你能描述一下你的一个失败的体验 内心的体验 它是有一个外在 什么事情触发你内在的体验 就是麻省理工的第一个学期 它有一个叫做成绩保护 成绩保护 就是所有的这些新生的同学们 他们都可以 就是上任何你想上的课 然后你不需要去担心你的成绩 不是一个A

因为这个GPA变得非常的重要 嗯 我身边有两类同学 我当时住在这个 麻省理工的一个 很有特色的一个宿舍楼 我们这个宿舍叫做东校区 东校区的这个 如果你走到东校区的这个庭院里面 会看到那种木头做的过山车 两个树之间有绳索 然后有一群人在玩喷火

就是这是一个非常 麻省理工精神的一个黑客的一种 一种非常nerdy的这样的一个文化 大家就是我 我反正我当时住在这里 就觉得非常有意思 然后我在整个东校区的这种环境下 我在西边楼的三楼 这个three west 这个叫floor pie floor pie就是因为它是三楼 所以呃大家叫把它叫做pie楼

就是圆周率楼 然后这个楼上住的全是IMO 就是这个楼上 呃不是IMO 就是IPHO 物理的 或者是IOI 就是信息奥赛 姚远住在这个楼上 这是美国的一个奥赛选手 然后中国台湾的 于洪勋住在 这个楼上 我们整个楼每一个人都是我的偶像 然后 所以他们就给了我一个建议

就是说 你就是去上最难的课 然后你就是去上 你可能都 没有这个预备知识的这个课 然后我就真的去上了这个课 因为我身边的当时玩的比较好的同学 可能都非常的有这个乐观精神 他们可能也从这样的学长学姐这里 听到了一样的建议 所以我们有好几个 这个大一的这个小朋友

去上了这个博士概率论 博士概率论 我们想 唉 概率论嘛 这个我们知道概率论是什么 我们就开始在想一些 可能让我们算一些可能比较复杂的 不会算的 概率不对 第一天开始上来测度论 测度论从这个 从Borel Sigma Algebra开始讲起 从这个测度论背后的代数 一个叫Borel的一个代数开始

开始讲起 我们就是面面相觑 我们 我们完全不知道这个发生了什么 然后这 其实 我觉得是一个很有意思的一个体验 因为它不是一个竞赛环境下 我自己一个人考砸了的 这种失败 就是有好几个这个同学们 大家一块去啊 去感叹一个事情很难 然后在一个在解题小组里面 我们一块去尝试

就是群策群力去把这个题集 MIT特别倡导合作 就把这个题集做出来 然后这个过程 我觉得特别特别有意思 所以你这次 就是你的不舒适感 是来自于你选了一个更难的东西 对 然后这个 这个考试 好像是满分试卷是40分 然后期中考 整个班的平均分 就连带着 我不知道是混进来了多少我们这种

吃了雄心豹子胆要上这个课的本科生 平均分好像只有9分 哦 就是平均分只有9分 然后我们 我们的分数都是5以下的个位数 我们这几个大一的小孩 所以 我们肯定是拖这个平均分后腿的 这个主力军 那你的失败体验来来自于哪里 来自于 我从来没有在一个考试上看到自己 一个40分的考试我能拿4分 4分 哈哈 对

但是你知道 这是因为我选择了更难的事情 我觉得它也不会触发你自己 觉得自己很失败的这个机制 对对对 我什么失败都不会触发 我自己觉得很失败的机制 就是我 我把这个失败 当做是我的这个default默认项 嗯 对 所以我就 我就开始说 那我要学分析 这个课我学不好的原因 就是因为我的分析的底子不好 于是我就开始很认真的

去重新把我可能14 15岁学过的 Walter Rudin的 实分析 我又再学一遍 嗯 那你的自我奖励的机制是什么呀 你在追求什么呢 你在那个时候 这是你选自己选择的一些选项 我自我奖励的机制 其实这是这是一个很好问题 其实它有很多重机制 我觉得我有 嗯 我在就是年纪比较小的时候 这种社区感

或者说 我有这个朋友 或者说我有战友们 这个大家有这种 camaraderie（战友情谊）的这种友情 一块去做某一件难事情 MIT它特别倡导 就是呃 攀登 就是登山队 呃 这个 这个会给我很大的 一个奖励的感受 就是我们没有放弃 就是我们期中考完了之后 我们大家一块说

就要么就一块drop the class 就是都把这个课给退了 要么就一块继续做 反正就是也有这个保护机制了 第一学期 然后我们大家就决定 一起继续上这个课 就这个事情 我年纪比较小的时候 这种奖励的这种感受其实来源于 这个社区 或者说是小团队 小团队 然后 呃 我不知道是为什么

反正近几年是不来源于人了 呃 近几年来源于 就是可能这个非常难的这个事情 本身就是近几年 可能我觉得是年龄小的时候 承受能力 虽然说仍然说是 就是经历了很多失败 但你自己感觉到麻木 对吧 仍然没有这种失败的感受 但是在 近几年

可能真的是对这个东西完全没有 负面的感受 所以 就是这个难的事情本身 我有种对pain and suffering 这个黄仁勋老师讲的这个 有更多的这种suffering 我反而对这件事情有点上瘾 为什么 我觉得大部分我知道的就是 嗯 founder就是创业公司的创始人 他们都对

就是苦难上瘾 嗯就是对 苦难上瘾 嗯对 就是其实这是一个不一定很健康 就是甚至就是有一个有意思的 我听一些风险投资人他们说 他们找这个founder 就要找这种对疼痛上瘾的founder 我听起来 这个感觉非常的 不可理喻 对 呃 就是他们有一句话叫做chip on the shoulder

chips in the pocket 就是说我感觉我的肩膀上有一些重量 可能是我以前的一些伤痕 这个chip就是在这个肩膀上的 这个chip 能够转化成口袋里的chips chips就是硬币 就是钱 就是 可能说某种程度上 对于疼痛的上瘾 从这些 当然从这些风险投资人的角度上来说

能够转化成一个 呃 小创业公司的成功 嗯 这是一个我觉得比较激进的一个理 理论 但是某种程度上 它有一定的一定的正确性在里面 嗯 你从小团队的这种奖励机制 到这种事情的奖励机制 这个分界线画在哪 疫情 麻省理工 你没有团队了 就是MIT毕业了以后 不是不是

我大一的时候 下学期就疫情隔离了 OK 所以等会 你零几年 我是 我01年 哦 对我01年 还没有到25 24岁 对 然后我24 特别好一个数 你看我 24点 哈哈哈 对 然后 嗯 就是 对对对 当时就是 就是大一下学期 所有人就就赶走了呀 就不在学校 就是 呃

off campus了 然后所以就没有小团队了 那课还得上 对吧 那你必须要去学会从这个事情 难的事情本身里面 去找快乐的感受 嗯 所以我当时觉得 学习曲线是非常陡的 它对我 MIT对我性格 真的是有很大的一个塑造 我觉得就是每一个 呃 我遇到的在麻省理工的同学 他们都特别能吃苦

他们会在雨天暴风雪里面去跑 晨跑 就是我 前段时间我上周末还去了波士顿一趟 就看到又是一个下雪天 Blizzard那个暴雪风暴红色警报 他们还在跑步 这是一个非常有毅力的一个学校 然后这种毅力它是非常有感染性的 它让我 呃 终身可能无法达到 MIT希望我们能达到的 那种毅力的程度

但我会希望往那个方向努力 嗯 就是什么难做 做什么 什么痛苦 做什么 什么长期主义 做什么 然后 对 还有一个 我觉得就是刚才讲到小团体这件事情 就是 啊 它也就是训练了 就是说在压力来临的时候 其实对 任何的人际关系 都会有一个比较大的挑战

就是可能说是 啊 有一些 呃 呃 一对一的这些人 人际关系 也可能是一个团体的这个人际关系 保持自己韧性 和就是自己的内心的 这种坚持和能够去影响 或者说是不一定说是影响吧 去促进一个团队 他们都有这种感受 其实我觉得 这是一个非常非常

非常困难的一个技能 然后这种技能我记得当时就是 巴菲特 查理芒格他们就有在一个访谈中讲到 说如果你看到这样的一个人 一定要把他就是 就是招进你的这个组织里 它的信号是什么 它的标志是什么呀 标志是一个 呃 自己内核很坚持 很技术派的一个人 同时能够有 啊

领导力 但是领导力这是一个非常满的一个词 就是leadership 在美国的语境下 我觉得和中文的语境下 它有一定的区别啊 我还是觉得 就是你 千万 如果你想 就是 领导力里面 领导两个词 你就没有办法有领导力 就是一定 就是服务型跟随型 哦 对 就是最好的领导力可能是服务 最好的领导力就是别人

就整个团队在登山的时候啊 你不是前面那个拿着喇叭的那个 你是就是后面递水的那个 嗯 我觉得 你刚才说不想打零和游戏 嗯 那你觉得你当时打的是一场什么游戏 当时就是 如果我去学高等数学的话 我就可以 就是啊 有种就是你 你感觉有浩如烟海的

不是你已经知道的这一些 数学的这些概念 它其实这是一个很有意思的点 就是 我在数学的竞赛中 我是有一个 就是Syllabus 就是有一个考试要领 可能说每一年就是都 是这些考点 然后在高等数学里面 我只要去新引入一个定义 新引入一个概念

我可以基于这个概念 与以前的这些概念 去发散出新的这种定理和问题 然后这个某种程度上看着像搭积木 就是其实有一篇就是 AI for Math的一篇文章 叫做Lego-prover 就是说像乐高积木一样 就是你可以往上搭一个 搭一个自己的小宇宙 这个过程是非常快乐的

这个过程是不受竞争所限制 那不受竞争 你就是在跟 就是你可以在历史上的这一些 站在巨人的肩膀上 去探索一些事情 嗯 对 你为什么高中毕业去美国读本科 而没有去 比如说清华北大这样 呃我 我是非常确定 我是希望能够出国 我挺喜欢麻省理工的 就我可能也确实看了一些电影

我在草稿纸上写MIT 我可能不一定是想出国 我可能想来MIT 为什么 噢 那个是段子 是真的是吧 就那个是真的 我就在在稿纸上写这个MIT 对对 如果说我想去另外一个学校 比如想去哥伦比亚大学 Columbia可能要写的比较长 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的数学的同学们 是啊 去竞争有限的名额的 就是其实某种程度上 你们每一个人有自己喜欢的数学 你们喜欢的数学 和别人喜欢的数学不太一样 你们就是 如果你喜欢这个领域的 我就介绍你去 这个教授 这个世界非常大 就它变成了一个无限的游戏了 在大学期间

它没有那么的竞赛和竞争了 对 然后我的教授们 他们是非常非常好的人 就是我 我印象中当时有说 当时就是疫情 就是中美之间 就是停飞了 就是没有航班啊 后来就是赶紧 就是有航班的时候就想飞 然后那个时候要写一些信啊 给这个就是 就是说这个人可以回来 我们的教授都是非常好的

他们对每一个他们的这个mentee 他们的这个辅导的同学 都非常的好 非常的照顾 嗯 比如说 这个北美数学本科生最高荣誉摩根奖 是怎么拿到的 我跟你讲 我觉得就是有我的教授 他去提名我 然后有另外的一些教授 包括Professor ken Ono 他们有写推荐信 嗯对 然后接接下来其实就是评审委员 委员会的

评审委员会的这个 这个决定 30年摩根奖的历史 每年说虽然有一个人拿到 然后有大概两三个人 是 就是 亚军和季军 呃 这些亚军和季军 和拿到的这个人的数学水平 没有什么差别 然后 可能还有很多没有被recognize到的同学 他们都非常的好 就是在我们的当时的那一个圈子里面

我并不觉得我是数学最好的那一个人 就我觉得 某种程度上 呃就是 但有那么一波大家觉得就是 可能研究还做的不错的本科同学 其实谁拿到谁拿不到 就是这个 这个事情的随机性是很大了的 对 理解了 嗯你在本科期间 在数学上有哪些新的探索 你感觉你喜欢什么 对 我当时喜欢 还是喜欢数论

然后当时可能有就是一个抉择 就是哪种味道的数论 是做更代数数论 还是做更解析数论 这个中间有有一些 就是决定 我印象中当时还是做了很多的 就是模形式 对 然后做了一些椭圆曲线这一些的工作 是在Professor Ken Ono的这个 我多于一半的文章 其实Professor Ken Ono在他的呃

就是这个夏令营的里面的合作者 我们一块去 去写的 对 嗯 然后硕士去了牛津 硕士去了牛津 为什么学了神经科学 没有继续沿着数学的路深造 当时姐进动不动往数学系跑啊 就是数学系 也离我们那个学院也比较不太远 对 就走10分钟 然后呃 神经科学那边是

我其实当时 出了一件事情 就我可能非常想知道 就是人脑是怎么样的一个一个构造 就是当时家里有一些事情 就是我可能想 对啊我当时爷爷有一些 我当时想对大脑有一有有更深的理解 对 然后 嗯 到了那里发现 你如果要对人脑有深的理解 你需要做实验 呃 我之前做过果蝇的实验 果蝇的实验是非常简单的

你就是把它这个头盖骨一翘 然后你就拿一个管子进去 然后你就看它的这个Neuro Dynamic 这是果蝇 这是一只一只小果蝇 但是到牛津的时候 你要考一个就是license 一个证你才能去做很多的动物实验 就考这个证的时候 需要你去杀一只老鼠 我当时就是 我做完了那一次实验之后 我当时就是我要走计算神经科学

我不要去做动物实验 在英国就是 其实计算神经科学和AI 他们的这个关系非常的紧密 在有一个UCL的Gatsby Institute里面 他是原来的DeepMind的Demis Hassabis 在那里做 他的postdoc 博后的工作 然后在这个之前 Jeffrey Hinton 其实是AI教父吧 他是founder

founde了这个Gatsby Institute 这个Gatsby Institute它叫做盖茨比中心 它叫做计算神经科学中心 computational neuroscience 但它实际上其实就是 大部分都是AI的faculty 然后我跟就是Andrew Sachs教授 然后包括Andrew Sachs 他的一个collaborator 其实就在Stanford 叫Sheridan Gully 我们当时有做一些研究 然后还有 Tim Berners然后Will Dorrell James Whitenton

就是有很多非常杰出的又懂数学 又懂AI又懂一些神经科学的研究者 然后我当时是一个硕士的一个 一个同学 当时我反正我记得 我见到他们中的任何一个人 我当时就觉得非常的激动 我就觉得我 我感觉这个人好像能带我做做研究 然后觉得这是一个非常好的机会 所以你是被AI点燃

你不是被神经科学点燃了 最后 我最后 就我的 我的那个快乐来自于来自于AI 不来自于神经科学 然后还当时还就是要写那个硕士论文 嗯就是这一些 我刚才讲的这些研究员们 他们要一起来协助我 把它写成一个更神经科学的 一个毕业论文 因为 就全是AI 后来怎么写的 写了个啥 呃 就是 我是有 其实有找到说

比如有一篇 其实就是continue learning的一篇 嗯 去看这个neural dynamics（神经动力学） 然后另外的一篇是就是去看一个假设 一个 one-layer linear Transformer（单层线性Transformer） 这个理论是理论 机器学习能做的事情非常有限 在这样的情况下 你也找不出 你也没有办法做 exact neural dynamics（精确神经动力学） 你就可以去 但当然记 我印象中非常大量的线性代数 非常大量的矩阵运算

就是在出现在然后前面那一篇 大量的这种就是ODE 其实都是非常基础的数学 应用在这一些呃可以有 嗯 有AI与 认知科学背景的背景的这些项目上 那你博士为什么又去读 数学和法学 在Stanford 噢 我博士 这个数学 我是本来本科的时候就是defer（延期）了 所以就是本来就知道自己要回去 哦回去读

所以我啊 我当时是本来打算 可能本科之后直接去读数学博士 就是没有去经过这个 牛津这一层 为什么牛津去了呢 因为罗德奖学金 我觉得是一个非常好的一个机会 OK 我有另外一层 就我从小喜欢打辩论 所以我觉得在就是牛津的这个呃 呃 有这个Oxford union 它有一些训练你

去成为一个更好辩手的一些活动 然后包括是后面到法学院去做 呃 就是呃 litigation 诉讼相关的 我不是我不是并购那一边的 我是诉讼那一边的 就是 呃 暑假实习之类的 其实都是因为由于这个辩论的这个 呃 很小的时候开始辩论的热情 嗯 所以你其实整个的发展非常的综合 能这么说 对吗

可但我差的也是实在是差 就是综合 一般意味着是没有短板 就是我还是有很多短板 你差的是什么 短板是什么我 很多事情我都就是做的不太好 比如说我 我印象中当时地理是非常糟糕 我到现在啊 没有任何的方向感 我就是 我觉得我是一个比较spiky（不均衡的） 又就是不太好的

就是不太会的东西 也非常spiky（不均衡的）的一个人 我是一个hybrid（混合）的一个人 哦 哎 那经过了数学物理神经科学AI 包括法学这多重学科 你站在这个交叉路口 你看到了什么呢 就在你可能在站在博士的那个时候 对 呃 当时看到了 就是几件事情 第一件事情 就是我当时对宪法非常感兴趣 然后我当时就是宪法里面

它分几种宪法 去诠释美国宪法的这个方式 呃 比如说originalism 原点主义 就是说所有宪法 现在我们看到的是基于（美国）国父们 就是建国的那一些人 他们的原旨原意来 应该来这样诠释宪法 这是第一种 然后第二种就是叫做textualism

就是说宪法写的这个英语字是什么 你就把它读成什么 你不要去想他们原来可能想的是什么 呃 你就是去 一字一句的去解读 去看到一个定义 特别像一个数学家可能会去 会去做的一个诠释 第三个呃叫living constitutionalism 或者叫policy consideration 就是说这个宪法 它会呼吸 它会与时代一起成长

原来的宪法是这样写的 我们应该把它看到21世纪 去怎么样去解读它 就是然后在我在法学院 就对这些东西非常感兴趣 我是一个 呃 非常 呃 我是一个textualism（文本主义） 就是我是一个 按照他是什么样就是什么样的 这是我的 我的司法哲学（judicial philosophy） 呃 指的是philosophy 然后当时他们就有人说 如果你想去了解这个到底是什么意思

因为我们不知道这些词是什么意思 可以去拿一个 就是LLM（大语言模型）去 去 给他一些 就是一些data 让它这些data可以包括什么在里面 也值得商榷 可以包括这些建国文献 也可以就是包括现在的一些呃 一些一些 一些新的当代的一些 一些政治与哲学的

一些著作 然后我当时就有一个想法 就是 如果我们已经到了一个能拿AI去看 这个宪法是什么意思的 这样的一个时代了 我为什么不能拿AI做数学 我当时就在课上我在想这件事情 我就觉得AI应该可以做数学 然后我就想到一件事情 就我最好的一个朋友之一 就是啊 他叫Kenny罗

他是 帝国理工 Imperial college（帝国理工学院） 他交换到MIT（麻省理工学院） 我们大一就认识 然后我们一块上了很多的课 我们是非常好的朋友 然后他还教会我怎么下这个象棋 他是这个象棋的这个大师 然后他就是告诉我 从 2020 年开始 告诉我他在做Lean 他在做形式化证明 他是最开始Lean里面什么都没有的

嗯就是Mathlib（Lean的核心数学库） 是一个空空如也的一个library 他把他里面所有的本科的代数 本科的分析 去把它一行行的把它打出来 做基础的 这个建设的那5-7个学生之一 是Kevin Buzzer的学生 所以他就我 就我当时我就在想一件事情 就是说AI如果能去做法律

是去看比较structure的东西 就是这个东西到底是是什么意思 而是研究的是比较specification这一块 而不是比如说让你去拿AI去判一个 这个人到底有没有杀了另外一个人 一个普通的trial court 一个case 而是去看这个constitutional law 比较就是precisely define 比较严谨 去定义的这个

那我需要数学不是英语 而是一个更结构性的一种一种呈现 而这个Lean这个形式化语言 它就把数学变成了一个代码 所以他就可能能够去 我当时就有一些这样的一个想法 然后当时同时和Shubho Sengupta（曾任Meta AI研究总监，现在是Axiom CTO） 我们在一个叫做Verve的一个咖啡店 我们一开始认识的 然后接下来 我记得在Palo Alto 在Palo Alto

对就是啊 Verve咖啡 现在墙上还有 我们两个 当时就是照了一张拍立得相片 他当时说你买了 一共买了1,000杯咖啡 你就可以照一张拍立得 我和Shubho在那一定买过1,000杯咖啡 哦对 我们给这个咖啡店 就是带来了非常多的 这个营收 哈哈 我们现在整个办公室的每一个人 他们每一天都在这个咖啡店 嗯 然后Shubho Sengupta（现Axiom CTO） 对对

然后我们当时也一直在聊这件事情 就是陶哲轩老师有很很多的 不管是播客 还是就是写的博客啊 就讲这个形式化证明 然后我身边的就是Kenny 他 我知道他有多对这个Lean进行狂热 他现在也在Axiom全职 所以就是好多好朋友们 大家现在就慢慢的聚到了一起 就是希望能能做这件事情

我当时看到的一个事情就是 一切我们认为的不可能都有可能 然后如果是这样的话 对我个人意义最大的 就是 让AI能够帮助我进行一些数学证明 尤其我不是天赋型选手 我有些时候真的是花 某种程度上 你说AI能够帮助最大的是谁 是那些蛮力型数学家

就我 可能真的就是 我要枚举多少个可能性 我要经历呃多少天去验证一个非常 可能是一个standard argument 一个标准的一种 一种证明方式 我按要按照那个比对 我记得当时呃就有一个一个事情 就是Ben Green老师有一篇文章 叫"Shiu's Theorem for Shifted Primes"（关于平移素数的施定理）

他讲的就是说我有一个集合 我要保证这个里面的集合的a和b 两个元素 中间的这个差值 就是a减b 它不是p加一或p减一 p是一个素数 然后我能够就是 从1到n中数出多少个这样的 一个多大的一个集合 然后我当时就我看到那篇文章 我想这个东西能够被证明

多少的数学问题 就同样的这一套machinery（方法/工具） 就是Ben Green老师的这一套 这一套发明或者是发现 你可以把它去做function field 你可以把它去做呃 当然说做shifted sum of two squares（平移的两平方和） 没有特别大的意义 可以做x² + y² ± 1 这个没有特别大的 不知道有没有特别大的意义 反正就是这一套的东西是工具 是可以用来做很多的事情的

AI应该把它完全解决 AI应该能够达到一个 一个很熟练运用所有Davenport里面 数论的呃 工具与技巧的一个博士生的程度 我当时觉得这一件事 这个事情一定能做 然后我就开始想怎么能做这件事情 就要算力 这要我要想我有多少 这是哪一年 二零二四 二零二四年 就是你 跟书包频繁的进入咖啡

出入咖啡馆的那一年 对 是2024年 OK 2020 2023年9月份 到2025年的12月份 去年12月份 啊 不 2024年的12月份 OK 对 就差不多 因为我当时还在 我第一年 其实我大部分的时间就是呃 我在作为一个法学生的时候 I had a lot of fun就是我

我每一天就是感觉特别的特别的神奇 我从来没有任何的作业 是让我去阅读的 阅读这30页 这就是你的作业 我的本科是一个工程学校 MIT是一个理工科学校 我不是一个文理 我没有接受过一个liberal Arts的education 哦 嗯 所以我就非常非常希望能够多读点书 然后我还想练练英文写作 我当时觉得我都可以去

所以我那一年就是 但是就是第一次吧 可能科学数学它不在你的生活之中 就有点想念 然后就是我想念的时候 我就跑到那个咖啡馆去 我坐那个校巴 当时没有钱 当时是特别 就是一穷二白 打不起Uber 然后从斯坦福 坐8分钟的 你要走20分钟 应该不远

你走 20 分钟到这个大草坪 你到了大草坪就可以坐个校巴 坐校巴8到9分钟 你就到了这个火车站 火车站穿越一个隧道里面 有一些流浪汉住在这个隧道里面 你就可以到这一个Verve的咖啡馆 Shubho就在那 你就可以去跟他聊这个科技与科学 哦 他那当时 已经在Meta上班了 他一直都在 他是在Meta 89年的一个Meta的一个元老

他是Meta的Facebook AI research的director 就是他当时跟 当时跟田源栋老师差不多时候进去的 就是可能还比田源栋老师早一些 那你们怎么成为朋友呀 我也不知道他是谁 他也不知道我是谁 那你怎么认识的呢 我们就在这个咖啡馆的这个桌子 就是我一开始到那写作业 我一开始到那 就是我有30页的阅读 每堂课有30页的阅读

我就抱着这个这么大的这个法律书 我就抱着这三个法律书 我就去 其实挺就是非常 不明智的一个选择 你有那么厚的书 你抱着它们去坐校巴 但当时就是 那你为什么一定要去那里去做作业 在Palo Alto downtown 就是我 可能我们这个法学院的图书馆 就是一般周一到周五待的有点闷

我说实话 它有地毯 然后有点密不透风 就环境 你周末你就是想放松一下心情 对 然后我记得这个Verve咖啡馆的一个点 它那个庭院有很多狗 然后它只有周末有狗 就是它周内的时候 那些狗的主人 可能没有时间带他们遛狗 我当时一开始去那里的motivation 就我可以读书 我可以喝这个

我会点一杯抹茶 然后我就可以看狗 这是我的一个我的快乐 就是读法律案例 做笔记 看狗 喝抹茶 然后这时间一多 就总是我 发现就有这么一个 每一次看的感觉非常面熟的一个人 然后我们就开始聊起来了 噢 是在里面 还是外面 因为它有里面一个区 有外面一个区 在里面啊 对 有可能共同坐在一个长桌上

对 一个6个人的桌子 对 然后唯一的一个6人桌 这个6个人的桌子里面 其他的人也永远都在那里 噢 对 噢 成了一个常客 对 谁开始先聊天的 应该是一个 就是没人打算聊天 好像是他坐在窗边 然后那个太阳特别晒 然后我需要那个窗帘拉起来 这么说上话 哦 然后呢 然后接着这个对话是 怎么

我就非常谢谢你 帮拉这个窗帘 然后他就说我经常看到你 然后我就说是 我也经常看到你 然后一个谈话就开始了 嗯 那怎么聊的数学的呢 发现他有 他学过数学 他的本科是数学 他的硕士也是数学 然后 他后面好像还读了两个数学的硕士 我印象记得不是特别清 反正就是 然后我的那个

就是他就很好奇 他觉得我应该是个法律学生 因为我有这个书 然后我们就聊这个 我当时可能我不知道 我在看哪一块呢 我反正就讲这个 这个案例就是非常的离奇 然后就 反正两个人就开始做朋友吧 就是我觉得 还感觉这个21世纪 就是有很多事情都是在互联网上 大家不太到一个咖啡馆 咖啡馆去聊天了

嗯 你们都聊了多久 我们聊了 就是我们一两年 我们是朋友 我们不知道对方在哪 但他不知道你是Stanford的学生 他知道我是Stanford的学生 但他不知道 他可能知道我是 法学院 数学 但他不知道我 他可能不知道我 有一个数学研究背景 就是他可能 他好像听说过摩根奖 他听说摩根奖 可能是因为

有很多摩根奖的同学转入了AI 比如说Levent (Levent Alpoge) 和Honorable Mention的Greg Yang是xAI联合创始人 和Honorable Mention的Greg Yang是xAI联合创始人 然后 呃 他不知道 我也不是个什么人物 他不知道也没关系 但是我是真不知道他是一个 这么厉害的一个人物 你知道他在Meta吗 他现在就是 你知道他在Meta吗 我当时不知道 我一直不知道他在Meta 后来你们是怎么开始决定要创业的呢

就是在你们这种漫无目的的认识 漫无目的的认识和聊天 对 对 我有一天 你们这种谈话持续了多久 持续了一年半 聊什么呢 这一年半 聊科学历史 哦 对 然后就有一天 我印象是秋天 2024年的秋天

那个时候我刚开始数学的PhD 但我当时很多的时间 其实在给XTX去做一些工作 就是XTX是一个 呃 一个量化金融的 我暑假就是 后半段在在那里 然后我 我当时就觉得 我在那里 就是觉得天呐 这个AI更有更有意思 就是你XTX有卡呀

对吧 它有卡 所以你能做的事情 就比你在盖茨比做的事情多很多 所以就当时觉得AI很有意思 然后回来 然后有一天 我是去跑步 我就是晨跑 然后跑完之后我不知道为什么 我就觉得 好像这个事情真的要 真的要发生 然后我就去找Shubho 我说 这个事情大概

如果我想融资要融多少钱呢 然后我们两个人在那算 我们算就是多少张卡 也在Verve 就在Verve 拿了张餐巾纸在那算 然后我们就说 好像这个事情还是得做一个创业公司 就是没有可能在学界去做 那我那一个学期在做XTX 我疯狂的往CS的那里跑 有一个CS 斯坦福 CS我觉得最好的一门课是一个叫做 就是first year PhD seminar

每一个教授为了就是招新的学生 他们就会去讲他的这个research highlight 你每一周去 就一个学分 你每周三下午去 下午5点 然后你可以认识 你所有其他的一些计算机系的同学们 我就坐在后排听 我是个数学系的 然后完了之后你就可以知道 我的天呐 就是有这么多 就是做机器人的 他们在做什么 做这个 computer vision的在做什么

反正就是非常it's an intellectual feast（这是一场知识的盛宴） 你是在哪一刻决定辍学要创业的啊 其实我大概知道 我开始融资的时候 我就知道 我总有一天要辍学 你先开始融资才辍学的 你是先开始融资再辍学 我先开始融资再辍学 因为这个我不能辍学 因为我辍学了我没有身份 我要拿到我的这个身份工作签证 我才能够辍学 所以我拿到 了我的工作签证 我就辍学了 因为就是

一般来说投资人也期待你辍学 就是你很难说是同时 硅谷 一般拿到融资就是开始要 甚至有些时候辍学 是融资的closing condition（交易完成的先决条件） OK 为什么不是Shubho当CEO 是你当CEO Shubho当时其实还在 一开始大部分的时间他还在Meta 他没有 他不是第一年决定 他不是第一年加入的 因为我们当时谁都不知道

这个事情能否得到这个投资人的支持 嗯 这个事情是 想不明白的 所以从 哪个月份决定的 我从9月份就决定了 但我不到11月 我没有融资 因为我一直在劝自己不要做这件事情 为什么 我不太喜欢 就是我 当然 我觉得中国语境下的创业者是一种 就是气质 但美国语境下

现在就整个valley都是founder 就创业者某种程度上辍学创业 他就是浮躁 我其实觉得 如果我是一个本科生 我绝对不会去辍学 然后去Y Combinator（美国创业孵化器） 我某种程度上 我觉得我是最不可能创业的一个创业者 我非常的喜欢向往学界 我非常的希望 能够去做更多的数学的一些探索 我非常喜欢在大学的一个环境

所以我就两个月是在劝退自己 但是每天早上还在跑步 然后 跑步的时候想事情想的非常清楚 到后面是非常非常确定 但我当时非常非常确定的时候 马上就感恩节了 从感恩节到圣诞节的时候 没有VC上班 所以你要么就是那个时候到感恩节融完 只有10天 要么你就来年再融 所以我当时就来年再融

哦 那两个月 最后你是怎么经过了怎么样的CoT（思维链） 然后决定一定要做 我当时去读了这个科学史 哦 读了科学史 真的读了科学史 创业读科学史 就是多少个 先是从维基百科开始读科学史 后面要找书读科学史 然后有一个叫AI for Math 的 GitHub repo 嗯

这个GitHub repo里面大概有几百篇文章 每一篇文章的abstract我都读过 然后有意思的abstract 我就会把整篇文章看完 然后我就做了多少次费曼的过程 在就是纸上去想 如果说我这个东西要搭起来 应该技术上怎么做 我不可能说 我自己觉得这个事情不会成功 然后去骗别人的钱 这个事情我觉得做不到 所以我当时就到了一个程度 我发现

我觉得它不一定是一个研究问题 它是一个工程问题 它这个东西的科技的风险 就没有我一开始看上去的那么高 然后在这样的一个情况下 我觉得是负责任的 去做这个创业 开始融资嗯 所以你是在自我验证 这个过程是在 我觉得就是某种程度上

你如果去 就是吸引一些风险投资 你需要自己 一定要对这件事情比较确定 比较了解 不然我觉得不太负责任 但你质疑自己的点 可能是说会不会我 啊 这是一种浮躁 这是一种跟风 一个是AI已经火 是不是浮躁跟风 这个我倒知道

我特别反对做一个AI founder 所以我知道我绝对不是浮躁 反对做一个AI founder是为什么 就是我 因为我在MIT 在MIT就是有创业社 然后我的好朋友们 一起去打那个Jane Street的那个 就是量化金融比赛 黑客 Hackathon的这些同学们 他们是创业社的社长 我当时就两个队友

他们两个就是这个创业社的社长 叫我去活动 说有这个free Sushi免费的寿司 我也不去 我觉得我觉得创业不好 它不是一件好事情 我觉得还是要做教授 这个有点不务正业 是不是 对 然后我觉得就是 总觉得 比如说一个以非常产品为导向的 这样的一个创业项目 感觉像是昙花一现 我当时也有这样的一个感受 然后我希望做的事情是非常长时间的

非常难的 所以我觉得 一般和一个创业的 一个这种风险投资的 一个周期 可能不一定吻合 所以我 我知道我不是浮躁跟风的那一批 然后 嗯 我当时还有在想 就是我有没有什么别的办法 能够做这个 AI for数学 然后我当时还尝试去 我要不加入一下 别的做AI for数学的公司 然后就在这个Verve的咖啡馆

这个我们现在的主要的竞争者 这个公司的CEO Tutor(Tudor Achim) 他也是常客 于是我有一天还就见到了Tutor(Tudor Achim) 然后我就说 你们招人吗 然后我当时真的是想 就是我是想做这件事情 要是我能跟别人一块做 我也不用自己去从0到1 就感觉太复杂了 然后 这是主要的质疑点 其实不是一个感性的

我是不是浮躁 我是不是跟风 就是我到底会不会这些东西 然后我就去研究这个AI for Math 真的当时就是看paper 然后这个过程也非常的快乐 就是非常非常的快乐 非常快速的去学习 一些主要的一些idea 从比如说2018年一篇文章叫ATPboost 在没有AI的情况下 去做这个形式化的这个定理证明 然后我看到Bartosz Piotrowski

一个波兰人 是这个作者 我们现在Bartosz Piotrowski 也就在Axiom 然后我当时有另外的一篇文章 叫 Pattern Boost 就是从 很多的数据中去找里面的这个pattern（规律） 找这个规律的 一个去从很多的图中去构造新的图 为数学家去找例子和反例的pattern recognition

当时看François Charton是这个作者 现在François Charton 也在Axiom 然后 我当时看另外一篇AI for Math的文章 叫End-to-End 然后这个是拿这个 一种transitive的翻译的一种方法 从问题能够翻译到解法 问题能够翻译到解法 如果看到了很多这样的例子 下一次来到一个问题的时候 是否能够直接翻译成解法 也是 做数学发现 而不是数学证明

这一个 这一个文献里面的Alberto Alfarano 他现在也在Axiom 是所有 这个美丽的过程就是我 所有这 当时我作为一个学徒 去看这些巨人的肩膀 这些文章 他们现在都聚起来 都在Axiom 这是一个非常 我觉得神奇 做创业者 我觉得其实这是最最高兴的一个过程 你又形成了你那个小团体 对对

你去问你那个竞争对手 能不能加入你们公司 有没有机会 他怎么说 他说你是 你是什么的PhD 我说我是数学的PhD 他说噢 我们只招计算机的PhD 噢 为什么 AI for Math 为什么呢 我不知道 他当时就是这么说的 但是你们团队很多是math 我们团队 呃 这么有趣 我们团队有三块

我们团队有非常多AI的人 就是强化学习agents 就是applied AI（应用 AI）的这一些人 我们有很多的做代码生成的人 就是programming language（编程语言） 然后 很多是compiler编译器的人 比如说LLM compiler 那个主要团队在我们这 然后他们很多其他的工作 compiler Arena 就是所有的这些compiler

就是深度学习 去帮助compiler 就是代码生成的这样的一群人 然后他们当时也是 Yann LeCun那个CodeWorld model 32 billion 那个模型的后面的 里面的一部分团队 然后都在我们这儿 然后有一群是数学 这数学里面比较tricky 数学里面有 纯数学家 像Ken Ono（小野肯） 小野肯教授

像Evan Chen 我说的这个 这个IMO（国际数学奥林匹克）的这个教练 然后也有做Lean的 做Lean这个语言的 里面其实就像Python里有Pytorch 它是一个图书馆和Python 它是下面的真正的那个编程 Lean里面也有Mathlib 是一个数学图书馆和Lean 这个作为一个编程语言 两拨人 所以我们也都有 我们又有这个做Mathlib的 像Kenny Lau（肯尼·罗）

还有他的朋友Jujian Zhang（张巨健） 张巨建就是这样的一些非常好的 好的同学们 然后我们又有 就是做Meta programming Meta programming叫元编程 是去把Lean当做一个编程语言来使用 去创造出Lean更多的工具 更多的抽象 层这样的 就是相当于 你可以拿Python去写一个auto grad的 一个著名的

一个coding的 这个 编程的一个面试题啊 可以拿Python写一个Autograd 我们来了一个同学 他拿Lean写了一个Autograd 对所以就是这 这里面又有很多块 所以并不全是数学的人 我们很多的就是招ML（机器学习）的同学 他们很多背景 我们队伍里面就是 当然说算上实习生 5个IMO 所以说5个IMO

然后他呃 就是他们会有很多数学的prior（先验知识） 就是context 就是 他们理解这个数学过程是怎么样的 但我们要求非常强的 again 这是一个工程问题 有趣 24年9月 你刚刚萌生了想法 但是在努力劝退自己 对 11月决定要创业了 然后

要等那个这个圣诞假才能融资 等圣诞假 圣诞假你干什么了吗 圣诞假 干了很多事啊 和Shubho一起在读文章 为什么是你们两个一起啊 他跟你 就是他 他已经说我要加入了吗 他当时没有 他当时就是在Meta 他当时 圣诞假闲着也是闲着 我们两个人就是找 像是一个reading group 又是reading group吗 他当时在旅游

他圣诞假感恩节 他都在 就是在不在一个地方 我们在Zoo 哦哦 你们还定期要开会 我们发现 我们就是讨论我们阅读的心得 我们发现 我们能够是很好的联创团队的时刻 是我们发现我们两个都非常讨厌Zoom 我没有办法跟人开Zoom的会 超过一个小时 他没有办法跟人

开Zoom的会超过45分钟 我们Zoom了4/5个小时 每次都 这是我们发现一件事情 我们思考的方式特别的又相似又互补 所以我们就非常享受每一次 我们的一些技术 技术的探索 他现在是 他是一个 他当然 你看他20年的GPU经历 10年的AI经历 他是当时CUDA第一批就是开发者

然后是2015 2016年 2014 15 16年 和Andrew Ng（吴恩达） 和他们这个百度 这个硅谷AI研究室 他加入百度 他当时是2015 2016 这是他进入AI的 他的第一步的AI 哦wow 是吴恩达说你懂GPU 你懂点数学 反正这就是AI 来吧 然后 当时有Dario 就是Anthropic的founder 他们当时有那么一群小团队 都在百度

都在百度 是美国 就在美国 就在硅谷 当时百度是叫 后来叫百度Mafia 像Paypal Mafia一样 这些人后面是做了多少 就是重要的工作 多少个 早期的OpenAI多少个啊 比如说Dario 就直接是Anthropic的这个founder 嗯 然后 嗯 非常好的 他们当时就是scaling works

我们就是做这个deep speech deep voice 就是把大量的这些speech voice的data扔进去 scaling works 他们当时办公室有一个 一个理念 我们绝对不招一个语言学家 哦 他们当时是做的deep speech和deep voice 他们需要语言学家吧 按道理 他们不招一个语言学家 有一点像我们 我们现在公司这个做编译器的 这个团队

他们当时16 17年拿就是机器学习 要去革命这个 Compiler code generation 代码生成 他们就说 当时就很多就是编译器的这些专家 说你不可能做到的 他们就说我们不需要你们 我们照样能做到 就拿AI进入一个领域去革命 这一个领域 某种程度上是我们这整一个 现在30个人了 当时就是早期这个创始团队的一个DNA 我们希望

我希望能够拿AI去 去给数学做一些 革命性的一些改变 你看他们说他们不招一个语言学家 要用AI去革语言学的命 对 那你们是不是也不应该招一个数学家 我们以为是这样的 我们以为是这样的 我们当时定了一个事情 就我们不招到第15个人的时候 不要招一个数学家

为什么是15个 就随便说了一个数 我们当时觉得 我们钱也不是 我们的种子轮 大家可能看起来数额很多 对于我们要做的事情来说 大家的普遍的想法是我们under raise（融资不足、募资偏少）了 我们raise的不够 我们的种子轮啊 所以我们当时觉得 这个人头是限制的 到20个人 我们可能就没有办法再招人了 所以当时觉得 那只能说 那就 以每15:1 这样的一个数学家的一个比例去走

但是他那句话的逻辑是我不需要语言学家 语言学家背景可能对这个团队是负分 我们现在的想法就是 我们招数学家需要他非常的思想开放 呃 早期的时候 其实 有一个叫做Frontier Math的一个Benchmark 与这个Benchmark相关的一些同学 当时有希望 就是我们有互相都希望能够一起合作

让他们加入Axiom 但当时就发现一件事情 就是一些数学家背景的同学 他对scaling这件事情 他有一定的 一定的犹豫 或者说不是犹豫 他就不愿意 他不喜欢scaling 这种哲学 他觉得说我数学是一个工艺 我是个手艺 像日本师傅捏寿司 你怎么能 就是给我一个

当时我们说我们要做Internet-scale dataset （互联网规模数据集） 有同学就是接了我的offer之后 就不来了 就说我不要 我不要做Internet scale data set 我们觉得又是要scaling 又是要更好的sample efficiency（样本效率） 就是当然说sample efficiency（样本效率） 这个效率是一个非常 样本效率是一个非常 非常满的 非常多意思的一个词啦 但是我就拿Percy Liang梁教授的这个话

就是它是做乘法 嗯 我们觉得来的数学家 我们现在希望他是跟我们对着干 就是 他们做adversarial（对抗性的）的 就是 就是与我们与我们相对抗的去做 Benchmark（基准测试）的创造 就 我希望你能够感觉我们的系统哪弱 然后去

就是当然是越做越来越难的这一些 这些基准集 所以某种程度上 就是Ken就是 小野肯他加入之后 我们的这个基准集的这个集结 是我们的第一号任务 嗯 我们继续把那个时针线来捋一下 好好好 我们刚刚说走了 就是 嗯 当时已经说到了圣诞假期 然后你们有一个reading group

对 两个人 OK 你们读了多少文章 那个阶段 读了好多 当时 而且当时我记得圣诞节 我们有一个叫圣诞大礼包啊 Yang Kaiyu（杨凯峪）老师他们写的一篇文章 Gabriel Poesia 他们一篇文章叫做 Formal Theorem Proving（形式化定理证明） AI的下一个前沿 是一个survey paper（综述论文）

survey paper就是它不是一个研究论文 它是一篇介绍其他所有研究论文的 研究论文 他就是把这里面领域的捋了一遍 然后我当时 我记得我 我那篇文章 我记得他第五部分是有这个目标 就是说 我应该一个好的AI数学家 能够做到什么样的事情 在这几个象限上它能够有什么样的

就是能力 这是一个 我们就把它做成了我们自己的表格 然后这个之前 就是从第一行到最后一行 我们 我记得 我当时就是每一个提到的 就是直接和间接提到的这个文章 不管是引用里 还是就是只是提到的一种逻辑 我就是比我已经有的阅读笔记 我想我还有哪些没读到的 然后还真有一半没读到的

所以那个AI for Math 那个GitHub整理的也不是很全 然后就是所有的这一些 当时就感觉就是我原来知道的 像是1 2 3 4 5个很好的做法 现在这篇文章给我连成了一个面了 就是他让我理解这个 这个big picture了 我就是更 我觉得我的理解 反正是当时有很显着的深刻 所以这个谢谢

谢谢杨凯峪老师 这篇文章 嗯 然后到这个假期结束 Shubho决定加入你吗 那还没决定加入我们 他到了就是后面再决定加入了 他是觉得跟你一起讨论很有乐趣 对 因为他是一个元老 他是一个AI的一个元老 我们 我当时都没有敢问他要不要加入我们 就是我 我想着就是 他为什么开始

你们是怎么开始这个阅读的呢 因为硅谷这个文化就是很多 就是AI的这个元老 他可以做你的天使投资人 或者他可以去做你的Advisor 就是他会 事情特别流通 就是硅谷 是一个非常有魅力的一个地方 就是学界 工业界 老师 同学 就是年长的研究者 经历丰富的研究者和就是刚进入

这个 工业界的研究者 他们就是汇集非常的流通 非常的 非常多的互动 就是大家是谁不重要 做什么事比较重要 比如说Shubho 另外的跟他 他指导过的创业公司也有很多 比如说Pika对吧 啊对

郭文景（Demi，Pika Labs 联合创始人兼CEO） 其实 Demi（郭文景） 当时进入Facebook的时候 Shubho还是面试 面试官 OK 好有趣 他也跟Mistral Mistral那整个founding team本来在LLaMA 就是是Shubho他们同一个org下面 另外的隔壁的那一个team 大家都包括 和我们队伍的 另外一个

就是我和Shubho说加入之后 第三个加入的这一个 这个人关系也也也很密切 就是他们也是很多年的朋友 然后你和Shubho 是一种tutor的关系吗 没有tutor 就是我 就是两个人 嗯有不同的背景 看这个事情的角度不一样 嗯 所以我们就聊了很多 比较呃哲学性的一些

一些研究的一些想法 我们当时就是觉得自己读的 读的足够多的时候 就想有哪些可以做新的事情 然后就是做新的事情的话 又其实可能连接到哪一个古老的 AI的其他的领域的一个做法 比如 我们当时看到的一些我们想做的事情 就在James Zou（邹昊）的那个AI for science那里 他们有做 比如说James Zou（邹昊） 这个实验室一直有做与

其实可以对AI 和数学很相关的东西 然后包括比如说我们当时想做 怎么样去做一个conjecture（猜想） 怎么样去做 好的猜想 呃 当时斯坦福的这个 计算机系就有同学在 希望能够造一个AI AI科学家这一个愿景去做 怎么样去能够去提出好的

机器学习的猜想 就所有的这些东西 它混在一起 比如说我们现在做的一些事情 跟当时早期做棋的这个expert system专家系统 这些都有关系 所以就非常有意思 就是所有的这些东西 没有人去尝试把它聚焦起来 在一个工业界盈利性的公司 也就有更多的

充足的资金和算力的情况下 去 去把这一些从 2022 年开始有一个爆发 一个想法的爆发 去把它验证下来 就没有人去做这件事情 我觉得非常可惜 嗯 这是有结构性原因的 就是2016年的时候Christian Szegedy 还有Wu Yuhuai（吴宇怀）他们在Google开始做 比如说Holophrasm 这一些

Holo是一个就是定理证明语言 2016年早期 Christian Szegedy大概在2018-2019年 一直在修改 自己写的一个 他写的一个白皮书 就是这个未来 非常长的一个白皮书 然后在2020年 我想说2019-2020年 OpenAI Ilya（Sutskever）带着人做了这些事情

Ilyalya 带了他们去做这个 GPT-f miniF2F 当时 OpenAI 还有 Jesse Han（韩杰思） 然后Stan Polu这一些 后面都成为了其他的好的公司 创业者 当时 他们有做在OpenAI做这件事情 2021年 有一个实习生 开始 一个人去在Google DeepMind做这个Alpha Geometry 他们发现 哇 这个做的是真好 所有的资源进来scale up

做成Alpha proof 然后做了 你看2021到2024 这是三年的一个耕耘 2024 一炮而红的这个呃 Alpha Pro拿了 28 分 差1分金牌的银牌 这个对我来说是一个 是IMO被解决的那一个时刻 他就是那两道组合题解决不出来 2025年反正也是 就一道组合题 大家都没解决出来 2024年的这个DeepMind真的是Kudos to them（向他们致敬）

这是一个跨世纪的一个时刻 就是AI在数学奥赛上达到了 达到了好的胜利 这是2024年 我们在2025年12月 做的这个 Putnam（普特南数学竞赛）的这个满分 是这 他们开启的这一个呃 序章的一个尾声而已 我们其实马上希望做的 就是研究数学 所以 这是这个

整个AI for Math的这个发展 发展的这个历史 Shubho作为你的第一个员工 是什么时候决定的 联创吧 对 联创 他是 2月份吧 2月份你融资 融好了吗 我当时有了不错的 就是这事能做起来 只要想做 就是已经有了 不是最终的价格 但是不错的价格估值

就是你出去融资验证一下 这个可行性 其实很快 就是1月份 1月7号 好像 因为1月头是这个JMM（Joint Mathematics Meetings，联合数学会议） 就是数学家大会 我当时到这个我记得是 应该是西雅图 就是那一年 2025年 居然 美国数学学会说 我们今年的主题是AI for数学 这个就是

由于数学是一个相对比较保守的 一个学科 这是 这是一个非常让人就是雀跃的事情 所以很多人都去了 还有一些计算机学家 我当时和DeepMind的Adam Wagner就聊了很多 我们发现我们都是 曾经在某一个这个 一个英国的学院就是上过学 还挺有意思的 然后这个Albert Jiang（Mistral研究员） 也是在这个学院上过学的 挺有意思的 然后 我回来了

回来之后好像就是第三天就有 就开始有offer了 然后就开始不停地VC们开始去竞拍 开始去竞拍 去竞拍 怎么竞拍的 就是比如说你给了我一个offer 然后过一周 又有另外一个人给了我一个offer 然后他们会尝试去把上一家的 这个价格 就是超过他 哦 所以最后从第开始的那一个offer

到最后的offer翻了3倍 翻了3倍 你是怎么去pitch这些VC的 这对你来说难吗 啊 融资之门 怎么打开的 因为你是第一次 没有人喜欢融资 没有人喜欢融资 如果说有一天有一个公司能把 当然我觉得这个很很难 因为毕竟这不是一个技能的问 就如果有一个很好的AI融资员

我希望能够让他去融资 你要付他多少薪水 我可以给他percentage 这个真的我可以给 我觉得融资是很难的一个过程 它不是说难 结果难 它就是累 呃 你是一个复读机 你一次一次的说一样的事情 你一次一次的接到一样的问题 真的我就能 我可以可以把它录下来

然后我就给你们大家发 对吧 你们反正问题也是一样的 但是呢 就是从这一些大量的 比较无聊的这个过程中 有一些让人很激动的谈话 通常这一些谈话是你最终选择的 选择的投资人 比如我印象特别深刻的 我们最后的领投方B capital 我跟Howard Morgan 就是有一个对话

我当时在赶这个rebuttal deadline（审稿意见回复截止日期） 就是有一篇就是文章的这个deadline 然后我当时跟他在Zoom上对话 然后 我发现Howard简直就是一个 他比你更乐观 他比你更觉得你的商业模式有前景 他告诉你这些是你的商业模式 Renaissance Technologies（文艺复兴科技） 的 co-founder（联合创始人） 和Jim Simons一起 然后他也是另外一个

硅谷老牌的一个VC 叫First Round的 联合创始人 所以他既是 他是一个数学家 他住在住在纽约 他现在有时候还去纽约大学上上课 然后 然后当时我就觉得 Harry Morgan是一个非常 让我感到 就是很跟他聊天 我很激动 就是我当时在MIT的时候 嗯 Jim Simon（吉姆·西蒙斯）先生还在的时候有来我们MIT

网上有一个两小时的一个围炉谈话（fireside chat） 我当时是本科的那个数学社 就是我们那个活动 我就跟他去去聊 然后所以今天见到我 不是今天 就那一天见到Howard 然后 他还在那个硅谷的那个TV show里面 就是出现过 然后 然后他就给我介绍了另外一个人 然后这个人其实是James Simmons的这个 表哥

或者表兄弟 反正反正还挺有意思 他们俩长得还一模一样 就是有一些有意思的谈话 你可以见到很多不同视角的人 然后 你可以 我其实觉得我不是一个特别厉害的 fundraiser（融资者） 我不是 我一般就是 这个事情是什么我就讲 然后我一般还把很多就是风险啊 什么的我全讲出来 是什么 你讲的风险

我当时种子轮 我就说这个 我们商业模式并不是非常的确定的 我自己做过了这个量化交易员 我不知道我们这个东西 是不是量化交易 我觉得可能不是吧 我听说这个还是有差别的 跟量化 效果到现在不如量化好 对对对 我当时就说我 我虽然我自己在量化中做了一些数学 我觉得你就是作为一个商业模式来说

它一定不是一个 一个最终的商业模式 我拿这个的举一个例子 是说 一个数学比较好的一个AI 大概率上是有用的 就这只是一个例子 这不是我们要具体要想的第一个市场 我们具体要想的第一个市场 我也不知道是什么 我们现在是个种子轮 目前的还是希望把这个东西 科技给做出来 当时反正是这样的一个 我讲的都特别保守 然后我后来才知道

投资人们 一般来说 他们见到的创业者们讲的比较 毕竟是一个pitch嘛 他讲的都是比较乐观的 然后所以他有一个打折 他比如说你可能讲说 感觉这个东西是10分 他心里就给你讲一个8分 他有一个这个conversion rate 我 如果当时讲的是一个7分 他就给我打折 就可能打没了

所以就我会是后面才知道的事情 但是他们都跟你say yes 你有被拒绝吗 有被拒绝 拒绝多还是yes多 没有人想拒绝我们 他们就不告 就没有人回你的消息了 因为他们其实在希望做的一件事情是说 如果有别的人要领投你了 他不太确定 他不想拒绝 他拒绝你 你可能以后不理他了

他就拖着你 拖着你 完了之后看 这个人给了你 哎 那我也给你 就是他是一个这样的一个群体 group think的一个过程 所以他们后来都跟了吗 很挺多的 就是那一轮其实挺多挺over subscribe的 所以你核心是需要找到一个领投 愿意 对 say Yes 我们当时有好几个领投方的 竞拍的一个offer 哦 几个竞拍 三个 你是怎么样竞拍的

我没让他们竞拍 这是几月份 这是1月份 到2月份到3月份 嗯 对 差不多一个月一个 一个月一个领投 对 领投方 因为就是价格从1倍到2倍到3倍 就持续你都在聊 你聊了多少投资人 嗯 我不知道 大概几十个 几十个 对 我觉得 其实有一点

可能说以前做数学一个职业习惯 就是总觉得 希望有一个很optimal的一个outcome（最优结果） 就总觉得说 希望能够把这个 这个轮做的这个结构好一些 对 嗯 然后 嗯 也不太知道怎么融资 嗯 对 后面就学会了一些道理 后面的融资就顺利的多 1月份有一个领投说

我愿意 然后你没有停 你为什么没有直接接那个offer 然后还在继续聊 因为他要dilute（稀疏股权）我50% 哦 我不可能让他dilute（稀疏股权）我50% 你当时say了yes say了no吗 我当时说了no 哦 但是1月份你就确定你这个事情有戏 所以Shubho答应加入了 是2月份的那一个 更真一点的一个offer 就是

那个时候他加入的 就第二个offer OK 但是他还不是最终的offer 你还在聊 最终 对 我还在聊 你聊到了3月份 我当时2月份那个我是想接了的 于是我后面我就跟所有人说 嗨 这个 我是想跟他们走的 就是你可以加入我这一轮 但我可能不会去看其他的 其他的offer了哦 然后到3月 为什么又变了呢

呃 我觉得就是这个Harry Morgan效应 这个完全就是我作为一个 就是我 我对文艺复兴有非常大的 这种崇拜 然后而且价格也确实很不错 就是2月 你已经觉得有一个不错的offer 但是你还在聊 然后聊到了3月份 是那个B Capital 他是怎么offer你的 他的一个风格

你每一天都会接到他的电话 就是他 非常看好你 我当时在那个做rebuttal 我没有时间 就为什么这个过程中拖了很长 是因为我还在 我还在上课 我还在考我法学院的考试 我还在那个 我还在上我的数学课 虽然说就是我去的也少一些 但是就是我还在 我有事情 我当时还有XTX 就我当时非常的忙

你2月份不就应该准备辍学了吗 嗯 2月份 但是有offer 我有这个offer 然后当时 我就开始 我还没 我还没incorporate呢 我去找这个律师去 我去建立一个公司 因为有很多 当时什么都不知道 没有人完全 这什么都不知道 然后什么都不知道 我没有任何的这个孵化项目 我也没有 我真的什么都不知道

就是到最后是说 他们说我要给你写这个term sheet了 你这个公司我写什么 我说我还没有一个公司 所以3月份开始成立公司 2月份其实其实1 2月份 你问我还在做一件什么事情 我在招团队 就是我大量的时间 比如说就是在吸引一些 我非常渴望能够得到的 AI for Math的人才

Shubho肯定是第一个 对吧 嗯 但Shubho其实他是战友的 然后去 再去我们两个再去找一些 找一些同学们 嗯 所以 你是几月份辍学的 我是夏天辍学的 夏天辍学的 那3月到6月在干嘛 那时候 我的那个工作签证下来了 所以我可以 我可以辍学了 哦对 3月6月在干什么

就是你签了一个term sheet之后 你要做很多的这个法律的due diligence（尽职调查） 然后他才能把这个钱汇到你这里 你要找这个办公室 然后你又去招人 当时有很多很多的AI人才在流动 同时AI人才市场的这个价格非常的高 我们这个创业公司 无法去支付一个100个million 这种package 所以我们 当时花了很多的时间与精力

在希望能建一个好团队 对 那一轮融资是3亿美金的估值 融了多少钱 融了64个million 就是6,400万美元 是比预期低的吗 是比预期高的 预期是50个million 是比预期高的 对 嗯 你觉得作为一个华人女性 在硅谷好融资吗 这个身份会给你带来任何加分减分吗

我倒没觉得华人女性 我觉得就首先我比较年轻 这应该是一个 加分 减分 减分 年轻做product 是加分 年轻做deep tech是减分 我没有 我确实不像说是我们团队里面的 除了我之外的所有人 我没有一个带 我没有这个track record 嗯 这肯定是减分 然后我

觉得华人女性这个没有什么 我没有什么 这不是一个加减分 年轻是一个减分 我有时候 我有时候倒是觉得说 我有时候觉得就是 呃 就是年轻这个事情吧 做产品的话一定是加分 但是做产品型 比如说consumer 那些start-up 就比如说Facebook这种

对对 其实我觉得就是真正应该加减分吗 年轻就是 我觉得作为一个创业者来说 呃 你要你被要求的是长期进行重复的 啊 高就是非常high-stake（高风险的） 非常重要的决策 而你的每一个决策

给到你的时间是非常短的 所以如果你没有一个很好的一个我 一个word model 一个 就是第一性原则的一个体系的话 你这一些决策容易不太 最值化 所以我觉得还是 我还是希望说我如果再来一次

我希望我能够在再多多几年 再就我觉得太早了 嗯没准备好还对就这个 就出发了 我当时听一些 扎克伯格19岁 他19岁开始在跟谁 他融资跟谁聊 他跟Peter Thiel聊 Peter Thiel跟他在一个餐馆见面 手上拿了一张term sheet 说 这是 这是我的term sheet

然后扎克伯格说好的 谢谢你 我什么时候能就是什么时候给你答复 他说我们这餐饭不吃完 你不签我这东西我现在撕掉 就这是一个19岁的创业者 就没有见过这种大风大浪的事情 他 这个故事就是 他就去了洗手间 去洗手间哭了一场 回来 签了 这上面肯定有他不喜欢的terms 他放弃了他去其他竞拍的机会

我觉得就是年轻创业者真的还是挺 就是但是创业者这个事情就难 就是年轻创业者这个事情就是你 大部分时候 你并不知道你自己的这一个决定 他到底是对还是不对的 你可能等一会有更多的信息 会能够让你对你自己的决定 感到更加的自信 但并不一定让你决定更对或者更错 而你去等这个更多的信息 这个过程中

是一个高风险低收益的过程 所以就是有些时候 你还不如就直接跳下去 就是我记得我们有一个 有一个投资人 他拉我们一群女性的一个创业者 去一个一个活动啊 找了一个那个森林 然后在那个森林里就是ZIP line（高空滑索） 就是你抓上那个东西 你就晃过去 就是一个树和一个树中间有个绳索 你知道自己拴在这个绳索上

我当时我第一次 我人生从来没有做过这个ZIP line（高空滑索） 我就不敢下去 然后呢但是就特别尴尬 因为我是第一个人 后面有一群就是女性创业者 她们都玩过这个好像 她们以前可能去年就有这个活动 然后呢她们就有点等的急 然后我就只能就是一闭眼一咬牙 我就下去 这个过程后面他们跟我说 我希望你能形成这种肌肉记忆

就这就是你每一天需要去重复的 麻木的这样的一种take a leap of faith（孤注一掷的信念） 所以我觉得 一个tech队伍的经历 所以我觉得 这是我希望 可能说我希望我如果说就是再来一次 还是这个年龄的话 我希望 我以前就是能够把阅读再再抓紧一点 我可能希望能读3倍的书 我可能 我学过的东西 都不够用

这是一个非常有挑战性的 一个一个事情 其实就是因为这种高压快速决定呃 这样的一个nature 就不管怎么样 你在那一刻你得跳对 你有遇到你要绳拴的不紧吧 就完了 嗯对 你有经历像小扎（扎克伯格）那样 跟Peter Thiel那样的时刻 然后自己在卫生间去哭一场 回来签了

我有一些 呃 我倒没哭 但我有一些各种各样的感受到 比较艰难的 可能我现在做的这个决定 我以后会后悔 但是我也得做这个决定的时刻 比如说 比如说 就是大部分的人才 早期大部分的人才的情况就是 人家手上有6个offer 你得进去 对

我成了那个 但我又没有 人家有leverage 你做不了Peter Thiel 对吗 嗯 那你是决定出还是不出 你肯定得出呀 你就这个 这个事情为什么他痛苦 就是你其实只有跳一个选择 你只要by as to what action 每一次你在执行与不执行

做和不做中选择那个乐观的选项 你就能够有一天走到那个终点 嗯 这其实是一个 这其实是一个我的 一个感受 就是有些时候其实没有办法去想 有几次这样的啊 情况很经常很经常 很经常 硅谷的AI人才的价格已经非常高了

但也不单指全是人才的这些 就是有很多 很多类似的时刻 对 除了人还有什么 除了人还有什么嗯 我们又有一轮融资啊 在这一轮融资中 也有很多的一些故事 对啊 或者说是 嗯 就是很多很多的情况下 我觉得就是要让利吃亏

啊 每一天的让利吃亏 让利吃亏 让利吃亏 这样才能够做到一个呃 一个 一家伟大的一个公司 让利吃亏 对 就是让利吃亏 种子轮是25年的 1月到3月 几月close的 嗯 6-7月close的 夏天close的 然后与此同时 你辍学了 等那个签证 等了等 然后第二轮

就是A轮 是25年底开始的吗 不 A轮没想融 A轮在圣诞节的时候 我们已经有的一个 投资人说 我们要Pre empt(抢先拿下交易)你 Pre empt的意思是 我知道你现在不融资 我知道你没有PPT 我知道你什么材料都没有 我要给你一张term sheet 然后 我希望你能够直接 有点像Peter Thiel

希望你能够尽快的把它签掉 这样你就不用再去融资 我省掉你这样的 一个 这是他们的这种 就是first mover advantage 有这样一个 这样一个感知 1月5号 我被叫到了 一个外地的一个城市 然后我给了一个pitch 然后 我拿到了 当天晚上 拿到了这个offer

然后接下来的一个星期之后 还是一个半星期之后 拿到了另外的一个offer 我们最终签了那一个offer 这是我们的A轮 所以是从啊7月15号到1月15号 这个差不多是6个月 嗯 为什么选第二个 嗯 这是一个很好的问题 其实主要的主要的原因是

就是 哇 我觉得就是后面我们也第一个 让他也投进来 所以并没有一个 没有特别大的一个取舍 对对对 就我反正也能够得到 就是 很多长期以来支持我们的 投资人的支持与帮助 但最终有一个both的 一个解法 嗯 领投方是谁啊 领投方是Menlo Ventures

为什么你觉得他跟你可能更契合 对 Menlo这个partner Matt Kraning是一个从我们种子轮开始 对我们提供非常多帮助的 一个投资人 然后他也是 本来是他是一个 电气工程的PhD和物理的本科 然后他是一个非常technical 非常 呃 有一点nerdy 非常有意思的一个operator

他非常的就是founder spirit 然后同时Menlo 又是 Anthropic的最大的 institutional investor（机构投资人） 然后嗯我们是Menlo Ventures 在这个 Ventures这一部分 继Anthropic之后第二大的AI投资 嗯 他们为什么愿意 为什么愿意 我觉得他们其实种子轮可能就想投 但我们

当然种子轮就认识的时候比较晚 嗯就是 已经差不多是就定下来了 对 然后我觉得我们在6个月里面 这个团队 嗯 执行的快准狠 这个 这个团队在这个6个月的执行中啊 持续表现没有失误 而且他们在 嗯 从0 从什么都没有 就是第一个月 搭所有的infrastructure

然后完了之后开始去 train模型 搭系统 然后去做这些决定 就是deterministic确定性的tuling 而不是写 用Lean这个编程语言去写 所有的这个东西 是一个非常 我觉得是spectacularly executed（执行得出色）的 一个非常完美的呈现的一个工程项目 然后在4个月的时候 拿到了普特南的满分 然后在6个月的时候去 做出了许多

研究问题 没有许多 一批 三四个 研究问题的解决 是没有人类干预的 第一个自动形式化证明系统达到这样的 一个里程碑 然后 发现了一些在代码证明中的 一些神奇的transfer learning 就是 原来这样的一个AI数学家 能够在代码的验证中

达到一个非常好的一个表现 在一个Putnam Benchmark中 老版的DeepSeek-Prover达到了11% 当然这是老版的DeepSeek-Prover了 我们达到了98.93% 呃 对 就是原来的这一个 解决普特难的这个数学系统 嗯 所以他是主动pitch的你 Menlo 我们就是 大家都经常 有时候会 定期会见面 毕竟他们是我们种子轮的一个 小的一个

他们种子轮放了 他们是我们的种子的1%的投资人 投资人 然后现在是 作为当然作为领投 整个过程 整个过程当然会更加的多 多几步 这一轮融资的估值是16亿美金 已经达到了一个独角兽的标准 融了多少钱 我们融了多少钱 至少是2亿美金 2亿美金 对 嗯 这个过程中

其实你们团队很多人都 就是看起来经验都比你丰富很多 对 然后包括也有非常知名的数学家的加入 为什么他们都愿意让你来做CEO 你刚刚也说你是一个 就最年轻的一个 然后也没有任何的tech lead的背景 他们为什么对此没有顾虑啊 我也不知道哎 我也每天在想这件事情 就是可能 可能他们也没有意识到 我也没有意识到 反正就是大家就一起在执行

然后现在的一个设定就是所有 所有的 嗯 所有的一些比较strategic的一些事情 其实就会就是root到 我和Shubho这里 所以我们其实 能够使得研究者和工程师们 有很好的一个环境 可以去就是在没有任何politics 没有任何人事纠纷的情况下去

纯新的去 就是纯粹的去 最新 在技术上 然后就是去执行 所以我觉得 这是一个很好的 一个frontier lab的一个环境 然后 我觉得还有一个就是这个 这个问题 它是一个非常有意思的问题 它非常的宏大 它也非常的困难 然后这个事情又有很多很明显的1 2 3 4 5 为什么这些技术上会难做

但为什么这些通过好的 就是engineering都能够去解决 所以呃 我觉得大家其实是被这一个问题 这个北极星去吸引 嗯 对 我只是那个递水的人 嗯 对 你们也算是现在的一个Neo lab（新型实验室）对吗 我们是在那个TBPN和Deedy（Deedy Das）的 这个Neo lab（新型实验室）名单上 确实是 你怎么理解 就是在相同类似时间内 就是在相同类似时间内

成立的这一波Neo lab（新型实验室） 我当时融资的时候 还没有Neo lab（新型实验室）这个概念 所以第一轮融资的时候 对 就是他们就觉得我疯了 谁认为你疯了 投资人 就是他们 他们就是可能就是觉得 这 这是什么呢 就是当时 而且还有一件事情 2月份的时候 DeepSeek出来了 当时大家对模型这两个字 就非常的恐慌 大家一听模型

不赚钱不要投 就是模型啊 这个感觉模型还不如一个consumer 产品有mode 但当时大家是这样的一个市场的一个 为什么 因为DeepSeek把价格拉得非常的低 对它commoditize（商品化）了模型 所以说大家都不想投模型了 然后 但是 大家没有意识到一件事情 我们不是一个模型公司 我们是一个deep tech公司 我们是一个深科技公司 我们做的这件事情有点像SpaceX

为什么你们不是模型公司 你们 相当于是训练了一个 数学家的大脑啊 对 就是Lean吧 他有一个很古老的一个背景 就是这一些做program synthesis 我查了一下这个中文怎么说 叫做程序综合 我也不知道这个对不对 然后 program verification 就是程序验证 就是它来自于这样的一个

古老的一个领域 然后Lean作为一个形式化语言 它目前就是在公开的这个 呃呃 domain的领域 网上的这个总的这个tokens 这个就是字符串的这个 这个就是不太大 就是它是一个非常小的一个一个数据 数据集 所以说就是会遇到很多的问题

比如说你怎么样能够做一个Internet scale 一个一个互联网这么大的像 像有多少Python 就有多少 Lean这样的一个数据的 这样的一个扩充呢 这是 这是一个不太不太清楚的一个问题啊 Lean它是作为一个编程语言 又带有自我验证的这样的一个性能 有点像 既是一个C 这个编程语言

又是GCC Compiler和C runtime 两者合一 它是一个非常fragile 也就是说非常脆弱的一个语言 它的这个 它有很多的限制 它有很多的 就是作为里面的这个object 它必须要符合一些种种的 这个限制 所以它是在作为一个Lean 它本身又带来了这些挑战 然后呢Lean里面

又比如说我想去验证一个东西 它真的是在证明 没有给我就是作弊 比如说我假设公理n加n等于n 证明2+2=2 你知道2+2=4 这一定不是一个合法的 一个运算 那么嗯 我如果要去找一个东西 能够去证明它是严丝合缝的 叫verify proof verify proof这个东西原来叫做community

里面用的叫做comparator comparator这个是比这 我们现在我们自己的这个verify proof 慢100倍的 也就是说在我们刚开始的时候 我们必须自己要造一个快的东西 不然我没法跑 我们造了大概12 13个 这一些 这一些能够辅助这个Lean能够更好的 去执行的 不管是生成还是验证的的的这些工具

然后 我们知道说Alpha proof用的是这个 Monte Carlo Tree Search 蒙特卡洛树 搜索 呃我们觉得这个太贵了 我们看一下我们有多少钱 我们觉得我们做不了这个蒙迪卡洛树 我们又得找别的办法 这个最后 其实和国内这个字节豆包的Seed-Prover 做的有点相似 这个系统的这个design 我没有理解

你为什么说你们公司更像SpaceX 因为我们有很多的这些技术壁垒 而其实 某种程度上如何去训练一个模型 当然说更高更快更强 然后又有很多的一些 大家的一些secret sauce 我们这个问题 可能在就是他遇到的这个科技挑战上 时间会更长 我们至少在种子轮的时候 是觉得我们的R&D cycle是会

拖得非常长的 我们主要的这一个竞争对手 我们刚刚开始的时候是他们1/5 只融了他们1/5的资产 我们的估值也是他们的1/5 然后他们比我们早开始两年 就是Tutor的这个公司 然后他们用了两年的时间才到IMO的 这个 6道题里做了5道题

我们觉得至少得花我们很长的一年半 一年 但我们想到说四个月 我们就往这个普特南冲 我们做出来一个满分 然后接下来冲 研究的一些问题 其实都是世界各地的数学教授 给这个小野肯老师 发邮件说 以色列有一个Technion 这个大学的

老师给呃嗯 给Ken发了一个邮件 然后那个 和Ken又有一些交流 然后有这个 波士顿的一个 代数几何学家 他他又有这个一篇文章 反正就是 我们其实某种程度上 在很大的压缩这个时间 这其实导致

我们也有一些Infra上的一些债要还 所以我们现在也有在还一些Infra的债 小野肯老师肯定 对你们团队来说是一个非常有 标志性意义的人 对 他像是一个 他的性格是一个高中的篮球队教练 哦 他的性格是一个就是他会给所有人 就是就加油助威 然后让大家就是 非常兴致勃勃的 乐观向上的 去做我们手上的任务的

这样的一个人 是你找他 还是他找你啊 他是你之前老师 对吧 对 他给我发了封邮件 几月份 就是你上轮融资已经公布了 对吧 对 他是11月 去年我们 我们之前就有邮件的 一些交流 你当时邀请他了吗 没有 不敢 对吧 不敢 我也不敢 Shubho 我也不敢 对啊 Shubho说他要来的吗 其实我觉得融资也是这样 我不太敢要钱

就是 我是 我是说你 我没有办法去说服你 你只能自己说服自己 如果你想做这件事 我也想做这件事 我们可以一起做这件事 哦 对 但我不希望 我万一开始引导你 我有可能会误导你 这个大家 大家都是成年人 自己做一些有趣的选择 然后一起去 去承担这个选择的风险 所以你跟Shubho的过程更像是我

我一直在告诉你我在创业的进展 然后你等他自己说我要来 我知道他是一个 工业界元老 毕竟你在director这个level上 我觉得可能也有很多项目 我怀疑交付的时间会是比较长的 对 但后面这个Fair(Meta Fair实验室) 后面就是这个组织 很多的人都离开了 对对 所以他是自己跟你说他要来 他是怎么跟你说的

Shubho 在Verve咖啡店说的 他怎么说的呢 他就说好多好多人都走了 感觉这个地方不太像是以前的地方 然后呢 然后就是 你要一起做吗 我说好 那个时候你已经融到了 2月对吧 已经有一个offer了 对 然后他有跟你谈条件吗 就正常吧 大家就是按照标准的来 你当时是什么心情 我挺高兴的 我觉得挺高兴的 因为我觉得

感觉一个人做这个事情比较孤单 你有预感到他会来吗 我有预感到 但我们当时 我当时想如果他来 应该一年后了 就我们 可能我 我总觉得就是 其实我现在对我们的公司 现在的一些新加入的一些成员 我总一种 我总有一种 就是 我感觉我 我们就是 希望我们能够把我们做的最好 让我们能配得上他们的这种价值 所以我当时想唉

一年了这个可能做出来一些小成绩 然后这个Shubho可以来指点江山 往上再做一步 当时是这样一个想法 那你的老师呢 他给我写了封邮件 11月底非常怪的一封邮件 他大概意思说他要来湾区 我说啊 你要来湾区 然后他说 嗯 如果他加入了OpenAI或者是DeepMind的话 我不应

就是他希望我有一个心理准备 然后我心想 你要加入OpenAI和DeepMind 那你为什么不来我这里 然后我就说 你可以来我这里 然后这个时候 你之前没有跟他说过这话 没有 我但是我 但我就觉得 你如果能够去加入OpenAI和DeepMind 我觉得你可以来我们这里 我觉得我们 他说那句话是暗示你吗 就是说 他是真的 我觉得需要一些建议 哦 他当时OpenAI可能给了他一个offer 噢

那为什么他说的是你要有心理准备 就是因为我们 我们知道 他知道我有这样一个公司嘛 有可能会 可能会有一些竞争关系 对吧OpenAI的 AI for Math的 这样的一个division 可能和Axiom会有一个战略竞争关系 他可能作为我们的 我们是朋友嘛 他不希望 我很突然的听到这个消息 就是他在给一个竞争对手进行工作 所以他希望他能告诉我说

可能这是他的一个选择 也希望我能够理解 然后我说那来Axiom 然后结果就谈得非常快 非常好 他是来玩就跟你谈的 还是线上自动谈的 没有就是Zoom谈的 我当时 飞的乱七八糟 11月底12月 我是从这飞到了 飞到了拉斯维加斯 是re:Invent 然后飞到了这个NeurIPS 我们在那NeurIPS赞助这个 AI for Math workshop

然后我们有一个就是活动 可以就是招聘的一些活动 我就在圣地亚哥 圣地亚哥回来 然后 就一堆一堆事儿 你怎么说服他呢 在你们那个Zoom会上 你说你 你对比OpenAI 你的优势是什么 我倒没sell他 我就说我们非常的就是 我们也open 你来

然后你可能还是得去OpenAI看一看 如果你能有时间来我们这边 看一看 结果他没时间来我们这看 我觉得肯定凉了 你想他来湾区 他就直接去OpenAI 然后就飞走了 他没有在我们这 那可能说明我们没有什么机会 结果他来了 哦 他来你公司了 对 他是来你公司跟你谈好的 没有 他没有来我公司 就是他 在Zoom上 我们就定了 你截胡了OpenAI 对

你怎么说服他的呢 他被什么打动了呢 我觉得首先他觉得我们的 就是这个团队更数学 这是一个事情 嗯 我怀疑发生的事情就是 他去了OpenAI之后 可能觉得那边比较 做数学的同学不是特别多 来我们这边的话 可能有更多就是数学的一个氛围 这个 这个公司的DNA和专注点就是数学

而不是一个general的AGI 然后数学是其中一个部分 可能更有marketing的成分 小野肯被认为是 继承了拉马努金精神的 现代数学家之一 而且他之前说 他根本不相信AI会超过自己 然后后来他内心发生了变化 可能这是他联系你的一个契机 我觉得是 他有跟你说过

他这个认知是怎么发生变化的吗 他有说 对然后 我 我其实记得就是 我们当时聊的特别的仓促 因为这就是一个截胡 哦 多长时间 嗯 就是两三天内 OK因为那边那个offer 要爆了 就爆炸explode 哦 那我们这边 我觉得还有一个很大的原因 Ken加入是因为François Charton

François Charton是AI for数学的这个 2019年François和Guillaume Lample Mistra的这个chief scientist founder 他们一起写了一篇文章叫做Transformer 可以在微积分上 在integration上能够比一些像Mathematica 这些电脑系统 电脑代数系统要做的好

然后从那开始 François就一篇又一篇的去 去做了非常多重要的工作 去让AI解决各种各样的 就是specialized的 就是特殊的数学问题 然后在AI for Math这个领域里面 我觉得就是Ken还有François 他们肯定是 对对方也非常惺惺相惜 François作为我和Shubho之后

第三个来加入我们的 我们这个团队的 他们就有很多的共同语言 就变成了一个it's called math club 就是我们这里有一个数学俱乐部 大家都有很多可以聊得来的东西 然后它也给了我们这个AxiomProver 去解决哪一些问题 选择这个问题 给了很多很不错的建议 我想多问一个关于小野肯的问题 他是一个什么样的人

他就是那高中篮球教练 他就是特别特别乐观 特别 特别就是让人你跟他聊 你就会觉得唉呀 我本来就很想做这件事情 我现在更想做这件事情了 所以他是我们特别好的一个 文化上的一个 一个增加 然后他也是 当然是一个非常好的数论学家 他在这个划分函数领域里面就是 非常年轻就做出来非常好的成就

然后他也是一个很好的研究导师 他带我做了很多文章 然后还有很多其他他这个REU（美国大学暑期本科生科研项目）的同学 都成为了 不错的数学学者 他是个直觉派的数学家吗 这个我倒是不知道哎 这是一个非常好的问题 我觉得他应该比我更直觉派 对 但是我 比如说我们就是合作的过程中 像我一个合作者张盛桐

他就是比 肯定是比 这个我和Ken我们 他比我们两个都要直觉性 所以就是Ken 我觉得在二者之间 Ken 我理解了 Ken的这个神奇的能力在于 他是理论建造者 数学里面的大概分两种 一种叫解决问题者 一种叫理论建造者 他能够把不同的 领域的东西

去连接起来 然后有一个完全全新的视角 看一个问题 他能够去发现很好的问题 并且给其他可能更善于解题的同学们 去做 嗯 他会觉得他从学校放弃了终身教职 加入一个学生创的创业公司 他会觉得有某种奇怪的感觉吗 我没觉得 我觉得Ken反正和我

我们两个都是比较就是叛逆的人 对 就是我觉得 Ken是数学教授 他同时又是 美国这个奥林匹克游泳队的 这个教练 去给他们分析这个游泳的数据 怎么样去把表现更好的提升 他又去拍这个好莱坞电影 拍了拉玛努金的那一部 现在要拍第二部 拍这个米尔扎克哈尼的这个 这个

第一位女性菲尔兹奖得主的这个 这个电影 然后他同时又做很多的 就是他有一个慈善基金会 就是以拉玛努金命名的 去给一些很年轻的世界各地的 希望能够 拿一些资金 去买数学课本的同学们 一些辅助 同时他又是美国 美国数学学会的前任副主席

然后又是 在白宫又有一些这个政策上的 就是咨询顾问的一些职位 所以就他是一个非常非常全面的人 他作为一个数学家 然后加入一个AI for Math的公司 建造一个类似于 AI数学家 嗯 会替代自己吗 他倒不觉得会替代自己

他我们其实大家都觉得 我觉得他就是思想非常开明 作为一个数学家 有一些数学家可能真觉 得 就是AI去代替自己不是一件好事情 但是我们见到的越来越多的 比如说Ken 比如说Andrew Grandville 那也是另外的一个很好的 加拿大的一个数论数论家 啊 也 这个Andrew也是 我们 他也是著作等身的一个数论学家 他们其实有一个想法

就是随着AI的进步 人类数学家会学习 在不同的抽象层面上 进行逻辑推理 这是一个非常有意思的一个点 就是 我们某种程度上在编程这一块 以前编程 我记得如果你去这个计算机博物馆 就在这附近 嗯 以前就是电脑计算机 就是有那个小卡片

然后在那里打洞 就是那个 那是很很早以前的一个 computer science的一个雏形 后面有一些更 low level更低层的这些编译器语言 然后一直后面到Python 现在到可以拿自然语言进行Web coding 编程 然后数学 其实某种程度上 数学家也学会有更高层的 这个抽象的这个思维 比如说我刚才讲的 有可能他们就是去说

这些问题是值得去探索的 然后让这个AI去帮他们探索 我们希望 我们真心的希望 我们的AI 能够有具备一定程度上的猜想能力 能够让这个猜想的这个部分 与证明的这个部分进行某种向上螺旋 就是我希望它能够随着这个AxiomProver 能证明的东西越来越多 我们每一天证明的东西

都会进入到明天的 明天的这个应用中 不管是 作为一个skill 一个技能 就像LegoProver的skill library 这个 这个设计 或者是 作为未来的这个训练数据 我希望它一定是self improving的 某种程度上 self improvement 甚至说你可以叫它continue learning 当然这是一个最近很火的一个词 一个buzzword

在一个能够有啊验证signal的 验证信号的一个领域 像数学来说 是可以去试验的 这些很好的很前沿的 AI的一些东西 包括subagents skills MCP这些东西 全部可以在我们现在的这个 数学作为一个操场 一个playground上可以去实验 嗯 你们在普特南的那个 那个故事可以给大家讲一下

就是大概就是在2025年12月6号 这一天早上 我们收到了啊 就是普特南大学生数学竞赛 当天的考卷 然后我们是拿到那个考卷之后 我们要做的第一件事情 就是我们需要把它 变成形式化的这个题目 让这个AxiomProver 我们的这个AI系统去做 那我们这个题目

当时其实挺有意思 早上6道题 下午6道题 如果这个题目本身是一个证明题的话 那么就可以直接就是把它变成形式化 如果是他说要求解的话 那还需要求解 所以 其实还是一个挺有意思的一个过程 我们所有人都在这个办公室的 一个 庞加莱这个会议 会议室是我们的这个war room 我们的战争室

我们数学家 有些人就在解题 所以其实就是解题 解题的这个过程还挺有意思的 就是我们可以看到说 有人类的解法 和就是我们最终这个AxiomProver产生的 这个完全是不一样的一个思路 我们在 大概当天下午3:58的时候 我们发现我们有8道题 然后我们有8道题的话

呃 就是 呃 80分 80分是一个什么水平 80分 一共120分 去年的80分是世界前五 然后呃 但是往年的80分可能不是世界前五 前前十前20差不多这样 然后我们 然后我们就希望能够拿到一个90分 因为我们当时就有一个选择 我们是否告诉世界我们做 还是我们再等一等 然后我们最终确实是有 就是12道题

就是全部满分 然后这个过程还挺有意思 当天我记得 就在解题的时候就是 小野肯教授 他有一些非常有意思的精彩语录 然后我和Shubho 我们两个人笑的就是前仰后合 他说 不要 现在 不是说数学纯粹之美的时刻 不要去精确的去搞这些东西 现在是战争状态 就是在大家在求解的时候 他就说能怎么快捷的去做

就怎么快捷的去做 就得到那个数之后喂进这个AxiomProver 也其实是和 IMO的这个其他的这个标准是一样的 就是说如果有需要求这个解法的题 把这个数就是一块的喂进去 因为Lean只能做证明 它不能够帮你说是去求解 所以求解是人做的 求解这个东西是人做的 求解在IMO的那一个 就是IMO的那个考试中

甚至是2024年 其实这是Alpha proof 它给的先例就是有6道IMO题 然后有一些题要求有一个得数 这个得数的话就是要把它一块放进去 变成一个证明 但是后面我们发现一件事情 就是我们其实可以不求解 就我们其实 因为我们这个系统里面 也有一些就是informal的这个model 其实我们是可以直接让 他就是做出这个解法的 最后其实我们发现

我们的每一道普特南的题 其实我们并不需要做人类求解的 但我们以为我们要求解 所以还挺有意思的 小野肯教授 为什么说现在是战时状态啊 因为就是时间紧 就是我们大概估计说 一般早上6道题和下午6道题加在一块 12道题 最多不超过3道题需要求解 因为确实是少数的 大部分还是证明题 早上那道试卷下来就是6道题 4道题要求解

然后我们当时只有 就是能做的动这个数学题的人 就是基本上就是我普特南成绩也不怎么样 成绩也不怎么样 反正基本上就只有Evan Chen 然后Evan Chen就一个人在那里 就是一道又一道题的做 还是非常非常有意思的 我们其他其他同学 有些人就是在 就是把这个数学题变成Lean 然后啊 Ken 他自己其实也没有做出来多少道 就是普特难的题 因为就是研究型数学家

和就是这种打竞赛 在一个最最短时间内的 还是很不一样的 一个数学家的一个特性 你们公司为什么叫原理/公理 我觉得Axiom是非常美的词 就我自己很小的时候 有一本书就是叫数学天书中的证明 就是说如果说上帝有一本书 这本书里面会有哪一些题 数学天书中的证明 就是说有一些这样非常好的数学结果

呃 我觉得就是公理给我的感受就是 首先把它跟Lean这个形式化语言 它是呼应的 就是从一些有限的一些公理中 可以推导出新的一些结果 就像是有地基 然后你再往上建高楼 呃 另外一个我觉得就是 呃 Axiom这个词 我觉得很美 它很数学 它很它很克制 它很理性

它又很sharp 反正我非常喜欢Axiom这个词 它就感觉来自那本天书 对 然后我们公司里 名字开头是a的人也特别多 我们Alex Alberto Armen 反正一堆这名字开头是a的我们是 Axiom 你觉得AI会把数学的历史 推向一个新的阶段吗 会我觉得会 我觉得 其实 非常的让人激动人心的一件事情

就是我随着这个 我们以前的这个世界 能够做到 比较顶尖的数学思维的人是很少的 我们现在会成 从一个math poor到math rich的社会 我们会从一个数学的匮乏 到数学的丰富的 supply

这个供给会会爆炸 这是一个让我个人来说非常激动的 一个野心 就是你想一下 所有没有被解决的理论问题 所有可能说是应用科学家们 他们遇到的 希望有一个数学家帮他们解决的问题 全部可以解决 就是一个 一个时代的 一个时代的

我觉得一个可以被定义 就是说指数级的数学发现的增长 这个我觉得一定一定会发生 然后 数学家们会扮演一个什么样的角色 数学家们 我觉得会扮演的角色 就是他们能够提供最好的直觉 他们会是能够提供到0.01%的直觉 说哪一些数学问题 比起哪一些数学问题 更值得我们去集中算力去解决 就只

我可能会讲一个 这部分会听起来显得我非常激进 我觉得这个就好像说 是很多不同领域的数学家 他们比如说三四十个人 或者说是十几二十个人 会聚起来去谈论说我们的wish list 我们未来希望的这些问题被解决 然后这些问题的重要性 这些问题的连接性 也就是说如果你解决了这个

你应该能够把这一些都解决 这样的这一个过程 可能会是他们的主要的数学工作 然后实际上是由这个AI数学家 去解决这一些问题 嗯 比如说如果我们 这当然是两种情况 我们人类有可能有有限的算力 能够去 我们人类决定花在数学的发现探索上 另外一种情况是

我们其实某种程度上有很多很多的算力 我们可以花无限的算力 在这个数学探索上 这个当然也包括说呃 比如说现在 我们可能能够用更少的算力 做更好的事情 如果是有限的话 数学家其实他们某种程度上 就是这个资源分配者 他们的直觉告诉我们说 我们应该比如说200个 h two hundred花在这道题上 8000 个h two hundred花在这个题上

某种程度上算力就会成为 与 这个数学家对于这个数学题的重要性 某种程度上画一个画一个等号 这是个资源分配问题 如果我们现在在一个无限算力的 这样的一个情境下的话 那就是 像是那个Demis Hassabis那个The Thinking Game 思考游戏那个纪录片里面 有一刻 他在一个这样的一个会议室里面 他说AlphaFold已经就是做出来了

他们刚拿了那个奖 现在下一步是什么呢 他的手下的一个科学家就说 我们做一个平台吧 让这些结构性生物学家可以去 去提交他们希望被折叠的这个蛋白 我们折完了 我们给它发回去 Demis坐在这个桌子上 他就问说有多少个蛋白 然后人家说有200个million 2亿个蛋白 然后Demis就把笔扔在桌子上 然后就说结束会议吧

就是fold everything that was a stupid idea那个平台 为什么你去做一个平台呢 你可以把所有的东西都折了 如果我们在一个无限的算力上 的情况下 我们就要做这件事 我们要把所有能够人类想到的 好奇的数学问题全部解决 所有与应用科学家物理学家 他们就是在意的一些问题 比如说很有意思的一件事情 中国剩余定理

现在被MIT的这个Ila Fiete去用在研究 这个有多少个神经元能够叠起来 这个neurocapacity 这个空间里能够有多少个神经元 这样的一系列的研究中 我们做梦也不会想到 数论 初等数论 会与这个计算机神经科学 理论神经科学产生关系 另外一个例子 比如现在整个的这个法律与经济 这个文献都是两个人

一个是斯坦福法学院的这个Mitch Polinsky 我当时上了他的law and economics 法律经济seminar 然后另外的一个是Steven 他是在这个MIT 我忘了他的last name 但他们两个人就有非常多的 就是关于法律与经济怎么样去想 比如说我有一个刑法 有多少是 用来呃让这个社会不要犯罪 有多少是实际上是对这个人

他个体的某种程度上的修正与惩罚 这个过程可以拿就是 微分方程去探 就是有非常非常多的 我在法学院的时候 就是还帮他算了挺多维分方程 就是能够去去解 就是数学其实可以被应用在这个 Tim Gowers菲尔兹奖 他有一个非常著名的一个 一个话 就是为什么我们国家基金委

什么需要去继续给 纯数学去提供这个经费呢 是因为数学是一个生态系统 你有纯数学你就有应用数学 你这个纯数学如果死了 你应用数学也就没了 你可能确实觉得你作为一个 一个政策上 这些应用数学更与实际的这个市场啊 与社会更有关系 但是 如果你不去做这些基础科学的这个

当然这个也与其他就是学科 比如说生物的基础科学也是一样的 一个论点嘛 就是说你一定要去进行 通过理论层面上的发现 我认为从数学math 然后到code 到这个这个编程去 在软件层面上去做一些 甚至就可以到real world testing 实际世界上的一些验证 数学和代码

某种程度上是孪生兄弟 math is code and code is math math is code因为有一个叫做 Curry Howard呃 对应就是它是一个 Lean就是基于这个 我每一个数学证明 可以变成一个 一个计算机程序 code is math 为什么因为code 现在我们发现 为什么backend 甚至是整个distributed system的web coding 没有办法做到 像就是 做一个网站这样这么好

其实就是因为它有很多的一些 没有办法backtrack 没有办法做很好的 就是hierarchical 就是分级的这种拆解 对这些能力 其实某种程度上数学能够给到它 然后数学和编码的这一对孪生兄弟 是一个 你能够在我们现在这个人类世界上 有这个验证的验证信号的

一个方面 另外一个部分 其实就是 实际世界里的这个实验 对吧 比如我扔一个鸡蛋 它的重力会到这个地上 鸡蛋会碎 就是这些实际世界里给我的reward 所以我觉得我们的AGI的这个world view 就是数学 编程然后 实际的这些是real world testing 然后everything else 嗯 对 你觉得在AI for Math领域

会诞生类似于ChatGPT时刻吗 我觉得会 然后我觉得就是 如果有这样的一个ChatGPT时刻 它 不单只是数学 它一定还会有一个 就是coding代码的这样一个部分 嗯 其实这个事情其实挺有意思 就是我们做的这个东西 很多人觉得是 他对就是验证它有很大的这个意义 然后对另外一些人觉得 这个对超级智能

或者说就是数学推理有很大的意义 它其实某种程度上这两者是是合一的 嗯 这个我觉得比较就是 这是一个可能不太明显的一个点 就是我们是在做一个 就是AI的一个数学家 但是我们又同时是通过形式化证明 加入进传统的 比如说就是LLM推理这里面去做的

所以我们产生的这个输出是可以 比如说几千行 就是Lean的这个代码 然后这个东西它完全可以 就是自我验证 如果我觉得有这样的一个 ChatGPT时刻的话 它某种程度上产品一定要加进来 这是一个 我觉得我们时刻警醒自己 就是作为一个 就是再把这个系统 就是能力建到越好的时候

其实要要记住 就是说某一天 这个东西一定是要尽快的去 产品推出和落地 这是一个点 然后我其实觉得 就是有一个ChatGPT时刻 然后前面可能一般有一个 比如说有点像当时早期的时候 大家说就是AlphaGo时刻 其实我觉得AlphaGo时刻对我来说 是两个时刻 第一个时刻其实可能是这个

在Google DeepMind 2024年拿到的这个28分银牌 另外 对我自己个人的一个AlphaGo时刻 其实是在 嗯 今年的就1月份的时候Axiom Axion-prover Attach to non-goal action file conjecture whether conjecture 包括同时I think就是 就是DeepMind 有一个AlphaEvolve（或FunSearch） 那是一个非形式化的 那是一个

就是自然语言的一个 它也证明了一些研究问题 其实我觉得是这两个时刻吧 一个是奥赛数学 一个是研究数学 你觉得AI for Math它会沿用 就是大语言模型的这一套 整个的技术范式吗 还是会在上面做新的创新啊 我觉得就是它是一个很好的 你想试什么就试什么的一个环境 就是 它是一个 他是一个

他是一个很好的一个设置 就是你可以在上面去试 你认为一些会成功的一些事情 然后这个可能在别的一些没有那么 clean的一个domain上不好做 就是在我们这里 我觉得我们可以做 然后比如说我觉得差不多 AI for Math有一套范式 对吧就是从 draft Sketch and proof开始 2022年的一篇文章 首先呢

你让这个informal的模型给你列个提纲 其次呢你把这个提纲变成formal的 变成Lean的 然后呢你再把这一些中间sorry sorry是Lean里面的一个 一个tactic 一个语法 它这个sorry的意思就是说 我这一块不给你证 但是你知道就是它一定是对的 相当于是让

你把它take it for granted的这样的一个 因为就是第一步就是draft提纲informal 第二步Sketch这个提纲formal 第三步proof 把中间的sorry全填上 其实填sorry有好几种方式可以填 你可以拿这个AI去填就可以 你可以拿一个就是有neural network的 你也可以通过一些 就是原来ATP的那一些纯规则的 没有这个

没有这个rule based的 没有这个AI的 这个去拿这些东西去填 就是让它自动的 比如说Hammer Lean里面有一个东西叫做Hammer 就是Hammer就是顾名思义一个斧头 斧头就是我一斧头下去 这个sorry就没有了 这个Lean 这个Hammer的这个历史其实特别有意思 很早以前其实有其他语言 像Isabelle 是另外的一个定理证明的语言

然后另外一个定理证明的语言 叫做COQ 后面改名叫ROCQ rock 他们就是有Hammer了 就是说有一篇非常 Hammer 我如果记得没有错的话 他是Isabel的一个Hammer Lean里面一直没有一个Hammer 直到我记得去年6月有一篇文章 就是CMU的几个人出来一个Lean Hammer

但是Lean的Hammer他并不足够 它的这个就是功能 并不够涵盖所有其他的Hammer的尝试 所以大家就是 我们当时就有跟Lean的这个创始人 Leonardo de Moura（Leo） 我们Axiom希望能够就是做一个 就是我们 我们给你赞助 你能帮我们找人做一个全部开源的 给所有社区的一个Lean Hammer吗 后来

这个他们可能是人力上就是不够人 他们不是说没有这个资金 所以这个事情没有做成 但是到就是今年的时候 有一个新的一个东西出来了 叫做Grind GRIND 这个其实某种程度上 它能够解决很多的数学的问题 我曾经见过一些其他的AI for Math 数学公司 它有做一些demo 其实那些题 你如果grind了一下

甚至它都能直接给你做出来 这里面没有任何AI的一个成分 我们觉得的这个世界 是AI和这个formal verification 两边 就是两股力量 就是合在一起去解决一道题 就是能够用deterministic 不上这种probabilistic 概率性系统的 我们就是拿这些东西把它解决

然后Lean里面自己能够做出什么样的 抽象层 能解决一些也能尽量解决一些 它就是我觉得一个很好的一种系统设置 就是说先是最简单的最便宜的 能解决就解决掉 然后剩下的再去上这一些 就比较大块的 这些 就是 大语言模型系统 有某种让你觉得非常a ha moment

的时刻吗 我觉得我们每天都是a ha moment 真的吗 这个团队还是挺快的 他们就是其实 我觉得有几个东西 我觉得可能是比较比较前沿 可能就是其他人没有 就是第一个 就是你如果觉得 Monte Carlo tree search 蒙迪卡罗树搜索 太费钱了 就是太效率太低了的话

你有什么别的办法 我们希望能够scale inference 把inference这里去 做大 嗯 这个 我们觉得可以尝试的一个办法 就是可以看一下Anthropic 它有最近讲的一些subagents 这样的一些方向 其实我们觉得subagents用来做AI for Math 其实做的很好 这个是一个

David silver和这个Richard Sutton 他们写过这篇文章 就是AI后半场这个 learning from experience 从经历中进行学习 嗯 这个东西其实某种程度上 在一个数学题里 是一个经历 这个经历就是一个数据的trail 一段 到达 你最终解决这个题目的这一个部分 这个过程

全部可以作为你的这个experience经历 然后 随着你能够让你的这一些subagents 能够应用的skill 而skill就是learning to use tool 学会使用工具 那随着这些种类选择种类变多 你可以去做scaling learning from experience 这些东西我觉得我们做的比较前沿 这是 这是一个我自己个人的一个a ha moment

所以一个树从 比如说40个 40个NODE 40个顶点的一个树 一个证明 就可以把它转化成一个树 这个树从40个 我们已经 scale到4000个 它是一个更深更广的一个树 这是 这是第一个 我觉得我们可能做的不错的一个点 第二个我觉得呃 有一个我们的aha moment 其实是

就是我们发现这个数学的这个定理证明 很好的一个AI theorem prover 能够转化到它很强的代码验证能力 对有一个 我觉得就是在这个Verina Benchmark上的分 我们看到了一个 让我们都很惊讶的一个事情 然后同时可以生成代码和这个证明 其实这是一个很有意思的事

如果你想就是正常的一个代码是Python 然后证明是英语 就是自然语言 那如果你去做就是强化学习的话 你相当于他指着你往两个地方走 你你到底是Python做的好 还是自然语言做的好 但那你如果说是你把这两个目标函数 把它就是聚拢起来 你让你的这个代码 和这个代码的证明 它都是Lean

或者说甚至代码不是Lean 它是rust 它也是一个 对它也是一个 就是linear dependency type theory 这个rush是一个strongly typed language 它可能就能够让它这个收拢 反而能够能有更好的一个verify generation 就是验一边验证一边生成的 这样的一个时刻 这是我觉得第二个 我觉得 我觉得我自己觉得比较美的一个东西 嗯为了更好的理解AI for Math

能不能给大家讲讲 就是在你的心目中 AI for Math它在整个AI的大地图上 它应该画在哪个地方 能够给大家一个mapping AI for Math 我觉得现在就是convert 收敛到大家差不多 其实是一个做法 就是我先拿一个open source的 一个开源的 一个 一个先训好的一个 一个模型

比如说我拿这个Qwen 或者我拿这个这个 这个Qwen的一个模型 然后我在上面去做 做后训练 大家做法不一样 有些人就直接上RL 有些人是SFT 然后RL 然后最后做好了这样的一个model 之后把它就是去 可以说是 放到一个系统里面去 然后这个系统里面

有各种各样的model 有一些model还可以做一些 就是非常specialized的一些东西 然后这一个系统 差不多他去call一些tools 然后这些tools 一些tools其实还蛮难做的 就是要做很多一些lean的meta programming 然后这整个系统的设计 有不同的方法 我觉得差不多是现在是这样的一个

大家其实都是差不多这么做 然后我觉得还是有一点点不同 可能我觉得我们和 像SEA Prover HOList Prover的做法比较类似 嗯然后我觉得好像是 比如说Aristotle 它和这个AlphaProof 以前的那个做法有点类似 其实大概分两派 呃 基本上我们比如说 就是邀请加入我们的同学的 这个AI的

过往的的工作 都是后训练呀 就强化学习啊 然后就是做reasoning 做推理啊 然后也有招一些做agent 甚至swarm of agents的一些同学 然后 就是非常full stack的 这个engineering skill也非常需要 差不多是这样的一个东西 差不多是这样的一个东西 我看了很多研究资料 我会觉得如果AI for Math突破了

它应该不会是只解决Math的问题 它应该是具有泛化性的 这个观点对吗 对 这是一个很有意思的点 我觉得AI for Math 大家其实讲的一般讲一个核心科技 叫做proving 就是证明 其实我觉得AI for Math它能做的东西 也就是说能达到一个更多用处的 其实是一整套东西 我觉得 你需要有一个非常好的一个prover 一个证明的系统

你需要有非常好的一个conjecture 提出猜想 能够提出数学问题的 这样的一个AI 其实某种程度上 这一个能够证明的AI 是你能够提出猜想的 这个AI的reward 就是我能够拿它 去拿这个证明这个prover 去做这个conjecture的这个reward signal 其实有一篇文章叫self-play proving 就是自我 自对弈 自对弈

然后这个其实是 董克凡 马腾宇他们就是这篇文章 斯坦福的一个文章 然后呢 他其实这是其实是所有人开始想 就是conjecture怎么做猜想的模型的 这样的一个起步点 猜想模型的难点是 我不像证明模型 我证明出来了 就是1没证明出来就是0 我没有这个reward了

我怎么去说我这个猜想是好还是不好 然后除了说 拿这个能够证明的这个东西 去做一个grounding 去做一个 去给他这个信号之外 还需要加一些其他的东西 比如说怎么知道你这个猜想 是否在数学上是非常无意义的 比如说你完全猜想出来了 一个不是那么重要的东西

就是一点也不重要 我也不知道为什么 你会让你的prover去证明这个结论 那就可能会有一些东西叫elegance filter elegance filter叫做 去判断这个东西是否优雅 然后在这个STP 这篇文章里面的这个优雅 这个优雅不优雅是靠长度决定的 就一个东西 它的题目与比起它的这个证明来说 是长还是短 这个是优雅不优雅

但是这个感觉上就很粗糙 因为他们 其实他们的那个数据集是叫Lean Workbook 是一个比较是高中数学的一个 一个数据集 完全 这个东西如果做到更高级的 比如说本科 或者说是就是博士研究的的话 你没有办法去靠这个长度来 就是绝对作为一个唯一的 一个优雅的一个过滤 对 没有没有

没有 就是没有特别 没有特别强的延展 延展就是难度 提高的时候 这篇文章不足够 嗯 所以就是怎么去做 这个 这个猜想 目前是一个 我觉得比较就是前沿的一个研究问题 然后这个猜想的这个 猜想家和这个证明家 他们俩就是要聊天 他们俩就是通过 通过就可以self improving

就可以自我提升 然后 他们还有一个很重要的一个部分 是叫做 尤其是我们在做形式化数学证明 叫做就是 知识库 这个知识库为什么很重要 是因为大部分就是存在的数学 在英语里面存在的数学 或者在中文里面存在的数学 它都不存在Lean里面 它连定义都不在Lean里面 所以说我需要一个很好的去

我需要两件事情 第一个我需要能够很好的搜索 什么是已知的 已经被证明的 什么是需要被证明的 然后或者说 甚至说如果你让我证明一个东西 我在已知的里面找到一个反例 那我就直接可以证伪 对吗 然后另外一个需要的就是说 把这一些浩如烟海的数学 转化为形式化的数据 转化为形式化的数据的话

这个过程就是我说的第二个核心科技 叫做auto formalization 它就不是证明了 它是转化 嗯 它这个转化 其实某种程度上 一是被忽略了 因为大家 比如说 你如果证明了很多普特南的问题 或者IMO的问题 你就可以到Twitter上 你就会说 嗨 我证明了 我是一个非常伟大的AI数学家

但是如果你只是把这个人类 已经就是发现了的 写好了的数学 转化为了这个形式化的 你会得到更少的这个赞美 但是这个科技 它其实比这个证明要更难 至少是一样的难度 我其实觉得是更难 为什么更难 就是 如果说我要求比较严格

我的输入是一个arXiv上的数学文章 而我的输出要求是 把这个数学文章里面所有的定理 证明的这个对 这一对东西变成Lean的 这个代码 成为了我的一个Lean的这个输出 那我需要几步 我第一步 我需要把这个文章变成拆分 我要拆分出什么是 什么是

就是单个的定理和这个证明 有一些文章 它结构性的比较好拆 但有一些文章 一个大的证明里面 可能能拆出好多东西 这个东西如果拆的不够细的话 拆的非常细的这个东西叫做什么 叫blueprint 蓝图 陶哲轩 还有说是 Kevin Buzzerd呀 Alexander Rowe 这一些数学家们 他们用人手写出过蓝图

他们曾经就是在polymath 还有就是后面的一些 大型的形式化的这个项目上 他们人手写了这个蓝图之后 丢出去 给全世界的本科的一些数学的 这些学生去 每个人领一个小任务 然后所有这些人小任务加起来 星星之火可以燎原 就整个的这个东西就形式化

就写好了 嗯 然后 如果你需要让一个计算机 不管是AI 还是一个就是rule-based的一个电脑系统 去进行把一个从一个PDF 一个arXiv PDF 到这一个非常细的蓝图拆分 譬如说20页的一个文章 变成一个200页500页的 这样的一个蓝图拆分

使得我能够把这一些蓝图 非常细化的东西 转化为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里面 你如果去看它这个怎么一个程序 是怎么写出来的 其实还蛮有逻辑性的 它对一些逻辑推理的一些处理 还比较好啊

作为一个就是 自动化形式化证明语言 它有一些兄弟姐妹 它又有一些其他的这些语言 比如说HOL4 Coq Isabelle 甚至原来更老的一些SMT SAT 这些都是就是基于逻辑的 就是证明语言 然后我们现在这个世界上

我们所有的芯片的一些验证 基本上要用Cadence这个公司 Jasper Jasper是一个基于SMT的 一个语言 然后Jasper就有很多的局限性 就会有一个很有意思的问题 或者说我们可以头脑风暴 如果全世界的SNT 挣扎着的struggle的SSNT 全部可以被被Lean代替 我们会是一个什么样的世界 然后又另外的一一层问题

是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 也就是这个证明 而Axiom做的是这个proof的这个部分

然后能够 所以其实但是你你要看就是program 对吧 就是我们可以 现在很多AI可以写很多的 这些就是电脑程序 这个specification反而变成了难点 verification condition这个东西 就是做这些形式化语言的这些 他们给我们提供了我们解决proof 这中间差的就是这个specification 任何你能

所以这个这个梦想就是像数学一样 我举一个数学的例子 任何我能写成一个数学问题的问题 都会被证明 嗯 在这个coding里面就是 任何能够定义的都能够被 被做出来 被执行 如果难点是specification 它应该怎么解决 唉 这就是为什么说在这个数学里面 这个猜想很难

就是做这个conjecture 猜想家这一块很难 这其实是难点 定义与猜想是难点就是 定义 比如说我 比如说 我们之前有一个很火的叫first proof的 一个挑战 对吧 有一些数学家 他们跟还上纽约时报 就是讲说 给AI出10道题 这个OpenAI做了好像做了5道 也不知道对不对 然后这个DeepMind做了6道 好像是对的

他们当然都是拿这个自然语言做的 为什么比如说我们Axiom 就没有办法去参加这个挑战呢 因为这10道题 我甚至都没有办法把它转化成Lean 这个就题目 我放不到Lean里面 为什么我题目放不到Lean里面 题目涉及了很多定义 这些定义完全不在 不在这一些 就是library不在这个math lab里面 然后我如果要去定义这些的话

这一步目前 机器很难做 所以由于我无法定义 导致我无法证明 所以这是这是我目前觉得的第一个 第一个难点 然后在在这个定义之上 当然也就是这个命题 对吧 所以 我们还是希望的一个未来是 当然一定是有局限性 比如说我们知道 就是从我们那两道没做出来的题 比如floating point这个 这个非常难做

这有一些就是计算机程序的 这个任务非常难 难去拿我们这个Lean去进行验证 但现在大家都有尝试去 各种各样的方法 让就是不能够验证的那一些 那一些情况变得越来越少 其实我问这个问题是想说AI for Math 它是一个更垂直领域的一个AI的事情 是的 还是说它

能够泛化成一种通用的智能 它泛化会泛化的 比你这个垂直感受到的效果更慢 也更不那么戏剧化 我觉得在垂直领域上 我觉得 是有可能有一个Cursor like moment的 你能够感到就是 就是你能有那种感受 然后某种程度上 呃 它和就是通用的智能有一些关系 但在某一些情况下

肯定是某种程度上 他们还是在战斗的 比如说我们发现就是数学做的好的AI 这个跟人谈话就听起来非常傻 就是好像 这些 这些性能是在互相互相相斥的 但是比如说从数学到代码生成 从数学到这些代码芯片验证 这些很明显是转化的

你说的这个Cursor like moment 它会是一种更产品化的moment吗 在数学这个领域 其实某种程度上我觉得是一个概念 我觉得好的产品 其实 它是来源于一个比较深的一个概念 就是1980年的时候 我们知道1980年代Donald Knuth 这一个计算机学家 他提出的是什么事情 他提出的就是 我希望让所有能够呃

希望让所有计算机科学家都能够 Vibe code整个所有的事情 我能够像数学家一样 在自然语言里面去做 推理 然后这个电脑就直接执行 但不单只是我们现在讲的这个vibe code 因为我们现在还有code review 他希望能够把这一些 直接代码直接到这个deployment 直接可以ship

然后我们目前可以在前端做 但我们后端做不了整个的这个系统 我们也很难vibe code 比如说我怎么vibe code 一个control flow 我很难去 很难去做这件事情 嗯 这是一个梦想 比如说你可以猜一猜 第一个提出形式化证明的这个人是谁 其实比这个Donald Knuth还要更早 就是就是艾伦图灵 他就是讲说

我就是希望我能够一边编程 这个编程完全背后的这个逻辑 不单只是这个逻辑 就是它完全能够与我的这一个 想解决的问题完美的这个 这个契合 而不是依赖于有限个 测试的这个输入输出对 但是我这有限个输入输出对 它其实是有它的 有它的好处了 你知道它能帮我什么吗

它能够帮我去specification 它可以帮我去做 这个定义 就是我比如说小珺 你给了我一道题让我去 就是去编一个程 比如你让我做一个排序 我把这个排序的题怎么样 从一个英语的题转化成一个 在我这个Lean里面的这样的一道题 就是这个过程 由于我还没有去解决出 也没有去证明出这个Lean的这个

这个命题 我需要这些输入输出的东西 来帮我去做一个验证的信号 嗯 我在想 因为Cursor他这个moment 他是让很多不会编程的人 也能够做了 那你说的这个math领域的Cursor moment 是不是会让更多不会做 这么高等数学的人 也会做数学了呢 我们可以用它做什么呢 呃 我们可以拿它

如说我们公司 有一些同学 他们以前做过芯片硬件 大部分同学没有做过芯片硬件 我们现在可以去用Lean去 证明芯片的性质 所以它还是一个非常专业化的 有一个专业门槛的人去做这个事情 不是不是 我们 我们公司的 呃呃

一般的软件工程师可以去拿Lean去 去知道一个芯片是对的 对 我觉得我表达有问题 我想说的是 还是一个非常有专业需求的一个事情 对吧 因为不是每个人都需要 就可能更多人需要编程 但是并不是每个人都需要 去证明一个芯片的性能 嗯 我觉得就是在这些芯片的领域上 由于可能说之前做不到

可能之前的解法是这个SMT 这个就是基于SMT的解法做不到 嗯 我觉得就是在 呃 我们比如说每一天就是更consumer 更day to day 或者prosumer的这样的这个市场上 可以就是以下的一个想法 就是你一边编程的时候 你一边就是它告诉你 整个编程不需要任何test case

已经完全解决了这个coding问题 这个我觉得会是有意义的 嗯 我只是觉得在一些芯片这些领域上 它目前就是感觉这个痛点更大 比如说这个亚马逊 在过去的 它有一个世界上最好的 自动推理 automated reasoning（自动推理） 自动推理团队之一 没有没有AI的 就是那个

它有很多的这个 形式化语言的这些专家 他们花了3-5年去写了 26万行定理证明的这个代码 去验证他们的 这我实在不知道怎么说 一个 用于去最适化CPU处理的一个hypervisor 一个工程 工程的一个东西 它的一个component memory记忆

memory isolation component（内存隔离组件） 我不太会说这个中文 它去确定这个东西写的是对的 它花了三年 人写了26万行 这个 这个AI没有改善这些工程师的生活 AI没有 改善那些必须要手把手教着这个 这些几千多个license的 去验证芯片的这些人的生活 我觉得

呃 就是可以在这些领域上 你会有更好的pricing power（定价权） 你会有更好的定价格的这个 这个空间 作为我们这一个 呃 我们的公司 这个提供方 科技提供方 呃 但是我们觉得就是在更广泛的 每一个人都要Coding的这个 这个情况下 我们会意识到verify generation的重要性 就你会希望某一天

在我要一个call action 要一个函数的时候 它给你是100%不需要验证的函数 嗯 所以这 也算是你们之后可能会探索的 商业模式 我们觉得就是 验证是我们最好的第一个市场 这个市场会在什么时候打开啊 你预计就什么时候 是你们要做商业的时候 呃 我觉得我们 就是我们还是比较坚信 说就是专注 就是说

这一些比较顶尖的这些科技人才 要继续把我们的这个系统的这个能力 往前变强 但我们同时又觉得说可以去 开始进行这些小的探索尝试 且某种程度上就是 你如果就是有更多的资源 然后能够有更多的人在这个团队里 能做的事情就可以越多 嗯 所以我们 其实我们还比较某种程度上 有点好奇心驱动的去想这个商业模式 我们其实还挺好奇

这个东西它能证明哪一些 芯片性质 电路性质 它不能够证明哪一些 它能够去 去证明哪一些程序 不能够证明哪一些 我们其实更关注 就是它不能做的这件事情 然后其实我们觉得 去解决一个有意义的失败 比很多个肤浅的成功来的更有价值 嗯 对 有时候在我们讨论大语言模型的时候 我们会说语言是模型的一个拐杖

对 数学是吗 数学是 然后没有之前大家把数学当语言了 就是把数学当语言来做拐杖 这个我觉得不对 我觉得就是真的是要把数学变成Lean 这个它就能够成为一个 就是更另外的 这样的一个很重要的一个拐杖 嗯 所以它是独立于语言之外的关系 数学跟语言应该是平行的关系 某种程度上是的 我们可以看到

甚至在我们的系统里面就是更偏 有一些问题更适合偏语言的解决 比如说你列出这个提纲 就是很大的一个部分的胜利 那进度条就到了很多 嗯 另外的 比如说适合 就纯粹的 在这个形式化空间里面去证明 嗯 他肯定是相辅相成的 我们其实觉得挺有意思的一个点 就是一个形式化 做的很好的一个模型系统

它 它能够比如说在这个芯片验证上 做的比一个更多语言一点的 要做的更好 但是在一些其他的 比如说这个通用的 这个代码生成的 这样的一个情况下 嗯 是我需要 我也需要 就是语言这一块的 因为我需要理解这个用户 他可能无法自我表述的很清楚的需求 我们觉得把这个语言的这个部分

和这个Lean的这部分放在一块 最有意思 嗯 你们是基于大语言模型的吗 我们这个系统里面有不同的模型 这些模型 他们一般就是 经过了大语言模型之后的后训练 然后是以数据为主 Lean为主 以Lean为主 就是输出都是Lean 它的目标是输出 就是Lean代码 然后Lean代码它自己带这个程序语言 自己带了这个验证的这个性质 所以就是这个有意思点

就是假设我 我什么都不懂 密钥学 我完全不知道密钥学是什么 然后你写了一篇密钥学的文章 然后你把这个密钥学的文章就是 就是你写的英语的这个文章 里面包括一些数学符号 你打印了 然后你给我看 我是看不懂 我也不知道你写的对不对 但是呢 你这个密钥学的文章 可以通过AxiomProver把它变成Lean 然后我不需要看得懂 我只要把它一跑

我看到一个勾 我就知道你这个密钥学的文章是对的 嗯 这是一个很有意思的点 是一个很好的验证过程 对我们 我们我们接受了 我们盲目的接受了 这个非常强大的AI会犯错误 但是我们相信在一些领域上 这些错误将极度的昂贵 我们相信能够去做一个尽量perfect的AI 所以它能

相对于 就是在现有的AI之下 它可以帮助解决幻觉的问题吗 对 帮助解决幻觉的问题 解决所有的幻觉问题 还是只能解决一部分 会有两种情况 它要么就说这个事太难了 我做不到 要么它会给你一个正确的东西 所以可能是语言是突破边界的那个 数学是在把它往回收的那个约束 对 其实在某种程度上

我其实觉得人类 比如说好的直觉是什么 好的直觉其实就是一个配比 配比其实就是幻觉和这个 规律 规律推导的这个pattern matching 和幻觉的一个配比 这个配比要合适 其实某种程度上 语言能够做很好的conjecture 这个猜想家

我觉得其实跟语言它会有一些很 它会很需要借助一个很好的语言系统 它可以帮你去突破这个边界 然后这个某种程度上generation就是生成 然后verification验证 这两个就是一个来回的 这样的一个过程 嗯 但我们又有其他的方式 可以去突破边界 并不一定非是要语言模型 比如说像François Charton

和Guillaume Lample 他们这一个数学发现 AI for Math discovery的这些工作 他们是通过去找有意思的数学物品 物品object 数学的东西 嗯 去例子 去尝试 去找到一些直觉 然后去把它变成一个猜想的 比如说我有很多很多的图 我可以让它再做一些 local本地和global 整个图 全图的这些

这些 扰动 我可以用这些方式去突破边界 然后我 甚至比如说另外一些方式做猜想 我可以去 我可以去看一下 怎么样去做一个 可以做embedding 然后可以去做 一些其他的方式 也可以去根据这个语言的这些相似性 反正有很多东西可以做 但它确实是跟语言更相关 然后 而证明是跟

证明其实跟两者都有关系 嗯 对 你们接下来的一些 就是想要达到的目标会是什么样的 对 我们现在 所以是还 当它成阶梯式对向前推进的时候 我们希望能够 我们也解决了一些研究问题 我们解决了交换代数的 代数几何的 然后 代数数论的 然后还有 是啊一个比较更理想数学 比如 组合概率意味的

我们解决了这些问题 我们希望能够选一些去 目前Lean没有多少这个定义的这些领域 比如我们希望能够看一下动力系统 我们希望能看一下这种 概率和随机曲面 我们希望看一下 没有这个基础建设的这一些地方 我们能不能去解决一些问题 我们想知道这个前沿到底在哪里 我们本来不知道 我们大概两两个月 我们就把高中的那个基准级

mini f to f 这个也确实是一个比较古老 也被打得千疮百孔 估计不知道多少人训练 在它上面训练的 一个基准级 就把它 就是饱和了 然后接下来饱和了普特南 然后接下来就饱和了 这个 这个 这个代码 就是验证的这个基准集 然后我们在研究层面上比较缺基准集 说实话

因为没有多少就是研究级数学的 这个Benchmark题不好找 然后所以我们只能说 找一些未解决的这些问题 在每个领域找那么两三个试一试 现在希望能找一些 完全看起来没什么希望的领域 这个可能花的时间会长一些 我觉得接下来就是就是A轮之后 就是我觉得希望 嗯 我们可能会更多的往工程 研究上这里去 去转换

可能解决一些光是工程没有办法 不足以就是摘起来的这一些 这一些low hanging fruit 嗯对 数学家的意义是不是在出题上 他要 数学家 很大程度 很大程度 我们的数学家的意义在出题上 嗯 对 我觉得他们 因为 尤其你现在机器出题出的不怎么样 刚才讲这个猜想家非常糟糕 目前的表现

所以就是确实需要人出题 但出题非常难 我们现在 比如说我们要到哪里去找 比如说800道就是未解的 研究题呢 你 你一个教授有这个题 你是给我们还是给他的这个学生呢 就是这 这是一个非常复杂的一个过程 所以我们 也是希望 能够去通过我们的数学家的网络去 大家去看

有没有题愿意给这个AI试一试吧 嗯 你们想把它往哪个方向引导啊 作为出题的人啊 我觉得它一定是要 就是满足一个以下的这个性质 就是 它一定要就是robust to distribution shift 就是说不管你是哪一个领域的啊 这个它都能做一点 它不能是一个只做 因为你要比如说只做欧式几何 那你就是一个几何 几何引擎 对吧

你希望它能够做更多的领域 尤其是那一些 目前没有基础定义的领域的 的数学题 我想让这个东西去做一个代数数论 代数数论里面很多的东西 其实都在这个 Math这个图书馆里面 已经这个定义已经打好了 我只要就是我 就很容易的就可以去写出我的命题

如果你连定义都没有 譬如说在这个动力系统 或者说是一些比较高级的组合 它就没有这个定义 我连这个题写都写不出来 这就是这个first proof 这10道题的这个挑战 我们很难去 甚至尝试的这样的一个问题 目前这个这个能力 那你可以说为什么 就像你拿AI做猜想 你能不能让AI去写定义呢 AI写定义的能力

它们这个 这个社区管它叫library learning 就是图书馆学习 图书馆学习能力 大概的意思就是说 让这个机器能够去搭出一个图书馆 也就是说从定义 包括上面的定理 包括上面的去证明这些定理 然后去衍生出新的定理加更多的定义 这个过程是一个建筑理论的这个过程 这个蛮难的 就是所以说

library learning 是一个大家目前可能卡在 卡在这里的一个地方 因为我也不知道这个定义 我首先我很难给它验证信号 我没有办法说这个定义是对还是错 向我一个证明 这是一个点 然后另外一个点就是是否是faithful的 faithful的意思就是说 是否与我这个人类给出的 人类在数学里面 已经创造出来的定义相同的 如果未来

这些人类的定义都已经被 假设我们全世界的人类就是无穷猴子定理 无限猴子定理 我们什么都不干了 我们就把人类的数学全部打成 这些定义 全部打进Lean 假设就是上帝给了所有的 已经存在的这个定义 做在Lean里面了 就会出现一个问题 就是当这个 当这个系统要做新的猜想

与新的证明的时候 它会发现我可能引入一些新的定义 能够让我的生活变得更容易 但是在这样的一个情况下 如果那个定义是一个人类没有 没有写过的一个定义的话 我怎么样能够保证 这个系统的这些定义不相违背 嗯 因为我 我可以定义一个图是好图 然后过了一会之后 就会发现

这个东西可能会呈现一个悖论 在这样的一个情形下 其实是是比较棘手的 嗯 对 就是这些都是比较 就是比较远的的研究问题 但是我们最近我们会在想的事情 如果AI for Math实现了AGI 嗯 你觉得它的标准是什么 它能实现什么 哎 Demis 他有一个 Demis Hassabis 他有一个非常著名的

就是说你把这个AI训练到1910 1911年 看它能不能就是去发明 发现广义相对论 呃 这是一个很有意思的一个定义 首先我觉得我不太喜欢AGI这个词 我觉得我们可能更是做ASI 就是确实这个 我们不能够去生成 我们做的数学是general的

数学它并不一定是那么general的 它不一定能带来泛化 我是这样想的 就是我是这样想的 就是我们 比如说有一个盘子 其实我和之前的一个同学 就是我和任宏宇聊过这件事 就是中间你是一个点 就是1+1=2 然后打印hello world 所有的这些非常简单的这些任务 在这个盘子

我们当时还真在一个中餐馆 这个盘子的外缘是 比如说证明黎曼猜想 找出治疗癌症的秘方 的方法 然后 写出一个像莎士比亚一样的 或者说像能够拿诺贝尔文学奖的著作 所有的这些 就是人类的 超人类的任务 嗯 就是有一些

就前沿的这些 这些实验室 像OpenAI他们 他们想法说我 一点一点的 我要做AGI AGI什么意思 就是我 我一点一点的把这个圆环撑大撑大 最终我到我 我 我接触到了所有的这个边界 嗯 我们不是 我们是 我们从这 然后往这个证明林曼猜想这打 我们就往数学 这个代表数学的这个超人类任务打 打完了之后

我们觉得它会发散出一个扇形 就是可能说这有个代码验证 这有个物理 我是发散出一个扇形 我绝对不会覆盖到这个 拿诺贝尔文学奖这里 但是我会有一个比较大的扇形 而我这个大的扇形 在我这个B2B的这个市场上 是有意义的 这是我们的一个想法 所以我们觉得它是一个ASI 其实人类的文明 ASI ASI就是 区别 ASI我觉得是

Specialized Super Intelligent AGI就是general 当然s一般大家意思是Super Intelligent 对 我觉得 我觉得Super Intelligent就应该是Specialized 这是我的一个hot take 那为什么呀 听起来ASI应该在AGI之上 那比如说我 我讲一个例子 譬如说就是我 可能我数学还可以吧 我自己都不会做饭洗衣服 就是 就是人类的这个智能 也不一定多general

OK 嗯嗯 那有没有可能AGI实现的非常好 他把你这个也取代了 这有可能 但我觉得我会更快啊 我觉得就我们现在看到 比如说拿这个强化学习 做到这个coding上 我们看到的就是take off 我们看到 因为你拿强化学习能把coding做出来 我觉得code verification 我们在做的是很重要的一环 所有这些东西做好之后 就是你有这个基于 你有 既有这个数学去做这些algorithm的能力

又有 如果把猜想能做出来 你就能够达到一件事情 叫做recursive self improvement recursive self improvement 是一个我们包括很多其他人 都非常相信的一件事情 我相信这个大家也很熟悉 就是说你就可以持续螺旋上升 就是 我希望你一个世界就是AI AI scientist AI engineer engineer OK 然后这个过程中 我觉得Axiom一定是其中的一环 嗯

但它肯定是 它不是整个的生态系统 而其中一环 嗯 所以AI for Math的尽头可能是一个 AI for Math 是一个 我觉得AI for Math 它比较哲学的一个看法是这样的 就是AI for Math能带来很多的东西 它能够带来你非常的smart 它也能带来你非常的right 也就是说

它既能够带来一个超人类的一个表现 也就是我们可以看到 甚至像OpenAI 他们能够做的AI for Math也做的很好 但是另外一个很重要的是 它能够给你grounding 它能保证你的100%正确 所以在这两个象限向上再往上推 然后我觉得AI for Math是我们公司的 这个DNA或者 math是我们的公司的DNA 验证是第一个市场 可能未来会有一个市场是AI for science

所有科学 他们需要的这个理论发现 可能未来还会有一个市场是最适化 就是 最直化optimization 就是某种程度上 我们经常讲一个词叫就是diminishing return 就是说我花了很多的力气 我最后就只有那么一点的收益 所以不值当 但这个世界其实很多程度上并不是 是 diminishing return的反面是这种沉没性付出

沉默性付出成本的反面 是你最后花的 你花了很多很多的力气 你能够带来非常大的 最后那一个mile 会有非常大的一个收益 某种程度上 比如说能够去把所有的edge case 边缘性情况都都覆盖的搜索引擎 比如说像Google 它就会赢得这个搜索的这个市场 然后比如说像 我们 一些文艺工作者们

他们能够就是好和非常好的 这个区别是天差地别的 所以在某种程度上 我觉得 像验证一个这种边缘情况 很很耗费很多的钱和人力 和很多这些资源 和这种比如说最最值化 我需要 目前大家花了很多的 工业界的资源 去探索这个 小数点后1,000位是什么 比起小数点后第三位是什么 虽然在一些其他的情境下

小数点第3位比小数点第1,000位要有 要有意义 但某种程度上 我们既需要 我们是需要 既需要这个medium 又需要这个outlier 数学我觉得给了这样一种一种DNA 我很好奇啊 你们公司 就是有数学家的公司 和你那个竞争对手 它不要数学家的 对 DNA区别会是什么 我觉得我们公司既要数学家 我们还要一个 他们不要的 就我们

我们要很多就是代码生成的人 就我们有很多就是编译器代码生成的 这些同学 我们其实我们相信多元产生智能 其实有有两句话是 多元产生智能 多元产生智能 就两句话 我比较相信 一个就是降维打击 另一个是多元智能 就是 我们觉得就是 这是为什么 我们 比如说你刚才说AI for Math的意义是什么 AI for Math它其实在探索 推理的一些非常难的问题

它某种程度上能够呃 与其说是泛化 不如说是 比如说你现在有 你有一个1兆这个 这个字符串 这个爬虫 爬虫的数据 然后你很明显很难 就是你 基本上通过就是 嗯 pattern就是这个规律的 这个找寻 能够做很多的事情了 你很难撞墙

你很难碰壁 但如果在数学这一个 就是目前Lean data非常少的一个情况下 你动不动就能够遇到一些就是拦路虎 所以你 hit这些roadblock是更快的 所以 某种程度上 我觉得我们做一个更难的事情 希望能够垂直下来 给其他的一些领域 就是某种程度上能够去 去 去降维打击 我讲这件事情的原因是

比如说我们现在AxiomProver 能够生成一个20页的一个数学证明 对吗 我然后我可以非常快的去验证一个 目前在芯片验证领域 是一个比较复杂的一个puzzle 因为那一些需要的是一些比较 可能说高中数学家 高中数学学生 或者初中数学 学生会的枚举法 分类讨论 而不是什么like 我想想 不是什么numerical（数值的）

numerical like semigroup 对 然后 嗯 这是 这是我的一个想法 嗯 哦 我刚才说三个 不好意思 我 我说忘了一个 就是三个 这三 三个背景的人 他们 联合起来 其实呢有很多想法 比如说AI和这个 就是有这种compiler背景的人 他们可以用一些方法 去做很多的synthetic data generation 去做这个

合成 不是合成 不叫合成数据 就是拿AI去生成这个Lean data 而不是靠人去去打这个Lean 因为你想 就是我去找一个数据提供商 比如说我们Mathlib Turing这一些 做这个数据商 他们可能就整个平台25个专家 然后可能Lean打的不怎么样 那我这个东西 是没有办法 去大规模的去做的 所以我必须要拿AI去做 那怎么样 拿AI 所以需要代码生成

我可以用fusing 我可以用repair 我可以用就是failure categorize 我可以有很多很多的方式 是这些人能够给我们的不同的视角 AI和数学 这里当然也有很多 我可以想 就是 正向推理 反向推理叫forward and backward conjecturing 我可以去想 很多一个数学家如何去 呃 有点像当时就是早期棋类的expert system 所有这些东西可以连在一起 总觉得我们是一个idea rich的一个公司 就我们有很多很多很好的想法

然后我们人不够去执行它 我所以我们现在 我们十二月份 的时候 当时Ken加入了 十五号员工 现在已经30人了 嗯 竞争对手多少人啊 不知道 好像50-75吧 还是比我们大 怎么理解 数学是现实世界的沙盒 数学是现实世界的沙盒 因为你既有验证的这个信号

又能够有更规律性的描述 更结构性的数据 某种程度上 我 比如说我们要在生活里 咱们俩现在来想个猜想 嗯 然后咱们俩再把这个猜想证明 我好像只能想到一个数学猜想 和数学证明 不然的话 我们可以说猜想一些生物的东西 然后来一个实验室 去做一些动物实验

这个任何与现实世界更有关的 这一些验证的过程 其实可能会比数学的这一个比较 简明的这个沙盒要 要困难和复杂的多 也就是我为什么非常就是 respect 我的一些朋友们 他们在做就是AI for science的公司 比如说Periodic Labs Liam Fedus他们在做 然后原来是叫Future House 现在叫Edison

这个Sam Rodriguez是我们MIT的这个校友 他们在做 就是一个AI scientist 嗯 很多人在做各种各样的 这一些尝试 但是就是如果你想要很快的一个验证 然后你又希望又能计算又有逻辑 我觉得数学和代码是好的选项 嗯 对 AI for science和AI for Math 它不是一个overlap的赛道对吗

不太是 我们 我们能AI for science 他们其实很多在比的是 这个iteration circle（迭代周期） 这个有多快 因为你想 如果他们出现了wet lab（湿实验室） 出现了实验室 这个 我身边很多朋友 各种各样的实验室 知道这个 Leila Sciences 这个公司 George Church的那个公司 他们有什么 Robot实验室 机器人实验室

这个听起来非常的 非常的 非常的自动化 但是他们所需要做的 前期的投入是很多的 LinkedIn feed他们最近这实验室又搞起来 又有其他的一些实验室 像Madrid Michelle Li 他们都有很多的 他们是一个赛道 我们某种程度上 如果他们有想要我们解解决的 一些理论上的一些 一些问题 我们希望能够帮他们解决 但我们某种程度上

只停留在一个数字世界 我们不走到他们这个实际世界去 嗯 但是你可以帮助 AI for science 你也可以帮助 大语言模型 对 就是 其实你们是一个拐杖 是一个工具 对对 我们觉得也不能算是 我们是拐杖和工具 比如说 我们可以去验证他们生成的代码 来帮他们减少幻觉 这个蛮重要的 我们可以去 我希望的一个世界是

每一个就是物理学家 他们都有能够找到他们的理论 物理学家 就是 他们都能够 每一个神经 神经科学 就是做一些真正是动物实验的人 都能够找到他们的 这些理论的 这些计算神经科学学家 而这些 过去数学家们 他们停留在 比如说自己的学术圈子里面

他们可能去 很少的一些合作 他们很少去与这些 这些应用科学家进行合作 我觉得 未来就是希望能够Axiom的AI数学家 能够去帮这些AI for science的这一些 科学的这一些探索 去解决一些理论上的问题 嗯 然后他们可以去进 在实际的生活中去做 去做验证 你刚才说了很多AI for Math

它能作为验证的手段 那他能有一天像一个天才 你走形式化证明 你就有验证 如果你不走形式化证明 就没有验证 你们现在走的是形式化 我们走形式化 嗯 那如果不走形式化证明 它通往的是哪里呢 不走形式化证明 它可能是 我觉得可以去尝试 我觉得就是它可以尝试

尝试一些怎么样做通用的推理吧 我觉得 AI for Math 有可能有一天 像一个天才型的数学家一样 提出非常好的问题 有非常好的直觉 它能成为那个创造的人吗 这个最难做的这个部分 但是我觉得 可能 我们和那个竞争对手的一个区别是 我们打算做这件事 而他们不太打算 哦对 他们好像直接要落地了 对 他们落地成什么 就是

他们打算直接做这些商业的这个东西 他们觉得IMO金牌 可能就是就是这个终局了 就是可以 就我们还是希望 我们真的能希望把猜想做出来 这个我觉得我们目前 有很多的一些试验和探索 然后也碰了 碰了不少 碰了一鼻子灰 对但是我觉得这个 碰了什么一鼻子灰 就是就是有做不出来的情况 比如说就失败了 你这个失败到底是

当时我记得 这个失败发生的时候 我们的这个证明家还做的不太好 所以我们分不清到底是哪一块出了 出了问题 呃 有很多的这些想法都可以去做 但是我觉得我们要做这个猜想之前 希望能够把我刚才说的这个核心科技2 也就是把这个转化能够做好 这个auto formalization 把这个自然语言到Lean这个转化 我们希望能做好

我们觉得能做好这个的话 能够有更大的 这是一个能拿更多数据的手段 又本身能够对证明做 做一个很好的一个帮助 然后我们才会去做这个猜想 嗯 当然 我们现在可能也在做一点 但是就没有完全的Ramp up（全面推进） 没有说整个公司打猜想 嗯 猜想是数学最有魅力的地方 是吗 猜想其实是 就比如我

作为一个数学的一个学者 我是很难 我很难去提一个好的猜想 然后比如说给到 比如说假设说现在有一个reading course 有一个本科的一个大一的同学 希望能拿一道题 对吧 作为一个reading course最终的一个 我觉得我很难给到这样一个题 就我觉得需要 猜想所需要的数学能力 是蛮难的 所以我们特别高兴

就是Ken能够加入我们 其实他是 他是非常 他是猜想家 他 他是高产的猜想家 他跟拉马努金的关系是什么 我听说的故事是这样的 首先故事一 就是他的父亲 当时一群要筹钱 众筹给拉玛努金修这个 在印度修这个雕像的数学家之一 他的父亲是一个非常

非常出名的 著名的一个 一个杰出的一个数数学家 也是做数论 当时是印度政府 要给这个拉马努金立一个雕像 但最终没有实现 于是这个拉玛努金的遗孀 这个女士 她就给这个拉玛努金的合作者 世界各地数学家写信 于是她们就是一起去做的 然后她还回了信 就是建成这个雕像之后

所以Ken的办公室里现在还有一个 他父亲给他的 留下来的就是拉玛努金的遗孀 写的这一封信 然后另外的故事二 就是当Ken 他是一个 我印象中 当他是一个本科生 他好像是在芝加哥大学 他当时 就是有很多的社团活动 然后可能课业呢 也没有特别 占据他所有的时间

所以他的绩点也不是特别好 然后他好像高中也没有毕业 反正就是 是吗 对 反正就 他就是一个非常叛逆的一个少年 然后他的父亲 就是拿拉马努金的故事勉励他 就任何时候开始也不算晚 你不需要像你的这些 已经上了多少数学课的同学一样 你才能够做数学 你完全可以自己现在去去追赶上来

于是他进入了他的这个数学博士项目之后 就开始非常非常努力 然后就是做了很多 非常好的数论研究 对 Ken的父亲也是前不久 今年年头 去年年底去世了 所以也是非常值得纪念的一个 一个数学泰斗之一 他的兄弟们 都非常的

就他来自一个数学世家 他的两个兄弟 一个是著名的小提琴 还是中提琴 某个提琴家 另外一个原来是密歇根大学的校长 对 他和拉马努金 都被认为是那种直觉型的数学家 对不对 我觉得就是 拉马努金是更尖锐的直觉型 解题型

而Ken 我觉得他是擅长 他提出猜想的方式 是连接很多不同的视角 是一个发散型思维的人 他不是那种 这就是一个公式 这个东西一定是对的啊 那是拉马努金 所以我在想 如果AI做的是验证的这个事情 是形式化数学 那它其实训练的

是一个更能验证的人 而像拉马努金这样的天才 他能够被AI训练出来 那他会不会是两种类型 这是一个很好的问题 大家说拉马努金为什么就是essential AI 也就是当时这个 Transformer paper attention is all you need 你需要的只是注意力 这个注意力机制 这一篇文章的这个作者叫Ashish 他有一个公司叫Essential

Essential是做Pre training先训练那个公司 他们先训练的一个模型就叫拉玛努金 人家说拉玛努金的那种浑然天成 那种直觉 其实是 有可能是预训练的产物 所以我们现在 没有做预训练 我们现在主要做的是后训练 我们有一天可能会做中训练 但我们可能很确实 你说的对 就是拉马努金 并不一定是一个能够通过后训练 诞生的一个

一个数学家 他是怎么预训练呢 他就是 我不知道 他好像是有很多他的这个宗教仪式 他原来是会计 他在电影里面 反正是拍他 有时候祈祷的时候 能够看到一些数学的 我觉得太有意思了 对对对 这个感觉没有办法 就不是说我们能够后训练

一个AI能够做到这样的 但是拉马努金到了这个剑桥之后 他接触了就是证明 他知道如何写证明了 然后他就使得他的这个数学的 这个影响 有更指数级的爆炸 它有更多的 更多的他想到的直觉 他可以进行证明 然后变成了新的直觉 我们可以训练这个AI去证明

所以说还是会对这个东西有帮助的 嗯 小野肯是后训练 中训练 还是预训练的产物 他有说过这事 啊 这个不知道 我肯定不是预训练的 而且你看他的预训练好像不只是数学 对 那我们现在 大家的预训练 也都是什么都有 目前 其实预训练我觉得能够去往下去 就是做的 能做很多东西

我觉得预训练有大量的 可以基于数据能够走的研究方向 但是只是某种程度上 也没有 大家没有在做 比如说你觉得有哪些可能呢 啊 我觉得 就是在 其实就是一些数据的一些 我知道的就是怎么做的 可能涉及一些其他公司的一些 秘密 所以可能不太能讲

但我们也没有去很深的去想 先训练的事 不做预训练 对吧 以后也不做 我们没目前没有做的打算 为什么你不做预训练 太费钱 嗯 然后我们也觉得 大部分的Lean的这个东西 可以从后训练 甚至是 我们会做一些 我可能会做一些mid training 那有一些人 可能就把中训练 划到这个预训练里面了 对 嗯 对 其实我们确实是认同

说是有一些基本的这个能力 是需要通过预训练 中训练 来提出的 我能理解你们是一个创业公司 里面要做的是AI for Math 那些大厂OpenAI DeepMind 包括DeepSeek 对 字节 他们为什么要做AI for Math 我听说的就是 比如说Gemini 就花了非常非常多的想法 在这个预训练

在预训练上面 然后他们的这个 甚至说他们的 呃 甚至说有些 有些公司会希望从Lean data里面去把 希望能够买Lean data 去做一些一些预训练 就我们现在的这些形式化的数据 甚至可以更多的在预训练 他们要去做什么呢 他们为什么要做 他们是要做一个垂直的专家 还是要做一个

他们就是AGI 那是general的 就AI for Math是一部分 AI for Math并不是每个 有些公司没有 目前我觉得比如说OpenAI 走的是informal这一个 它其实是Kevin Wilson 他的个人的科学雄心啊 就是要做 科学发现 然后 我好像就是DeepMind里面有几个队伍 同时在竞争做 AI for Math 有一个formal的队伍

有一个informal的队伍 嗯 SSI我不太确定有 然后Anthropic我觉得他们有 但是 只是作为 只是作为帮助他们提高推理 推理效果的 就是说 比如说我有一道题吧 一道数学题 它先把它informal变成formal 然后在Lean里面验证完之后 再回来提升它的推理分数 但是

并没有把这个作为一个专注点 其实我觉得作为这个一个 如果我是这些就是玩家之一的话 并不一定会去做 我们现在做的这件事情的 原因是 我一样的人才的这种 这种高密度人才的队伍 我可以把他们再继续在代码生成 或者说在一些更红海的 一些目前竞争咬的比较紧的啊

的领域 去做的更深 去把他们的护城河筑起来 然后完全可以就是和我们 或者是我们竞争对手 这一些做的还可以的 这些创业公司 去进行 去合作 然后这有点像 比如说OpenAI 他们就是会在搜索这一块会call 这些搜索做的比较好的公司 嗯嗯

所以你们这个行业现在目前是蓝海 并不是蓝海 我觉得这个东西是 嗯 比较难 嗯 比较难 不太像蓝海 其实也 比如说就像是机器人的foundation model 一般比如说PI和Skill的两家 然后我觉得现在就是创业上 就是我们和我们竞争对手两家 就是估值也差不多 总共融的也差不多 一个新一点

一个就是比我们两年前差不多 是这样的一个状态 嗯 对你来说挑战是什么呀 嗯 执行的速度 执行的速度与学习的速度 我们现在会有一个 对我个人来说 我执行的越多 我学习时间越少 这是一个非常痛苦的一个过程 就是你我以前可能说 我每天有多少的时间能够用来阅读 现在可能少了这些时间

但我又有那么多的事情需要执行 所以某种程度上这是一个挣扎 然后这个挣扎容易就是会 我相信就是我们其他的一些 很好的科技人才 他们有类似的research 和engineering ratio的一些挣扎 就是一些trade off 我们希望能够执行速度很快 我们也希望探索商业模式的这些 从一个技术的角度去探索

从技术和好奇心的角度 去探索商业模式 但同时 我们要做的这些事情确实是挺多 然后也困难还挺大的 所以我们就是担心这个速度 我觉得最大的一个苦恼 因为我们现在是 我们现在是 成立7个月的一家公司 我觉得期待 也由于这个A轮吧 期待比较大 我们还是希望能够

还是能够做长期主义的事情 我们有点怕 是怕执行的不够快 另外一个是怕 由于要执行的快 导致焦虑 导致这些就是方向上出一些战略错误 嗯 对你来说 实现AI for Math的终点更重要 还是说 成为一个更成功的商业公司更重要 我觉得作为一个就是founder来说 你对你的这个员工和早期创业团队 你负有责任

所以这不是一个 某种程度上我觉得这不是一个 这不是一个纯科学项目 就是我们必须要成为一个 一个能比较长的 一个企业 一个公司 但与此同时 我觉得这个公司的DNA就是登月 其实我非常 对我 非常喜欢MoonShot（月之暗面）他们这个名字 天哪这个名字简直是太好了 这个公司的DNA

如果我们就是太去逐利商业化的话 我们会其实是一个平衡 然后嗯 我们可以看一下我们竞争对手这公司 他们公司的起源其实是因为 Robinhood的这个啊founder CEO 他可能啊现在还全职在Robinhood 他可能希望有另外的一个 让他感到比较 有激情的生活 有热情的这样的一个项目

所以他们可能在早期的时候 更讲这种科学雄心 嗯 我们认为是 我们认为是科学雄心 然后但是我们 我觉得理想的现实主义者 和现实的理想主义者 两种都是不错的 不错的 这个落点 但是不能是太远 就不能是 有一天你们公司如果创业失败了 你觉得可能会是什么样的

是因为什么 嗯 我觉得这个事情其实挺有意思的 就这个事情它的结果 一定是极好或极坏 嗯 就这个公司 其实没有一个在中间的 一个可能性 当然要么登月成功了 要么登月失败 对 就是登月成功 登月失败 某种程度上 为什么说像SpaceX呢 要么火箭发上去了 要么火箭坠毁了 可能火箭要坠毁几次才发上去

可能每次都差那么一点 就其实这是为什么 我觉得就是像伊隆马斯克 他作为一个就是企业家 尤其你看他早期的时候 呃呃 还是一个非常锐意进取的 一个值得学习的 这样的一个企业家的 一个模式 呃 比如说好几次就是濒死 对吗 他的公司也只能两个留一个 但是就是他很坚定的说 both 永远是鱼与熊掌都要兼得

这样 比如Ray Dalio在Principle里面也是这样 我自己也是这样的 一个认同 我觉得这个公司是一个binary outcome（二元结果） 我觉得如果我们是 失败了或者我们很成功 其实都是有可能发生的事情 对 嗯 如果失败了 你去干嘛 这是一个非常好的问题 我自己有 我自己有一些个人的雄心 我看吧

当数学家 我觉得我可能会去希望看一看 我觉得我那一年的神经科学的 学习的一个心得 就是 我们基本不理解人脑 我完全不理解人脑 我可能会希望做一些 跟人脑相关的事情 啊 不 不是跟人脑 就是跟神经科学相关的事情 可能是动物呢 就是我可能会 我可能会希望看一下这些 嗯 我觉得就是 brain and machine interface

的这个vision 目前的implementation都不太足够 就是人机交互的这个目前的选项 我觉得太 太不理想了 嗯 嗯 你今天怎么看待硅谷这些模型公司 的竞争啊 不管是这些大的模型公司 还是这些Neo lab（新型实验室） 我前几天还在跟一个 我的一个朋友在讲就是 其实为什么说

为什么说我最后不想去做一个 就是金融 或者说是一个量化交易员呢 你会出现一个问题 就是你的 你的 你的赢与输 是一个短期内能够决定的一件事情 我觉得这个事情是就像Peter Thiel讲的 就是 这个我是比较激进 垄断导致创新 竞争导致平庸 这种竞争会导致平庸 会导致没有一些长远

一些很有长远想法的人 他就要自己出来做 做Neo lab（新型实验室） 这就这其实这Neo lab（新型实验室）的产生 就是因为好奇心与创造力 是我们人类的基本需求 这就是因为 可能说是在一些 前沿的一些大的公司里面 无法去做 这一些满足他的burning passion的事情 他就要出来 然后

我觉得可能是一个很有意思的点 就是刚才说到这个 好奇心为什么是人类的基本的需求 可以我们可以假设一件事情 就是AxiomProver非常的成功 或者说是我们竞争对手的这个 他们的非常成功 反正就我们中有一有一方非常成功 然后 所有的数学题 你给我一个千禧年问题 我这个AI就把它全部解决了 这个时候还会有数学家呢

这是一个 这是 一个非常值得去思考的一件事情 我答案就一定会有 就是 你给我一个100万行Lean代码的一个 我一定要去看里面是怎么做出来的 你不让我去看 我都会去看 这就是人类的这个好奇心的体现 由于这个证明最后被产生的方式 这些去看懂了 他的数学家们又会有新的猜想 新的想法

这就是整个发明发现的这一个 这一个循环 其实就是 然后就是AI做了 可能AI做了这个发现 让数学家更好的发明 然后这种好奇心 和这种探索的这种愿望意念 是一个 我觉得人类无法被压制住的一件事情 所以说不管是现在是 one hundred million

一亿美元的大包 也无法去压制住 这一些青年研究者的这个 这个好奇心 所以他们就会 去做出来 我们看到做出来 多么有意思的东西 比如说Stefano Ermon 他们做了这个diffusion model 更快更好的这个推理模型 我们可以看到就是呃 比如说就是Periodic 我们第一次把这些顶尖的这些AI人才

就是去 在一个就是现实世界 他们要做这个material science 这是一个非常有意思的 一个方向 他们不怕这些messy的这些data 然后他们其实 比如说我们看到有Recursive 他要做AI与这个 这个硬件之间的这个AI提升硬件 硬件提升AI 这 这是非常有意思的一些方向 我觉得 这其实是

这背后是一个基本作用力 这个基本作用力就是人类的好奇心 然后我觉得可能最有意思的点就是 有些人说现在是一个泡沫吗 还是说现在是登月 就是 有一些公司 他成了他就登月了 然后有一些公司登月了 人家真的是了很努力 大家真的是每一天996 一块去朝那个梦想努力 结果没成 那就是泡沫

其实我觉得就是我特别希望的一个 一个环境 有点像我 我也知道 说有一些好的学府的一个环境 就是不怕失败 MIT有一门课就是learning to fail 你如何更好的失败 就是当然这个 每一个这种登月项目的失败 它都会在资本市场上会掀起涟漪 我们会从这个就是私有市场 一直到这个公开的市场 会有连锁的反应

你 你有可能说这是非常不负责任的 就是为什么这个 一些可能说pension fund 一些大家的退休资金 最终通过好几层的投资 到了这个私有市场 去给这一些有想法的研究者 去满足他们的好奇心呢 这是一个 这是一个很我觉得很公平的一个问题 但是 就是如果说这些好的 有想法的研究者 不是由于他们自己的这种虚荣心

或者说是我自己要占山为王 不是由于ego而驱动的 而是由于使命而驱动的 所以导致他们不是碎片化的 好几个比如同样的一个问题吧 就是8个尝试 他们真的就是在一块了 他们从不同的背景 不同的技能 不同的 不同的 对于这同一个理想的解读 聚起来了去朝这个东西

我觉得这就是一个比较比较legit的 比较比较靠谱的一个尝试 我能理解这一波的Neo lab（新型实验室） 他们都有different的信仰 也有不一样的bets 对 那当有一天 他需要跟这些大的frontier lab 竞争的时候 怎么应对这个竞争呢 刚才我们说了 你们AI for Math之间的竞争 对吧 对 那当你要遇到OpenAI

你的竞争对手是DeepMind的时候 你怎么竞争 对 呃 我觉得这是一个非常好的问题 我觉得首先第一个 就是会有一些结构性的问题 会导致 如果说他们需要 一个单位的创新 是需要有多少单位的资源的 而这个比例的话 在一个早期的创业公司 是非常高效率的 这是第一点 我觉得我们公司就是在做的一些事情

我觉得可能在另外的一个环境 会更难的去达成 也就是为什么 许多人从脸书 来到了我们这个公司的原因 然后 这是一个点 然后第二个点就是 其实吧你作为一个Underdog 这个黑马 你好像除了这个效率之外 还有这个人才 这个之外 人才是人才密度 因为毕竟他们会有更多的人才

你没有什么资源能够和这些大的 这些玩家抗衡 但同时这更有意思的一件事情上是 OpenAI曾经也是对着Google的那一批黑马 他也是那个 就是在Google要把伊利亚 就是最后counter offer抢走的时候 焦头烂额不知道怎么办的也 是那个曾经一度发不出工资的 这样的一个小玩家

所以这其实是一个很有意思的一个点 就是我觉得历史的钟摆来回摆动 就是大家 大家螺旋上升 但是又有很local的这种扰动 某种程度上是有 there is always a way 就这 这个 这个东西我没有办法证明 there is always a way就是你 你得信 嗯 对 然后信的 可能就是 喜欢加入早期创业公司的这一批人

譬如说Humanoid 这个公司最近融了很大的 他们的这个cofounder 是Google的第7号员工 嗯 他到了现在的这样的一个人生阶段 仍然认为 好奇心是 他就是所拥有的最珍贵的东西 嗯 值得他倾家荡产 你这么说我能理解 嗯 很多 包括我去跟赛宁聊 他们其实有different bet

他们甚至是一个Anti硅谷的 都收集了一波Anti硅谷的这个派别 他们也非常反感这种剧烈的红海竞争 对 然后觉得也阉割了研究员的创造性 对 其实是 我是这样想的 就是 嗯 可以 可以就是 就是在一段 在所有的这些就是local的扰动之后 你看到的整个的这个

宏观的这个局面是什么样的 一个竞争的结果 就是能力在飞速的上涨 另外的一个结果就是 呃 好的 且快速 不只是好的 好的且能快速验证是好的的东西 被做到最scale up的一个状态 但是完全有一些可能 可以时间长一点的东西 没有被实现

这是一个机会成本 但所以说竞争 它也不能说不好 它就是确实它 这个让我们人类在这个AI的这个进步 在非常短的时间内 达到了一个 非常高的一个进步速度 嗯 你刚才会说到 你的自己的自我奖励机制 从团队里面获取这种能量 变成了从事情中获得能量 现在的你 是从事情中还是从团队中

现在 我是从事情中 现在的我是从事情中 然后 但是我觉得团队是一个很好的一种 它会给你一种安全感 它会给你一种 就是你有一个 有一个能落地 你的脚还在地上 它让你觉得grounded 但是 你事实上能够让你就是break out的那种 那种冲动的那种能量 有可能是愤怒 有可能是 有可能是悲伤

有可能是 就这种卯着一口劲 我就要去达到一个 让我们这个队伍达到一个什么样的 一个 一个目标的这种的 这个能量 它不由团队中来 它由事情的本身来 嗯对 那个让你最burning的事 终点是什么 我觉得就是

这个事情讲起来就是有一个 莱布尼茨他有一个想法 它叫做universal representation theory 就是说所有你能够表示的 这句话听起来很怪 所有所 所有大部分你觉得能表示的东西 你都能表示 我觉得我目前非常期待一个

让推理能力成为最顶尖的推理能力 成为一个默认状态的一个 这样的一个情况 然后且是能够自我验证的推理能力 嗯 这是我目前个人的一个一个理想 嗯对 其实就是有些时候就可能说 人一辈子 他能剩下什么 有一些数学家

他一辈子解决了一个非常困难的问题 他被这个问题 就是人们 因为这个问题记住了他 他可能这个墓碑上就写着 他解决了这个问题 这一个人一生这一个问题 你想这个伽罗瓦21岁他就决斗 就挂了 然后拉马努金 他是因为这个营养不良 还有各种各样的身体疾病

也早 也30几岁就挂了 就 人类要多少人出一个伽罗瓦 多少人出一个拉马努金 然后你如果说是能够去用AI去复现 这样的一种数学家 然后你又有那么多已经存在的数学家 能够与他互动 然后去有新的这个 Jevons Paradox 对吧

Jevons Paradox我也不知道中文怎么说 他的意思就是说 当你把一个 一个工具变得能够你做出来 让他更便利更普遍的时候 就会有更多的用处 比如说我最近 我们公司好久 就是第一次找了一个 找了一个能够帮我去处理一些 每一天就是杂事的 这样的一个同事 他来了之后 我们就是一块做的 杂事反而变得更多了

就是 这其实就是指Paradox 就是这些科学家 这些物理的 生物的化学的 他们能够与这个AI伽罗瓦 或者说是所有的这些数学家总和 他们能够有多少的科学的理论 能够被发明发现 就数学家们和这些AI数学家 能有多少数学的

就是基础数学的这东西被发明发现 这其实我觉得这是我的一个 你想从算盘到会计师 就是当时是 商务贸易 从这个微积分到这个物理 各种各样 什么力学 然后是thermodynamics 就是然后 然后到工业革命 对吧 然后从这个

这当时一个叫babage 查理斯巴贝奇 他这个能够去算这个log 对数算的更快的一个babage engine 这是电脑的前身 当时哈代写 我作为一个数学 一个数学家的道歉 这个 mathematicians apology好像不是这么翻译 一个数学家的独白 他就说 我这个东西 反正也没有任何的实际价值 后面就有 密码学就有

对吗 我们看Victor Miller 他是一个 他也是Shubho的同事 也跟Axiom很多的互动 这个椭圆曲线 基于椭圆曲线的 密钥学的 就是就是泰斗之一的这样的一个人物 他是一个纯数学的一个背景 然后就是看了一眼 然后就看出来了这样的一个理论 这对于很多就是纯计算机的 这一些同学们

有非常大的一个价值 这是终局 但是有些人说 这个终局之后怎么办呢 这个就不知道 终局之后我觉得还是要 我觉得其实就是钟摆的摆动 又会卡 但我觉得 AI for Math没有像AI模型被scale up一样 被scale up 而我们希望能做这样的一个人 这样我们能知道天花板在哪 我们可能又能回到research 然后又能这样 就是钟摆的来回摆动 嗯

我见过很多的70后 80后和90后的CEO 你应该是第一个00后的CEO 我不想就是画这种代际 但是我还是很好奇 就是一个00后 而且是女生的公司 嗯 会和之前的这些公司 或者是就有任何的不一样吗 你觉得特点会是什么呢 我这个 我这个其实是非常好的一个

因为我自己最快乐的一个状态 绝对不是CEO的状态 我自己最快乐的状态就是 我能够当一个research scientist intern（实习生） 为什么要去intern呢 就是这个 我说的话如果比较愚蠢 这个大家认为是正常的 我这是最快乐的一个状态 我是真的想做这件事 然后我如果能够有另外的一个 很明显我可以加入的一个地方 我就会去加入它

而不会把这个事情单独做起来 所以我这是我的一个舒适的一个状态 所以我 我不太因为事情本身而创业 而并不是说你想当一个创业者而创业 我特别不想当一个创业 这个能理解对对 我反正就是 所以我不太CEO 这个可能大部分 所以 但也有时候有一次闹一个笑话

就是我有一天特别就是想做这个 Benchmark 我想做一个就是 我不是说嘛 那个基准级就是到博士级别就很难搞 我当时就把 我们办公室有那个数学背景的同学们 我就是说 我想搞这么一个东西 我也不知道 就是现在搞这个 是不是优先序上是对的 你们都是搞数学的 你们要不跟我一块 我们分一下

就是你负责这个领域 你负责这个领域 每人找个二三十题 然后完了之后 我就后面就被 我们那个一个比较元老的工程师 就说了 你让这些这个实习生的同学们 就是还有这些比较年轻的 工程师觉得 这是一个非常重要的一个任务 这和优先级是相斥的 我说为什么是重要的任务呢 我说这不就是一个side 一个hobby的一个project吗

他们说但是你是一个CEO 所以你跟他们讲的时候 他们就会觉得 这是一个正儿八经的一件事 我真的要去 把这个当做我的前几件事情去做 从那以后 我就更hands off了 所以就是 这是一个非常非常有意思的一个 一个事情 嗯 还有什么不同吗 你觉得可能和我觉得 就是 我觉得我

我觉得我做这个CEO的一个好处就是 这是一个 Techno Crass rule的一个公司 就是我们的技术人员 他们是整个公司的主干 且和定向和锚点 就是他们 有可能由于我并没有一些 strongly held beliefs 所以导致我觉得我们就是很多ideas 都可以被 由于我没有一个特别我自己

其实我有一些特别坚信的方向 但是很多其他的一些 就是很low level的一些东西啊 就是一个bottoms up的culture 所以我觉得这个公司的文化是一个 是一个比较有意思的 就像一个 比较比较 皮克斯梦工场 对 你们公司的会议室 好像都是用数学家来命名的 有什么有特别的 对 如果你想 如果这个梦工厂

或者迪士尼的这一个CEO是一个 已经假设 OK一个梦工厂的CEO已经是一个 就是拍过多少个 好莱坞或者迪士尼的一个导演 的这样的一个人做CEO 这个地方就成为不了梦工厂 为什么 因为他们会觉得这个人是对的 应该听他的 所以我觉得反而是这种bottoms up的这种 这种culture对创新来说是最好的

需要一个Intern对 我觉得Intern挺好的 我非常愿意给Axiom当Intern 你们的会议室有任何有意思的吗 有 对 不同的名字 它们就是有 叫做高斯 对吧 高斯 庞加莱 希尔伯特 Lovelace 还有图灵 这个中间大家差点打起来 因为怎么命名啊 为什么差点打起来 就大家喜欢的数学家不一样

大家说 你有了这个 你有了图灵 你没有Church 哎 这个不行 然后你有了这个Lovelace 你没有Noether 不行 反正我们还接受到世界各地的邮件 说为什么不把Emmy Noether 作为一个一个会议室 我们说我们不好意思 我们目前只有5个会议室 后来是怎么选择的取舍的 啊 好像是 我也不知道最后是怎么取舍

大家反正就是还是在Slack里面 经过激烈的争辩 大家认为庞加莱 希尔伯特 高斯这些都是polymath（多个学科领域都有深厚造诣） 他们在数学里面不止会一个领域 他们会好多好多领域 所以所以拉马努金就是这么落选的 他只会数论 所以说就是大家要找这种 就是我们觉得要是做一个AI数学家 希望他什么领域都会 没有distribution shift这样的一个问题 所以要找一些polymath

图灵是跨世纪的 当然Shubho他 也lay his body on the table说 如果你不给其中一个叫图灵 我就走了 我说 行行行 那就是图灵 然后完了之后 我们希望能够有一个女数学家 然后这个女数学家 我们觉得Lovelace 其实就是在Babiage engine这里 也不错 嗯 这其中有你的偶像吗 我的偶像是Goss 他 他在 对对

然后庞克瑞 其实庞加莱和弗朗索瓦沙尔唐 他们家里是 他们都是法国人 然后他们家里那个族谱还是连着的 为什么高斯是你的偶像 为什么高斯是我偶像 就是 他是 就是解题里面的天才 对吗 他这种 他这些故事 什么正17 持规划求正17边形 然后包括就是我喜欢数论 然后高斯在数论里面的这个

都是非常基本的 就是fundamental的一些贡献啊 高斯比如二次互反律 然后 各种各样 反正高斯在初等数论 他是 他有点像是我学数论刚开始的时候 初等数论里面就好多高斯 所以 然后又他又是一个年轻数学小王子 然后反正就整个 我还是挺喜欢高斯的 对 如果可以穿越时空 和历史上的任何一个数学家共进晚餐

你希望选择谁 你想问他什么问题啊 我觉得就是去跟埃尔德什（Erdős）共进晚餐的话 他给你讲的那些描述 毕竟是组合学 你晚餐这个就是table上能听懂 然后埃尔德什（Erdős）是有 又是那么一个 就是peculiar（古怪） 非常古怪的一个 有趣 有趣又古怪的一个 性格古灵精怪的 我觉得跟埃尔德什（Erdős）共进晚餐 会比较有意思 另外一个我觉得

我觉得跟罗滕迪克（Grothendieck） 共进晚餐的话 如果不是我的话 就是说另外一个人 他跟罗滕迪克（Grothendieck）共进晚餐 应该意义会很大 因为 但是我这个代数几何学的不是特别好 所以就是跟罗滕迪克（Grothendieck） 可能容易浪费这个宝贵的机会 嗯嗯 你看当你说到这些数学家的时候 他们都是这么有趣的人 对那如果有一天 AI for Math 能做到所有数学家能做的事情

会不会是一件很无聊的事情 我有想过这个点 我觉得我 其实我一开始觉得是一个非常 就是 非常非常 我当时觉得是可能会是一个 我不希望让这个局面 是一个非常遗憾的局面 因为就是 是可以说数学家们 他们之间的这种友谊 他们的合作的这个关系 他们的文化社区 是一个非常有意思的一个文化

就是比如说有一个数学家生日 大家会给他办一个生日的一个峰会 然后所有他的学生 他的合作者们去轮流去讲一个 这个人所做出来的数学的贡献 或者是一个 跟他们合作的一篇文章 我曾经就是作为一个 硕士生在这个牛津去过这个

Roger Heath brown的生日峰会 然后像Ben green James Maynard他们都在那里 然后当时就觉得是非常的感动 就是这是一个非常好的一个一种传统 所以人的这一个元素 我觉得在数学中它永远不会被磨灭 我觉得AI会把 就是数学的很多 证明可能能够帮数学家们 去很快速的解决

但是这个猜想 直觉以及构造 以及这些方面 我觉得数学家们仍然会 有非常多的乐趣 然后他仍然是会 他们会成为智力的灯塔 嗯 对 所以我们刚才说的那个 当然这个也不一定我们能解决 这个当然是有的时候你做梦 想着自己能能把它解决了 会不会反而是一个

不太好的 一个添加 因为比如说这一些数学家们 非常珍贵的 这一些legacy 他们的 他们的 但是啊后来觉得 他们就是会有更多的问题 他们会难倒AI 像他们已经在难倒AI一样 做基准集 他们会永远永远是智力上的挑战

以及大家这种互动应该会很有意思 所以我们刚才说的那个问题 拉曼努金和做一个验证的AI对 他其实还是偏这边对吧 他验证偏验证 他并不是那个天才型的选手 对这个我觉得直觉就太难做了 我觉得直男直觉可能5-10年 有可能 对 但是我有一个很我有一个比较 又有一个比较激进的一个想法

就是我觉得大家现在如果看 有多少解析数论里面的问题 是被一遍又一遍的 在一包很标准的证明方法里面去抽 抽 这个证明牌就是就 就一个牌 一个卡牌 一个一个卡牌 一个卡牌 就这么重复的熟练的去运用 比如说哎 我看这个啊

major arc minor arc Hardy–Littlewood 这个circle method就能解决一些 一些 一些就是bounding的 就是上线 下线这些这些方式解决一些 一些概率法解决一些 然后比如说你去上Sieve theory Sieve筛法又能解决一些 筛法也在被 就是有一些人 他们不解决任何问题 在提升筛法能做的

筛法作为一个工具 我觉得就是已经能有的这一些工具 能解决很多很多的问题 然后我们会说一个人直觉很好 可能是他很快的 能够想到怎么样去重复的 我们现在讲的这种直觉 我可能讲的是说 给大家一个完全不同的一种 一种方法和机制

这个我觉得是5到10年 嗯 你有过一个说法 就是说热爱数学 就是看到了上帝的面容 为什么会说这句话啊 我是这么觉得的 就是我很小的时候就觉得说有一些 有一些基本的这些真理 然后我觉得数学家 科学家他们存在的这个 意义之一 当然就是去把这一些东西

进行发现和探索 其实我 这是我16岁 我曾经写过一篇文章 我当时是这么 至少是这么想的 然后 后面就是临要开这个 就是创立这个Axiom的时候 就是 不是说老跑步嘛 早上 斯坦福他有一个 就是教堂 叫Memorial church 这是就是纪念教堂 然后如果你去 就是我们Palo Alto这边往那跑

然后如果平常我都是绕着跑 因为就是特别晒 那一天就是往这个草坪底下去跑 然后就是突然 我就在那个教堂的下面了 然后当时那个阳光也特别好 然后那个教堂上有壁画 有天使十字架 其实有那么一点spiritual的一种感觉 一点灵魂的这个感觉 就是觉得 可能说如果那个就是一个人的

这个木制碑上可能印了一个 他曾经证明出来的 这个事情 是他的智力遗产 那么如果能够让这个东西乘以1亿 你会不做 可能不会 所以当时有这么一个想法 当然这个我觉得也自己就 这是一个出于ego的一个想法 就是说我 我可能说想 我这个公司 能够去

作为这样的一个AI for Math的一个unlock 这个想就是我希望登月 也希望登月的是我们 这个肯定是出自于一点这种ego 或者是就是的自私的雄心壮志 但是总体上 这个事情我是非常希望它会 它会实现的 对 就算我们是失败了 可能要谁其他人登上去了 也是一件好事 虽然你现在还很小

问你这个问题好像不太好 但是还是想问 你希望你的墓志铭上写的是什么呢 哎呀 你是希望你是一个数学家 还是一个 别写 对 其实我是一个比较 就是觉得体验比较重要的人 那我反正要活过了 我也有体验 这个就无所谓 我都不知道我要有什么墓志碑 不重要 那就不重要 你会希望你自己是一个数学家吗 啊 也不重要

不重要 我觉得我 我曾经是觉得很重要的 这是这是 这是这是 我曾经觉得就是我一想到我 可能我就没有办法成为一个数学家 我有时候一开始我有时候还哭 我还是一个比较 比较比较emotional 有时候会 刚决定创业的时候是吧 对对对 那个时候是这么觉得啊 然后后来觉得 其实就是 我想当学徒 对 其实就如你要非写一个什么

就写学徒 就是我想去 在尽量多的一些智力领域上 能尽量多的去学一些东西 比如说 为什么你看我跳来跳去就是数学 然后跳物理 为什么又跳物理 因为我高中初中物理可差呢 我想着怎么着学一下吧 然后嗯 去学点神经科学 也学的 生物那一块学的不怎么样 但是我觉得 跳这个计算 神经科学学的挺有意思 然后AI挺有意思

然后学这个量化交易前沿 在XTX真的是很感谢那段经历 然后又去学法律 然后法律 喜欢各种各样的 从反垄断 by the way反垄断是一个非常 就是antitrust 是一个非常 像树状的一个 逻辑的一个 一个非常像数学的一个学科 合同法也是 然后又有那种完全不像数学的 比如宪法 就是 宪法其实这个

或者说是这种民事诉讼 这一些 庭审 这个最初级的庭审 这些都是讲故事的 一些 这个领域 然后 就是 所以我还是希望能去学很多的东西 就我觉得AI for Math 其实对我来说 我人生最快乐的时候是我拿到那个 我找到那个GitHub的那个Lean 然后我把这里面的那个文章的abstract 全读过一遍 那是我人生最快乐的几个月

然后那个时候最快乐的几个月 那个时候Shubho就跟我一块在读 然后现在跟Shubho一起做 然后当时最快乐的几个月 那些作者 他们陆续加入了Axiom 我们现在有 如果你说前30篇AI for Math的文章 我们就是大部分都是作者 都在我们的Axiom这里 所以又他们就是每天和你就是一块 去 冲这些目标的战友 又觉得非常的快乐 其实我觉得就是这

这可能是不错的一个game 你现在是什么的学徒 我现在是怎么能够让一个 一般来说创业公司都会死掉 怎么样不死的 一个学徒 一个创业者的学徒 一个 创业者这个词听起来太好了 就是 创业公司99%他都会死掉 所以就是 怎么 我现在是 就是Don't die 这个 Brian Johnson有一个好玩的Don't die movement

我现在是Don't die的学徒 你看你的第一个自我奖励的方式 是通过人来获得的 第二个是通过事情来获得的 你说 钟摆 已经到了事情这一边 但是人能给你提供一个安全垫 让你觉得grounded 那有一天你作为CEO 当这两个事情发生冲突了 冲突过呀 这个怎么冲突过 我们也

我们也开过 实习生 就是我们 我们也冲突过 但就是 这个事情 我觉得就是你任何的乐观主义收起来 你要谨慎的做决定 你要想很久 就是因为毕竟是要对 就是可能 人就是要负责 然后但是 同时我有另外一点 就是很多时候你觉得为什么要想很久 是很多时候 你觉得人与事冲突了的时候

其实是你自己不够好 就是可能这个人可能都跟你关系很远 但是你总是有一些 由于你自己技能点和能力的问题 是能够让这两个事情不发生冲突的 就是他走到冲突的那一刻 一定是因为你自己本身 曾经有做过一些错误的决定 就算这个人可能是一个你不认识的 如果公司很大 这是不认识的员工 他一定是有一些管理层的一个决策 他一步一步的尽头

trickle down到出现了这样的一个问题 嗯所以我 我还是比较相信一个词叫authorship 就是authorship 就是作者 就是你 是你自己人生篇章的书写者和作者 所以你 你不能够有 觉得是呃 可能不能够觉得说就是一个情境 它就能够决定你的一个决定 是你决定让这个情境决定你的决定的

所以你也可以决定用其他一些方法 去使这个情境不要这么走 我是这么想 嗯 那我们最后还有一些小问题 嗯 我们会让每个嘉宾给我们的观众 推荐一本人生之书 你会推荐哪本它 要真的对你人生产生过很重要的影响 不能是数学书 你也可以说是数学书 呵呵呵 嗯 我数学书的话 如果是年龄 年龄比较小的观众

我推荐初等数论 里面对数论讲的真的是很好 如果是 数学书 其他的数学书 我觉得 David Porter的那本分析数论 我觉得很好 然后 我还是比较喜欢书 如果不是数学书的话 我是 我挺喜欢红楼梦的 就是我确实是挺喜欢红楼梦的 甚至是红楼梦很多学者 他们去研究红楼梦

这个是一个曾经在我小时候 对我比较有震动的一本书 然后刚才也讲到 大雅宝胡同甲2号 对我人生产生影响比较大的 其实有 挺多关于一些企业家的一些故事 譬如说 伊隆马斯克的故事 就是说 还是他之前的一任太太 他讲的是他晚上睡不着 翻来覆去

然后就痛苦的咆哮 马斯克 痛苦的咆哮 然后 包括说 是一些其他的 黄仁勋 就pain and suffering 这些东西 我觉得就是 由于就是可能看到过他们的这些故事 会让你有些时候比较难的一些感觉 像嚼玻璃的日子里面 会觉得哎

这就是一个正常的一件事情 你觉得现在训AI 跟你当年训自己有什么不一样 这是一个很好的问题 对我 我觉得有时候你会觉得有点像啊 比如说 就是看到他这个表现刚刚好了一点 马上给他更难的题 这种curriculum sampling 对吧 这是一个很有意思的一个事情 比如说啊 让他能够去 给他

又觉得是 跟自己曾经的那个数学家的 那个感受有点像 呃没有说特别应该有区别 但我目前没有特别能够想的起来的点 就是你感觉你看到相似的时候 你就会特别有这个 你的大脑里的神经元就在fire 假设Axiom的AI 在未来证明某个重大的猜想 但在证明过程中使用了一个新的公理

这个公理不是现有数学的一部分 但是看起来非常的合理 你会接受这个证明吗 能想 想像到所有的数学家们 就是 感觉就是世界末日的一个思想 思想实验 呃我们看到了 AI在尝试用各种各样奇怪的公理 去帮它作弊 这个事情已经发生了 对吗 就是我刚才讲的 其实这个事情 DeepSeek还为此受害

他当时说DeepSeek-Prover 我忘了是哪一个version 说做出来了 Putnam上的（题目） 当时600多道Putnam上的题 就是Sota 在个位数 然后DeepSeek说我们做出来了49道 事实上只做出来47道 有两道题其实就是这个 这个 AI在作弊 我觉得 如果这个公理大家觉得是自然的 大家就会接受它

但是这个事情 我觉得 就可能是一个大家以前没有探索的 很足够的数学领域 不然的话你可能会认为存在 即合理或者 不存在即不合理 这个公理可能已经被被假设了 它可能是到了一个 有点像我们看代数几何混这个组合 除了群赫的这个代数组合学 这个我们可能未来有一个 我瞎说啊 probabilistic analytics

这个真的是瞎说 可能我们未来有一些就是混的 混了好几个领域的这样的一个东西 大家再往里面加东西 我觉得就是 是可以按照接受和不接受 两个世界 照样去运作的 当然你这个branching factor现在是2 你如果继续这样 你就会有无限多个世界 然后就会一团混乱 然后有一天大家可能就会说回收 我们把它Titan 这个其实是数学

某种程度上是一个 是一个人类文明的一些构造 所以我觉得大家是可以的 就比起比如说物理 你要加一个什么定律 这个可能大家会觉得 其实还就更不可接受一些 其实这挺有意思的 嗯 刚才我们其实也谈到了Deepseek 嗯 你会怎么看中国AI现在的发展呀 包括DeepSeek 包括字节 包括Kimi MiniMax等等公司 你觉得在未来的AI宇宙里

中美会是什么样的关系和角色 我很respect 就是这些 中国的这个AI玩家 就是比如说 我很我很诚实的说 我觉得就是豆包Seed 他们做AI方面做的非常的好 非常的好 然后他们也是非常短的时间 非常执行力强的一个团队 跟他们的一些同学 比如说Zheng Yuan（袁政） 跟他们聊过 就是非常好的一个团队 我觉得就是他们 然后他们可能会

选择或者选择不发 发一些文章 然后我觉得就是这些ideas可以 就是流通还是挺挺好的 对 但是当然大家可能最核心的一些东西 还是会可能不在文章里写 然后可能会做一些 他们没写什么的deserver 但是就我还是觉得 如果是要做纯粹的科学与创新的话 就是稍微往学术一点 就是少一点就那种商业的一些顾忌

多一点学术的就是信任与纯真 我觉得是好的一个 希望大家一起啊 是一个好的 就是工业界的一个practice 对 中美呢 中美的话我也不知道 就是我觉得好多 反正人才不分世界 对吧 但大家可能有 就是有些同学愿意在中国生活 有些同学愿意在美国生活之类的 就不知道

你觉得2026年你对AI发展会有哪些预期 2026年我觉得大家应该能把这个会看到 很快 我觉得我们能看到 第一个continue learning的 一个小模型啊 我觉得我们很快能够去 看到一个非常好的multimodal recent model 我们很快所有的这些 就是什么agent economics 全部会被scale up 我觉得我有一些个人大胆的预测 我觉得很好值得做的

一个orchestrator是很好值得做的 然后我觉得subagents刚才讲过 是很好继续做的 我觉得formal verification tooling 应该作为RL reward 完全是under export 这个和我们做的也很有关系 你刚才说的第一个和第二个分别 你说的是被谁做出来 第一个 continue learning 持续学习 我知道有一些不错的团队 我感觉他们很快就能出model 是小公司还是大公司

嗯 小公司 全是小公司 哦 都是Neo lab 都是Neo lab Multi model也是吗 Multi model也是 Neo lab 他们应该很快就会 就是很快就会问世了啊 也是我的好朋友 对当时也希望他能来加入Axiom 最后也祝福他 一些快问快答 一个全球范围内你喜欢的食物 全球范围内 喜欢的食物 喜欢 就是寿司 任何的寿司 在全球范围内你喜欢的地点

喜欢地点 悉尼 为什么 我小时候第一次出国是去悉尼 一个少有人知道 但是必须知道的知识点 可能是一个冷知识 你可以自己搭CPU 你最近对于生活的一个非常新鲜的 鲜活的认知是什么 或者体验 我都可能我最近过得也不是特别鲜活 我每天早上就是几点钟起来 然后一直工作到晚上几点 哦

鲜活的认知和体验就是 我觉得还是 每一次我去 就是在跟 就是新希望 能加入Axiom的同学聊的时候 就会觉得 未来无限好 未来无限希望 然后觉得 感觉到 那种自己曾经做这件事情的初心 并没有因为就是反复日复一日的执行 感觉被打磨掉就是觉得非常的快乐 感觉像是两只鲸鱼又在找到了彼此的

这个聊天频率 这个还是挺好的 所以招人是一个我非常快乐的事情 鲸鱼找到了自己的聊天就是 对 就是有些鲸鱼 它那个就是频率跟别的鲸鱼不一样 然后如果说你遇到一个人 然后你们都以前是学数学的 然后 可能你们现在都AI for Math有一些理解 但你们又同时有一些新的理解 然后你们聊一些东西的时候 还挺有意思的 另外一个我觉得比较鲜活的体验是

我们就是发现非常多了 古老的一些技巧 对我们现在的这个比较前沿的研究 有这个 有指导价值 然后这个有点像这个二十四诗品 有一个叫 如江不尽 与古为新 还是挺有意思的 每一次有这种call back 我觉得特别有意思 像世界是一个 世界是一个圆 我们又回到了原点 你心目中影响AI进程的几篇论文

我觉得第一篇我觉得是 就是 Christian Szegedy的那个白皮书 都不是论文 就是他想未来应该是什么样的 这是这是第一篇 第二篇我觉得是 可以看Guillaume Lample和François Charton的 那个 发现说可以去让Transformer去做一些啊 一些task 然后后面 当然

这一篇论文是他们开始很多的尝试 后来拿这个东西去找其他的构造 第三篇Draft, Sketch, and Prove 这个讲过了 第四篇其实我就是一堆bundle 就是从Kimina Prover到DeepSeek Prover Gödel Prover 1和2 Seed Prover 所有的这一些 就是真的在拿RL把它做起来了的 因为我们刚开始的时候 连就是从来没有一个RL 做的formal prover

我们刚开始的时候连这个都没有 我们在融资和这个 做这个法律 使得这个钱到账的这个过程中出现了 Kimina prover 基于当下的认知 一个你最关键重要的Bet是什么 啊我bet system 我不bet model啊 我bet就是 这个system有非常多的事情可以做 然后包括orchestrator 然后我另外的一个 基于与这个又相关的一个bet

就是我完全相信recursive self improvement 是很快就能够做出来的 然后有一个问题就是 如果你做出来之后就是 然后呢 你是 然后做什么 这个东西就是能否 就是我觉得可能会出现一个 这个需要一些forward deployment的一些东西 我觉得forward deployment的东西 还没有在AI的时代得到一个革新 然后我觉得传统SaaS会死

我们工作室叫做语言即世界工作室 当你第一次看到这个名字的时候 你会想些什么 我第一次看到这个的时候 我想的就是说 我觉得数学家们 他们在几千年几百年 他们都是在拿英语写代码 或者说拿中文写 就拿他们的那个本国语言写代码 就是他们在进行的是逻辑的推理 但是

他们是在自然语言里面去进行的 逻辑推理 这是一个让我觉得 非常神奇的一件事情 然后由于这个特质 现在我们可以看到说是 比如说 就是就是 做这个计算机的同学们 可以拿自然语言去写代码 但数学家已经做了就是几千年了 所以数学它所有带来的这一些结构啊 这一些逻辑

为什么说和这个代码验证它有帮助 其实是有这样一个特性 这是我当时在想的一件事情 然后另外我在想的一件事情就是说 如果你去把 这个世界想象成一个manifold的 一个比较高维的这样一个几何拓扑的 一个流行 你这个语言 它这个带来的或者说是基于text based的 就是next token prediction这个AI

它到底在这个上面有有多少 探索了多少 然后又flatten了哪些呢 我反正就在 我曾经有段时间在想这个 因为我在想怎么调loss function 但是 这是 这是我的一些感受 对