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

Summary

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

---

节目主题概览

本期访谈主角为00后华人女孩洪乐潼（Leting Hong），Axiom公司创始人兼CEO——Axiom以“AI for Math”为使命，刚完成16亿美元A轮融资。她的创业和前沿研究引发高度关注——其中一则新闻尤为惊人：57岁的美国终身教授辞职为24岁的华人女孩“打工”。本期采访深入探讨了AI与数学的关系、AI4Math大局、如何用Lean这样的形式化语言“把数学变成代码”、证明的美感、算法与直觉、科学家与创业者心路，以及新时代的科学创业图景。

---

重要议题与核心讨论

一、洪乐潼的背景与Axiom的起点

[00:12 - 07:25]

• 洪乐潼，2001年生于广州，从小热爱数学，现为Axiom创始人兼CEO。
• Axiom定位为“AI for Math”公司，刚拿到16亿美元A轮，处于AI新赛道风口。
• 创业契机：一次次试题失败和“自认最愚蠢”的历程，孕育了「非天赋型」「蛮力型」选手的坚韧精神。
• 与联合创始人Shuobo在硅谷Verve咖啡馆“神奇相遇”，组建创业班底。

精彩片段

“我确实在每一个时期都觉得自己是那个环境里面最愚蠢的那一个，最怎么样努力都看不到结果的那一个。”——洪乐潼 [00:14]

---

二、数学的本质、被创造还是被发现？

[08:11 - 21:33]

• 数学：创造与发现的辩证统一。它是一种“结构的语言”也是文明秩序的雏形，由公理体系出发，无限衍生理论与“解题”艺术。
• 数学的美感体现：“最深刻的美往往来自不同领域的连接——如模型式椭圆曲线定理，将代数和几何贯通。”
• 各流派对数学的认知不同：有“压缩”公理、讲究简洁；有重视“表达力”；有天才直觉型与蛮力型的做法。

引用

“数学有一点像是我们决定去创造一个文明的体系……这个过程是很多人觉得数学是解题，但往上搭理论的这个过程其实很有意思，一般先从例子，再归纳，再证明，有点像艺术。”——洪乐潼 [09:00]

---

三、AI能不能成为数学家？人类与AI的头脑对比

[21:34 - 38:02]

• AI并非人类的专利，自动定理证明（ATP）和交互定理证明（ITP）早于深度学习出现，通过规则系统解决数学难题。
• Axiom 研制的 AI 系统以 Lean 语言为核心，能够在像 Putnam 数学竞赛这样极高难度的实际任务中获得人类历史第六个满分。
• AI在解决某些题目上依赖“蛮力”与完整枚举，人与AI解题路径与风格均有差异，两者可形成互补。

引用

“AI是大力出奇迹的那种，它把题拆解成几千行代码，一步步枚举验证……但人类有时一张图就把事情做出来了。”——洪乐潼 [24:00]

---

四、形式化证明与自动化——让数学成为机器语言

[38:03 - 53:21]

• 形式化证明（Lean等语言）让数学变成“可以被检验的代码”。
• 这场变革不但能让数学更易验证、更少出错，也是 AI 能进入高端数学殿堂的敲门砖。
• 具体案例：AI系统自动形式化 Putnam、IMO题目，极大提升人类数学知识的可扩展边界。
• 未来愿景：AI进化为“猜想家”，不仅验证人类定理，还能主动出题、提出新 conjecture。

---

五、自由注意力与创新：数学家/创业者的灵感之源

[53:22 - 70:00]

• 洪乐潼分享成长中的“自由注意力教育”：童年时光用于漫步、沉思、看书与跨学科探索，这种“游荡”是灵感与直觉的泉眼。
• 创业后反思“邦定/自由注意力”的转换，提出：“纪律性执行带来累积，而自由注意力带来突破。”
• 她也区分三种创业者——Visionary（梦想家）、Executioner（执行狂）、Sales（销售型），自认为属于第1类，极度乐观、善于折腾，小扎（扎克伯格）则是“执行者”的典型代表。

引用

“我非常怀念小时候走路上学的自由注意力……很多求解的灵感，是在非线性、不被限定的空间里突然出现的。”——洪乐潼 [64:40]

---

六、成长、友谊与逆流而上的选择

[70:00 - 91:45]

• 童年与初高中数学竞赛、群体中的零和游戏、如何拒绝被“过度竞争”的文化训练、寻找属于自己的兴趣部落。
• 海量阅读与发散思维带来的“学习突飞猛进”现象——不是刷题，而是对知识体系的整体吸收。
• MIT、牛津、斯坦福三校的学术磨砺，特别强调与世界顶尖“大佬们”共处的自我心理适应。
• 自我奖励、失败与苦难的观照：创业者普遍“对suffering上瘾”。

引用

“失败是你的默认项，只要你有足够乐观的机制，你经常能扛过去，再跌一点也不怕。”——洪乐潼 [79:10] “大部分founder都对痛苦上瘾。” [79:34]

---

七、法学、神经科学与多学科交汇视角

[91:46 - 104:14]

• 牛津硕士阶段研究神经科学，最终被AI吸引归航。
• 在法学院研习宪法解释学时，AI已被设想到法律文本解析领域，这也启发了「为什么不能用AI做数学」的想法。
• 从“textualist”司法哲学到“数学可被形式化为程序”，创业梦想逐步立体成型。

---

八、技术体系、创业艰辛与顶尖团队搭建

[104:15 - 141:20]

• 技术体系：Axiom强调系统架构创新、scaling、自动化，以及ML/编译器/数学家多元混合的人才结构。
• 融资艰难：洪乐潼坦言融资是“复读机式的折磨”，但“只要找到信的人”，对话仍旧会点燃激情。
• 采访中穿插众多一手创业观察，包括团队选人标准、人才密度和科学理想主义的坚持。
• 独家揭秘与Shuobo、Ken Ono（小野肯教授）等顶级科学家团队如何汇聚，成为“MathClub”。

引用

“我给自己最大的自我怀疑，不是浮躁，而是这个问题会不会本来就做不成、技术风险太大？”——洪乐潼 [133:28]

---

九、AI4Math的现时生态与产品落地展望

[141:21 - 178:02]

• AI4Math是垂直专精领域（Math & Formal Proof）的深科技（deeptech），不是纯“模型厂”。
• 从math到code验证、芯片安全、行业自动化，数学代码化带动超高价值市场落地。
• autoformalization（自动形式化）是ultra-hard问题，难于证明本身，标志着AI认知的“硬核升级”。
• 在与OpenAI、DeepMind等大厂的关系上，Axiom作为专精创新者能提供关键补全与合作机会。

---

十、哲学视角：AI、理论极限与人类意义

[178:03 - 224:30]

• AI4Math不只是训练出一个“完美验证员”，也要成为能够自我提升、递归自完善（recursive self-improvement）的超级科学家。
• AI冲击下，数学生态不会消灭人类互动与浪漫，反倒会促发更多创新——好的机器证明将激发数学家以“猜想家”身份继续引领新问题。
• “终极梦想”：把顶级推理能力和自验证能力推广为所有科学家和工程师的“默认配置”。

引用

“AI for Math 将把我们从数学的‘mass poor’，带到‘mass rich’的社会。”——洪乐潼 [198:30] “我人生最快乐的时候，是那几个月把AI for Math的全部论文阅读一遍，作者全进了Axiom。”——洪乐潼 [221:15]

---

十一、文化、管理与初心——00后CEO的新范式

[224:31 - 240:00]

• “实习生文化”、Bottom-Up管理哲学贯穿Axiom，公司会议室以高斯、希尔伯特、庞加莱为名，强调多元、开放、好奇。
• CEO自我定位“学徒”，不是传统领袖；“作者精神”（authorship）强调对选择和团队的自我承担。
• 对未来的畅想：希望AI能替代自己，让自己去体验更多学科与人生乐趣。

---

十二、快问快答与生命观照

[240:01 - 260:00]

• 人生之书：《红楼梦》《大雅宝胡同甲二号》；数学推荐德文普尔、初等数论等。
• 现阶段学徒身份：“dontdie的学徒”；最快乐时刻是与团队伙伴作为“战友”一起冲目标。
• 对AI for Math的能力极限和哲学难题（如AI自创公理体系、天才直觉型创造）坦陈挑战，既有敬畏、也有开放自省。

---

十三、对中国AI与全球产业格局的见解

[260:01 - end]

• Respect中国AI创业公司（DeepSeek、SEED等）；中美人才、学术与工程实际流动紧密，好奇心基础上建设全球合作生态。
• 预言：2026年将见证continue learning（持续学习）与多模态推理（multimodal reasoning）模型的Neolab爆发式突破。

---

经典语录 & 高能时刻

• “我确实在每一个时期都觉得自己是那个环境里面最愚蠢的……最怎么样努力都看不到结果的那一个。”——洪乐潼 [00:14]
• “数学到底是被创造还是被发现？这个千古难题，我想它其实是一种共谋。”——洪乐潼 [10:50]
• “AI是大力出奇迹的那种。他把题拆解成几千行代码，一步步枚举验证……但人类有时一张图就把事情做出来。”——洪乐潼 [24:00]
• “大部分founder都对suffering上瘾。”——洪乐潼 [79:34]
• “AI for Math 将把我们从数学的mass poor，带到mass rich的社会。”——洪乐潼 [198:30]

---

重要时间线索引

| 时间点 | 主题/人物/事件 | |----------|----------------------------------------------------------| | 00:12 | 洪乐潼自述成长与公司起源 | | 10:50 | 数学的本质：发现or创造 | | 24:00 | 人类VS AI解题方式与例子 | | 64:40 | 自由注意力与灵感—创业/求学与数学直觉 | | 79:10 | 谈“失败”：仍然乐观，有痛苦也要前进 | | 91:46 | 神经科学与AI for Math 的交汇灵感 | | 133:28 | 创业自我怀疑与阅读科学史自证之旅 | | 141:21 | 对AI for math市场落地与技术架构的深刻逻辑梳理 | | 178:03 | AI4Math哲学极限、自我递归完善展望 | | 198:30 | 数学普及梦想与大时代科技跃迁观 | | 221:15 | 最快乐时刻：与AI4Math论文作者共同战斗 | | 224:31 | 00后CEO的管理/文化观，强调“实习生”思维、学徒精神 | | 240:01 | 快问快答环节、人生之书、对未来身份与“学徒”定义 | | 260:01 | 中国AI与全球格局、未来预测 |

---

全文氛围与风格

• 坦率真诚、乐观浪漫、知识密度极高
• 语气中透露自省、幽默却有使命感
• 技术细节与人生感悟并进，既有数学美论，也有创业鸡血

---

结语

“如果我的访谈能陪你走一段孤独的未知之路，也许有一天可以离目的地更近一点，我就很温暖。”——张小珺

在AI低谷与突破、数学与技术、创业与人生成长的汇流点，本期对洪乐潼的长谈，是时代青年科学家的真诚注脚，也为新一代AI+数理创新拼下了鲜明的路标与精神样本。

---

更多链接

• 播客公众号：语言及世界 Languageisworld
• 时间索引如上，可快速定位原文各重点话题

---

Transcript

[A]

Hello大家好我是小峻今天我们来到了美国硅谷此刻正在扎克伯格最早的创业所在地FacebookHouse这是一栋外表为淡蓝色的可爱的小房子而今天也将迎来商业访谈录最年轻的一位嘉宾她是一位0后的华人女孩名字叫洪乐彤她的探索方向是AFformat所創辦的公司Oxim剛完成了估值為16億美元的A輪融資而它引起了很多人的關注則來自於這樣一條新聞57歲的美國終身教授突然辭職去給24歲的華人女孩打工那接下来就是我对洪乐同的访谈因为我确实在每一个时期都觉得自己是那个环境里面最愚蠢的那一个最怎么样努力都看不到结果的那一个在你的心目中AF4MAD它在整个AI的大地图上它应该划在哪个地方我觉得大部分我知道的就是创业公司的创始人他们都对苦难上瘾我接下来我会有一个问题因为现在coding也很火对那用math作为手段和用coding作为手段去执行任务的区别会是什么呢没有人喜欢这种词没有人喜欢荣泽他不是说难结果难他就是累你是一个复读机一次一次的说一样的事情你一次一次的接到一样的问题真的我就能我可以把它录下来然后我就给你们大家发对吧你们反正问题也是一样的这个但是呢就是从这一些大量的比较无聊的这个过程中有一些让人很激动的谈话通常这一些谈话是你最终选择的选择的投资人比如我印象特别深刻的我们最后的领头房BCapital我跟HowardMorgan就是有一个对话哈喽乐同还是先给观众朋友们打个招呼并且做一个简单的自我介绍好哈喽小骏谢谢你邀请我我是洪乐同Axiom的创始人和CEO我想我们的聊天可以从一个故事开始就是很多数学家在说自己被数学打动的那个时刻都叫做被数学击中的时刻比如说高斯就说像闪电一样你自己有过这样的时刻吗我就是自己解题的过程中这个稍微就是低频率一些但是我经常在看别人结果的时候有一种哇这个东西怎么这么美的一个感受呃我印象中特别深其中一个例子就是说呃第一次看到这个呃模型式椭圆曲线定理就是说每一個這種模型式它都對應著一個橢圓曲線相當於是把一個比較代數性的一些一個表達式和一個更幾何性的一種幾何物體就是聯繫起來然後我覺得就是數學中這種两个领域然后他们相当于中间有一个交集的这样的一个例子还是每一次我都是觉得非常非常非常优美的然后呃我印象中就是还有另外的比如说概率然后物理那里面又有一堆的可以就是呃让我觉得非常就是有意思的结果呃然后我自己解题的话还是就是小的时候可能见的不太多就是觉得数学还能还能这么玩就是当时从初等数论的时候一直推推到这个二次互反率我当时在美国的一个叫罗斯夏林林然后他每一天就给你每一天给你一个题集然后你要把它全部做完还挺多题呢全部做完才能拿第二天的题集像游戏打怪一样然后如果你做不完所有的题他就不给你下一个题集然后你就看你隔壁的那个同学已经就比你就是多了三个提及有更多有意思的可能是正确的东西但是由于你的证明能力还没有跟上你一直到不了然后到最后到二次互反率的时候就是他给你呈现了很多的证明我在这个过程中一定是觉得有被数学击中的时刻然后就是觉得非常表达非常简洁的东西它后面的这个证明可以很深然后也可以有很创造力的一些解法我有一个问题它可能会很好回答也可能会很不好回答就是有一天我跟AI在谈论数学的时候他提到数学是一种结构的语言所以我想知道从你的视角来定义数学到底是什么对这个确实不太好回答我觉得数学它有一点像是说是人类我们决定说去创造一个文明的体系然后在这个文明的体系里面由于一些就是我们愿意去说是呃我们认为是是对的一些公理然后往上去搭建就是我们我们他其实某种程度上是数学家他有一个契约就是说哪一些东西我们是愿意接受是呃理所当然的然后在这些东西上面最少的理所当然或者说不一定是最少看你从哪一个角度去看有一些人他会去从compression压缩这里去去看他希望是最少的公理有一些人是去希望能找最有意思的或者说就是搭搭配最合理的一套公理系统然后往上再搭建然后往上搭建的这个过程中其实我觉得这个过程是很多人觉得数学是解题就是我有一道题然后我把它做出来但就是往上搭理论的这个过程其实很有意思一般是先从一些数学的一些例子出发一些它就是比如说是一个序列或者说是一个集合然后你去发现一些规律然后这个时候你觉得很自然而然的下面的一个题应该是怎么样的然后再去证明它所以这个过程其实有一点点像艺术我觉得数学是一个介于艺术与科学之间的一个存在所以数学到底是一个被发现的过程还是一个被创造的过程这是一个千古千古的难题的辩论点你是哪一派我觉得就是如果一些数学家他们有一套比较相似的训练背景或者说他们在同一个领域里面他们阅读了同樣的一批代表作他們會有一個某種程度上比較大的一個默契去說我們認為這個很自然而然的它應該是是什麼樣的然後如果說出現了一個比如說最有意思的就是當拉馬努金他從印度來到了英國他遇到了這個哈代和LittlewoodHardy,Littlewood他们两个人就是一直就他们两个写paper他们写了很多很多的文章然后拉玛努金来到这里就是像一个外星人一样他说嘿这是我的这个草稿本上面这些东西全都是对的我从来没有接受过数学的这个训练我不知道怎么去证明它然后Hardy和Littlewood就会觉得这些东西看起来很有意思他们很新然后他们和我们之前做的东西又感觉这个东西是对的但是所以他们就开始用证明所以某种程度上证明是一个与原来的这一群数学家所不太一样的一些人他们可以用证明来说服他们证明其实某种程度上它是影响力就是我只要能够去把这个东西严丝合缝的逻辑证明出来我这个数学的发现就是可以被接受的然后在它被接受的这个情况下当然了又会说你这个证明是美还是不美是自然还是不自然这个我们之前看到很多国际的数论学家去看张一唐先生的这个的数论证明他们就觉得这个证明是和他們熟悉的一些學派非常不一樣的一種證明方式但是在就是非常著名的那一個結果就是素數的這個固定的這個差這個他們覺得是正確的所以他們又接受了這件事情於是就是又开始去互相的去学习和整理他们的证明方式比如说JamesMaynard20年的菲尔兹奖他有另外的他的一套的证明的这个技巧然后他的学生们去继承他的证明的技巧然后他和这个张立昶先生的这些就可以进行大家可以进行比较也可以进行简化这个过程其实是非常非常有意思的一个一个智力过程你是哪一派呀是那种直觉派天才派还是证明派我一直就是非常希望能当直觉派天才派然后这其实是我很小就是痛苦的一个根源就是我一直发现我自己没有什么特别大的数学天赋就我是一个蛮类型选手对我是蛮类型选手就是你给我我小时候在打数学奥赛的时候我记得他们说就是每个卷子的第一道题几何题欧式几何题歐式幾何題是必拿的分你如果不拿歐式幾何題你連這個三等獎你都拿不到然後我就一直做不出來歐式幾何題我倒是可能能做代數不等式我的大腦可能更偏代數的符號的表達然後幾何和拓撲實在是差所以我一般就是去把每一个点然后每一条线就用这个复述法就是大力出奇迹我最后我不需要去理解这个几何题它背后的几何意义我就把它完全是就是照本宣科的去拿一个套非常复杂的复述法去把它就是解决出来我可能会需要比别人多两到三倍的时间导致我可能其他题目的时间分配不均但是這是我做這個幾何體的唯一方式其實最有意思的是201年開始就是GoogleDeepMind他們從他們很秘密的開始一個這AlphaGeometry的這個項目就是說如果我們這個拿AI去證明歐式幾何體非常困難感到困難能否把它變成符號表達他這個不是複數法跟我說的這個人類我這個人類做的方式是不一樣的但他這個背後的哲學是一樣的我把幾何的圖形變成這個符號表達式於是這就是他們就能夠通過這個東西去解決好像81%的就是AI能夠解決81%歷史上IMO的幾何題就这是一个很有意思这是一个我不是天赋型选手的这个解释解释一我有一个解释二就是我在MIC的时候我身边所有人他们都是天赋型选手所以你只要就是看看左边看看右边就知道自己不是天赋型选手但是呢我不放弃我是打不死的小强就是你给我一道题我三个月我做不出来我继续想我记得当时HenryKong教授他给了我一道Spherepacking让我去想一些关于28维的这个Spherepacking的一些小的问题这个东西当然不可能就是期待一个本科生完全解决然后我六个月我什么都没有想出来但是我每一周我就去说哎我这是我试过的我没有成功然后我又试了一周我又没有成功所以但这个这种蛮例行其实某种程度上会和一些天赋型选手存在一个互补就是说他们可能有一些脏活累活不愿意干的我可以把它去干完所以你的這個過程有點類似於AI的過程AI是這種蠻力型選手嗎AI是直覺派嗎現在AI裡面它也分了這個比較天賦型聰明型的AI和這個和這個比較蠻力型的AI比如說我們現在這個我們公司的這個AI系統它里面就是它是一个系统所以它中间有很多的模型它有一些模型就是能够很快的去认定这个题目应该是被1234567步这么大概证明出来然后就是偏形式化见到了很多另这种形式化语言的AI他就会说哎反正我就是一个tactic一个tactic的tactic是另里面的一个步骤或者说是策略它能够让你就是从把你的一个很复杂的问题一步一步的去把它解决它更是这种严丝合缝就是小步小步走然后不是之前刚才讲的那一个能够裂提缸的AI所以其实AI这系统里面两种就是类型的AI数学家他也能相辅相成某种情况下其实最有意思的是当看到一道题就是我们发现在我们最近我们公司在这个普特南大学生数学竞赛中就是这个ActionProverAI拿了满分然后是人类历史上有五个满分过去的98年1001927年开始第一次普特南数学竞赛然后这是第六个满分是一个AI拿到的然后我们就有看这个AI的解法有一道题我印象特别深刻我们队伍中有这么一个同学他叫做EvanChen他是美国IMO数学竞赛队的教练所以他是非常天赋型的一个选手他看到这道题他画了一个图然后我们所有人当时在那个会议室一看到这个图我们就说那你是把它做出来了就一个图的一个解法這個AI果然就沒有找到這個一個圖的解法我們看到了就是幾千行的這個lin代碼它是就是硬生生的把它某種類似媒舉類似分類討論然後就是一步一步一步核實去把它就是幹出來的所以就是这是一个大力出奇迹的AI它可以看到这个机器它会去就算是一道很明显可以去做创造力解法的一道题目它可以去通过它自己擅长的东西去给出给出一个完全不一样的解法其实我觉得去比较人类与AI就是得到的这个证明解法背后的数学是一个非常有意思的过程所以數學不是人類的特權對嗎? 現在感覺上這個自動定理證明這個領域發展得很好其實這個領域它不能夠叫是AI的勝利它在沒有AI沒有這個深度神經網絡的時候就有一群電腦計算機科學家他們就是去希望能夠使得基於規則的電腦系統能夠去幫助人類去解決能夠解決的數學問題然後這就叫做自動定理證明ATP然后ITP就是交互性定理证明互动性定理证明就是毕竟有一些ATP无法解决的就是过去会有一些人类他们是数学家他们也会去写这种Lin这种特定的这种程序编程语言他们就会去与这个电脑系统一起去合作证明这件事情现在其实我们只是把这个ITP中的这个人类换成了一个AI這個古老的學科其實某種程度上是ATP與AI的交集我相信很多人都还是会对你很好奇你虽然一直在说你不是天赋型选手你是一个蛮力型选手但是你的过往的背景非常的强所以还是想聊聊你自己你在广州长大广州是一座非常有烟火气的城市所以你的小时候的成长环境是什么样的对广州是一个非常非常有烟火气的城市其中我最深刻的一个童年记忆就是确实有很多好吃的就是感觉到了后面长大就是留学感觉就是食物上比较比较匮乏尤其是和家乡的家乡的美食比起来呃我爸爸妈妈啊我们是在广州啊我在广州出生长大然后我们住在就是离学校很近所以就是每天可以走路去上学然后有些时候上学的时候就也会想想数学题然后也走到不知道哪里去就是这种呃说是就是想数学的同学们经常犯的这样的这个习惯我也有呃走路到需要多多远呃就十分钟然后就是有时候会会开始游荡因为就是就是有时候脑子会想想别的事情其实我觉得这是一个非常快乐的一个状态呃后面就是我最近创业呃我有一个这个呃导师他讲到一个概念就叫做呃bondedattention和freeattentionbondedattention的意思是说呃被框架住的注意力然后freeattention是说自由注意力比如说我们每一天早上起来我们会看到很多邮件然后我们会有很多我必须要执行的事情因为我不执行这些事情可能说有一个期限性你必须要把它执行掉这个时候你的大脑是在一个被框架住的注意力的这样的一个情况下对然后很多很成功的企业家他们是非常有纪律性的执行家他们就是每一天日复一日的去compound复立他的这个执行呃这个很好然后所以我一开始就是创业的时候非常希望我每一天能做多少事情做多少事情但是就是后面这一个自由注意力其实是能够区分一个平均的一个创业者和一个很很好的一个很有呃策略性和决策性的一个创业者的一个区别其实是在自由注意力这里或者说一个数学家自由注意力这里是可以把人与人之间的这个差距拉开了点所以當你所有的時間自願的去由於說我要做一個像就是像軍訓一樣我每一天就是要幹掉多少活你可能會使得你這個自由注意力這一塊反而是欠缺了你喪失了很多的機會成本所以我就是就是特別有時候懷念小時候就是走路上學的時候就是有很多這種自由注意力某種程度上就是就是人家說愛因斯坦的洗澡事件這個過程中其實能夠呃有很多很有意思的一些就是大腦能到一些很有意思的地方去这可能是灵感和直觉来到你的大脑里的时候对但是这个事情是它不是一个线性的不是说你投入多少自由注意力的时间其实也有可能自由注意力的时间你什么都没有想到然后在后面的你可能在被逼迫做一些任务的时候在中间你会就是有一个callback就是回到了你其实自由注意力给你大脑里面打下的这样的一个一个一个基础你反而会在那一刻可能可能你大脑也不想做那些无聊的事情他就说我想到了这样的一个比较有创造性的一个一个想法所以自由注意力和邦利的尊甚和限制性的注意力它应该是结合的它有配比吗呃不知道我觉得大家的配比不一样人家说有三种创业者第一种叫Visionary就是有前瞻性的野心家第二种叫做Executioner就是执行他就是能够其实扎克伯格我们在这个Facebook小屋今天特别特别有意思的一个场地扎克伯格他就是一个执行狂就是他是一个执行执行执行执行执行的一个人然后你可以看到他每隔一段時間會有一些行動去彌補可能前瞻性的決策落後所以它是一個非常就是執行的執行派的一個企業家然後第三種就是銷售派就是它是能夠銷售派其實並不是一個負面的詞就是它有非常好的溝通能力它有非常強的與不同的這個受眾溝通的能力然後它能夠去影響別人引領別人然後把一個隊伍就是這麼建起來呃我我一直从来不觉得我是销售派这个是肯定肯定不是的呃然后我也不是一个多好的知性派其实我也我可能就是也不能叫做前瞻性这个前瞻性是说是对的我就是想做一些事情然后我想做一些事情会极度乐观然后我极度乐观的情况下呃就算是往下就是跌一点他好像也也还也还行也还达成了一个一个kpi所以你觉得你是第一种Victionary我觉得我是Victionary我反正肯定不是Salesman或者是Executor你刚才说扎克伯格是属于第二类他是第二类对你觉得像其他的一些企业家呢在美国这边一些知名的企业家虚名的企业家马斯克是是是是visionary这个是绝对的然后SamEllman是salesman啊然后啊我觉得一定要互补就是嗯比如说扎克伯格他身边全是梦想家看SHREP这个CTO梦想家嗯他也有其他很好的执行的其他执行的人就是我觉得光互补也不行你要有一些是你的同类然后有一些是互补呃桑德伯格做了很长时间的很好的执行家呃稳健的去呃把零到三千人的情况下这个文化都把持的很好其实我觉得facebook非常强的一个点是就是每一个facebook的人他们都bleedpurple就是他们的血液里面就是紫色就是就是facebook的这个颜色他们紫色紫色代表什么呃紫色就是facebook的办公室有很多呃很疯狂的颜色其中有一个很明显的是紫色其实这个是因为扎克伯格他是他是嗯colorblind他是有一些颜色光谱无法区分所以说他的那个就是办公室有非常大胆的大胆的颜色和其實去看那個Facebook的這個園區像是一個夢工廠它有24小時的這個雪糕店就冰淇淋店然後有地方讓就是大家去玩鼓玩吉他玩樂隊我們公司大部分的人其實之前都是在Facebook的所以你很了解他们对他们有一个非常强的一个叫做bottomoftheculture就是由下往上而不是往而不是上行下效他是这不是topdown就是topdown非常google然后bottomof非常的非常的facebook所以我们公司其实某种程度上呃并没有一个定义文化的机会我们某种程度上沿袭了呃我们大部分的早期创始员工他们本来的文化好的关于Facebook我们后面还会聊到我们先回来你在广州那个城市是怎么长大的对就是打打数学竞赛然后我看看百家讲坛我是非常喜欢这个百家讲坛对我非常喜欢就是所有的就是中国的这个文学与历史我喜欢就是看那些历史故事我当时记得就是一中天讲三国然后住自百家然後就是還是非常快樂的一段時間我特別喜歡文學就是黃永裕他有一本書叫大雅堡胡同甲二號然後比我老的老頭就是那本書的書名然後其中講到了這個中國的這個文藝界就是畫家然後作家然後他們各種各樣的畫家版畫家雕塑家然後他們都住在這樣的一個北京的一個胡同裡面我媽她是北京的北京人所以说我们家某种程度上我们虽然住在广州然后又有受很多这种京城文化的这个影响对所以我发现你小时候自由注意力是很旺盛的很旺盛的自由注意力因为你并没有把所有的时间都集中在数学上我对我也被数学教练小时候就批评说不是最刻苦的那一个但是我如果遇到一道题这个题就是要跟这道题去死磕就这某种程度上你如果看我花了多少时间的那道题上你会说这个小孩很刻苦但这个过程中像玩一样他不他不像work就我觉得区分说是呃这个框框住了的这种限制性注意力和自由注意力的这个其实一个主体感知就是你到底觉得你是在玩还是在工作然后我觉得呃我小时候大部分的事情都感觉是像玩然后就是那些学校作业就是一般课间就是写完然后我放学之后就所有的时间我就是可以做一些其他的其他的事情呃后来就是大概是初一的时候呃发现就是可以去可以发现了一个一个事情就我可以去找一些就是更高等的数学书看就是小时候是意识到说我一直要做数学竞赛嘛所以我要比如说三年级做五年级的数学竞赛提级就是一直是做数学竞赛更更更更更高级的但是到初中的时候就开始我为什么不去学学高等数学呢所以就是开始看就是微积分啊就是当然十分析负分析哇然后就觉得非常有意思因为它不像是一个零和游戏了就是做数学竞赛的时候总觉得其实比如说在这个广东省的这种奥数这种这个训练环境下比较痛苦的一点就是你的同学们他们要跟你考同一场试所以对于一个一个小孩来说这种友谊的这种概念也比较复杂就是竞争它就是特别存在但是你如果是看高等数学这个它不是一个零和游戏它是一个正和游戏你可以自己就是到你想到的这个深度广度然后你可以找一些你们班里就是对这个比较感兴趣的同学们一块去讲然后你们不需要某一天同时去参加某一个考试所以但是你还是要回来打这场零和游戏对我还是要打这个零和游戏然后这个就是零和游戏上就非常吃亏了有些时候看到一个一个卷子吧就是四道题最后一道你就发现是数论数论多美啊你你可能刚最近看了这个高等数学里面去学了更多就是数论的这种这种这种高级的这个这个概念然後你就一套卷子你如果你的理智會告訴你你要在這個零和遊戲中取得高分你應該先把第一道歐式幾何題把它做出來接著你做第二道代數不等式然後最後這道數論題大概率你是做不出來的你要是做出來你就進省隊了然後所以你不應該拿到這個卷子的第一課先從最後這道題開始但是我当时由于我就是课外的这种非常浓厚的兴趣加上我非常的喜欢数论我长大也是就是做数论我觉得我非常非常的爱数论于是我就会先从这道题开始然后一般来说这个时间就开始流逝然后在一个一个一个固定的一个比赛时长中这是一个不是最优的策略你是一个竞争力很强的人吗因为你刚才也提到就是在打比赛的过程中这是一场联合游戏也会影响一些友谊你是一个竞争力很强的人我觉得我在拒绝被驯化成为一个竞争力很强的人你在拒绝对我在拒绝被训话成为一个人你初中的时候意识到的? 我意识到的对我当时你很难不意识到你小学数学奥数奥林匹克学校的时候我记得四年级到六年级对吧每一个月考一次试然后每一个学期之后他把你一班到二十四班全部重新排列就是说你如果二十二二十三二十四班是重点班然后就是一班在这个楼底二十四班在楼顶然后你每学期之后就是把你这个就是同学们就是换换教室二十四班都下去了下到十九班了不是重点班你楼梯也往下走你这个心情肯定也不是特别好一班在哪一班在楼底啊我当时进去的时候我是四班然后我记得就是就在这个洗手间旁边这个感觉就是说明这个我入学考试考的是真差对吧不是天赋型选手就猛足了就是想上这个234的那个楼顶听说楼顶这个风景也好对吧就一个四年级的一个小朋友他肯定是会有这种就是争强好胜心就是在一个比较大家就会有这种压力的感受然后我后面是觉得就是这个不好玩我不想玩这个后面是什么时候初中吧初一初二就我开始看这个高等数学书的时候我就开始不太想玩这个游戏了哦那你做出了什么样的改变呢在你不想玩这个游戏之后嗯就客观条件上你还是要去参加那些考试你还是要去排名你还是要去竞赛我不是那么在意了就是我一直不到初三我没有就是初三要打初中数学联赛了然后我就是呃开始初一到初我临到临初中数学联赛我才开始准备初中数学联赛最后好像好像也考的非常好这个初中数学联赛就是反正我当时还特别就是惊讶我觉得我肯定是要考砸但是呃初中数学联赛考的挺好然后到高中的时候就是更多的时间就是呃当时还学英语对高中的时候又又更多的去学英语毕竟当时也打算是要出国所以就是更多的时间花在这一些这一些事情上面然后呃我我其实觉得做出来的改变改变其实就是我发现一个有意思的事情就是你在一个群体里面你如果发现大家有一个很清晰定义的一个目标然后每个人都往这个目标也就是当时的不管是下一个季度的什么数学竞赛开始准备的时候呃然后你自己有一套完全不一样的这个呃mentalmodel世界世界的这个模型你就会开始找呃这个群体里面的一个tribe一个部落你会希望能够去建立一个小的一个部落然后去找看谁跟你一样想读这个跟这个考试没有关系的书然后你就会和这些人成为很好的朋友我记得我初中的时候有一个游戏我到现在其实我们也在有时候显得无聊也在玩就是你有一个N乘N的一个格子你有一个棋盘比如说8乘8的一个棋盘然后你可以从这个任何的一个格子开始去走马步棋就是你只能去走这个跳马就是2乘3就是的这个每一步你只能这么走然后你连续的这样去走然后你每走到一个格子你就标1234就这么开始标最后你的目标是说我能够走满每一个格子不重复或者说你走不完每一个格子你希望走到一个更高的一个数比如说8x8的话你希望尽量靠近64你不要在50你就停了你希望至少到个59就是这个游戏我当时我记得我初中就和好几个好朋友们一块玩然后我们就特别希望我们一个一开始开始比看谁的数更大后面我们就希望能够去证明说任何n至少是5的一个棋盘你永远有一种能够走满整个棋盘的方式我们希望拿就是我们当时猜测应该能拿数学归纳法去证明如果你要去拿数学归纳法去证明你就需要在N比较小的情况下去构造一些比较有代表性的一些basecase基础情况于是这个是一个非常复杂的工程让我们所有的这一些对这个游戏比较感兴趣的同学在华复我们就开始去构造然后非常难构造然后所以就是群策群力一起构造让我有一点想到我们等會我們應該會聊到的就是形式化證明比如說陶喆軒老師還有就是AlexKontorovich他們做這個素數定理的這個證明然後他們就是把它也是分了很多項不同的項目讓全世界的幾百個數學家和另的這個編程的同學一起去把這個事情搭起來有點像就是數學其實某種程度上大家強調說这一个人他是一个天才他一个人证明了一个困扰其他所有人几百年的一个猜想然后他是一个多么厉害的数学家他有一种个体性的一个强调就是说这一个人他非常厉害但数学如果你去看软件工程师他们几百个人几千个人去做一个一个project一个大的一个项目它是合作性的合作性就需要一个比较好的一个结构和把它就是把这个任务去分散分散成不同的小任务这个过程其实我觉得是很有意思的然后某種程度上在玩這個馬步棋的時候我們當時就是我反正一個人肯定是不可能把所有的這個例子找出來的我需要我的這些同學們這個小部落的這個幫助多少人這個小部落一般是三到五個人三到五個人對都是數學很好的人我們當時是那個數學班就我們整個班都是數學很好的人然后就是上课就不听课了就是就是传纸条那个纸条上就画着这个格子就是说这个你看我又找出来这样的一个就是n等于比如说9的时候已经被我kill掉了就是非常快乐的一段时间在这个这么快乐的时候你的成绩是什么样的呃就我反正要不到大考我也不太我还还行吧我反正也到了那个反正你的最终的目标就是你初中好像我们是九十个人你要进到一个二十二十五二十七个人的一个一个数学组高中这个数学组所以我也进去了我记得我们当时是啊七个女同学好像初中然后啊到这个高中好像就是二十五二十七个人三三四个女同学反正就是也那也那也那也进去了但是这就很奇怪因为你说你不是天赋型你是买力型可是你实际上花的时间没有那么多对这就是一个很有意思的一个点就是我认为你在学这些高等数学的时候某种程度上你的竞赛的这个数学也在得到这个前移默化的提升就这是这其实是很有意思的就是我们等会应该可以讲到就是我们发现最近有一个AI的一个发现就是说我感觉我像是这真的是我每天在想的事情我不是在打印过就是一个数学非常好的一个模型它在编码能力上也非常好就是它会有这种东西叫做transferlearning就是转移技能的转移呃我觉得肯定有这么一定的程度反正我当时我记得那个考试嘛就是从初中考到高中的那一个考试我是觉得我肯定要完了然后我的爸爸妈妈说你应该没事你就去那里坐一坐你看一下就是结果怎么样反正觉得应该你能考好然后结果我觉得我应该是拿了满分那一次然后我觉得我连几合题我做出来了我十几十几个嗯十几个大大的考试中没有做出来过一次几个所以那次也可能是运气比较好哦这个很神奇就是从学习上对于你来说突飞猛进是来自于你其实变得更发散了而不是更聚焦了你不是更努力的去做题了而是变得你可能兴趣爱好更广泛了你更想玩去做这件事情了对对我当时是这么觉得的但是这个事情到后面我在大学的时候在MIT的时候就觉得还是要学会聚焦哦我觉得可能就是数学好这件事情它没有公式然后我一直也不是数学最好的那一批就是每一次大家可能说你以前打数学竞赛然后可能现在在计算机的这些同学里面我有一定的这个数学背景但是我在麻省理工的时候我身边的每一个人他都比我聪明每一个我是整个数学系里面最愚蠢的是你自己这么觉得但是别人也觉得自己才是最蠢的那个我觉得他们应该是意识到他们是很聪明的他们意识到自己是天赋型选手的对哦为什么呢为什么你会有这种感觉你觉得自己没有他们聪明就是你的背景在别人看来就已经是天才型的选手了对但是我当时我的同学们比如说任秋宇张声彤高纪阳就是这些人每一個人都是在這個我小時候看著他們的新聞長大的我看著他們的新聞長大看到他們去了北大術院看到他們轉學到了MIT見到了真人我每一天就是在就是頂禮膜拜這些大神就是我當時在MIT的時候這種这其实是一个非常有意思的一个一个点其实甚至是有一些其他的小国的这个IMO的选手比如说我有一个好朋友他是这个比利时的这个这个IMO来到MIT看到美国和中国的IMO们然后也知道大家的IMO分数他也会有一个心理落差我这个其实没有落差我的期待就是我是最最傻的一个所以我我其实就是适应的也很好我反正我就觉得我每天很幸运我和能能能和这些人一起说话一起上课一起做作业我觉得还挺好所以你对你预期没有那么高我预期没有那么高我觉得我当时觉得我来到MIT吧我可能以后就去做这个量化金融了因为我可能反正你说这个数学博士为什么他会要我而不要其他每一个人都是IMO金牌呢就是他肯定肯定我觉得我肯定也考不上数学博士所以我那我就反正我记得我大一的暑假我就是呃本来是要去桥水桥水基金去实习啊因为当时就我想着我要做金融了那我肯定秋天就是校招的时候开始打一去递典礼然后我记得去去啊还是挺高兴的就是能能当时去桥水然后当时疫情来了疫情来了的话就呃桥水就变成从一个呃就是呃线下的变成一个网上的这一个实习了然后同时当时就有另外的一个机会就是呃我当时被呃professorcanno呃小野肯老师我们就是他现在也在action对他是当然他是一个就是神级教授他有一个就是REUREU的意思是ResearchExperienceforUndergraduate是在美国是一个名词就是给本科生的暑期数学研究项目这些项目他们竞争非常的激烈他们是美国的这个自然科学委员会他们去赞助的所以他们的这个经费有限經費有限就是能去錄取的同學們也有限然後我當時就被小野肯教授扔到了這個waitlist候補名單上然後他給我發了一個郵件他說我在候補名單上的名次比較靠前然後我當時感到非常的激動因為當時我身邊的朋友們我剛才講的這一些大神們他們都已經被錄取了他們在同一天已經收到了錄取函我看到了一个邮件说我在居然能够到这个候补名单上我居然还能够在候补名单上名字比较靠前然后我当时就觉得我可能还是想去做数学研究因为我觉得我如果这个暑假不去下一个暑假可能就不要我了我可能连这个候补名单上我也上不去了所以我就最后居然被捞上来了因为可能疫情吧可能好多同学他们就暑假不想在一个一个一个一个数学夏令营他可能还是想比如说就是在家里可能隔离呀之类的所以拒绝他的人那一年比较多我就被捞上去了我被捞上去之后我就没有去敲试我最后是结束了大学结束的时候那个暑假去了去了敲试你们家里有刻意的引导你在数学上的发展吗呃我觉得有我觉得我妈妈她有一个这个危机意识她小时候数学特别不好然后她哦是吗对你们家大人有数学基因吗没有就是彻底没有哦嗯他数学特别不好他数学就是他其他可能都好他就是数学不好他就觉得说你要不就是先就是学一学数学因为可能到后面你数学会是你学科里面比较落后的一个他是觉得你可以就是笨鸟先飞一下你的青少年时期获得了特别多荣誉这个非常的长我就不念了我们到时候可以给大家打出来小朋友时候的事情了对只是小朋友时候的事情那这些对你来说是轻而易举获得的吗我们刚才聊天的经历他们好像都不是你的当时的目标对不对他可能考试前两三个月成为了我的目标我觉得我还是比较喜欢去做一些有创造性的事情比如说我记得当时大部分的时间确实花在了就是对于数学自己的探索上然后你说这些目标它其实跟这个也有很大的关系嗯对它反正都是数学它只是类型不一样你可能说准备奥赛我也有准备奥赛的时候我准备奥赛就是在好像是很短的一段时间里面就刷了75套卷子然后就是就是当时它其实是一个纸的那个杂志然后就一页一页的每一天就是做一页然后做完把它撕掉然后就是75套卷子75套卷子做完之后没选上去打那个比赛就是我觉得我的这个所以一直对荣誉这个事情我的感受非常复杂因为我确实在每一个时期都觉得是自己是那个环境里面最愚蠢的那一个最怎么样努力都看不到结果的那一个然后最呃绝望某种程度上就是对他不是一个在舒适区持续的不在舒适区是一个非常嗯我觉得是对人很有就是塑造的一个一个体验就是失败是你的默认项你是在持续的不在舒适区对自己的要求比较高你就会觉得什么都是失败但是你又很乐观对就你没有因为失败很痛苦没有就是你我觉得是可能是因为你很乐观所以你经常失败你每一次就很乐观觉得自己能够到达一个一个去希望能够去成成成就一件一件事情然后失败某种程度上去自我定义的并不是说客观定义的可能客观看来不是不是失败你们描述一下你的一个失败的体验内心的体验它是一个外界的什么事情触发你内在的体验对就是麻省理工的第一个学期它有一个叫做成绩保护成绩保护就是所有的这些新生的同学们他们都可以就是上任何你想上的课然后你不需要去担心你的成绩不是一个A因为这个GPA变得非常的重要我身邊有兩類同學我當時住在這個麻省理工的一個很有特色的一個宿舍樓我們這個宿舍叫做東校區東校區的這個如果你走到東校區的這個庭院裡面會看到那種木頭做的過山車兩個樹之間有繩索然後有一群人在玩噴火就是這是一個非常麻省理工精神的一個黑客的一種一種非常nerdy的這樣的一個文化大家就是我反正我当时住在这里给觉得非常有意思然后我在整个东校区的这种环境下我在西边楼的三楼这个threewest这个叫FloorPieFloorPie就是因为它是三楼所以大家叫把它叫做Pie楼就是圆周率楼然后这个楼上住的全是IMO就是这个楼上不是IMO就是IPHO物理物理的或者是IOI就是信息奥赛遥远住在这个楼上就是这是美国的一个奥赛选手然后呃这个台湾的这个呃于宏勋住在这个这个楼上就是我们整个楼每一个人都是我的偶像然后所以他们就给了我一个建议就是说你就是去上最难的课然后你就是去上呃你可能都呃没有这个预备知识的这个课然后我就真的去上了这个课因为我身边的当时玩的比较好的同学可能都非常的有这个乐观精神他们可能也从这样的学长学姐这里听到了一样的建议所以我们有好几个这个大一的这个小朋友去上了这个博士概率论不是概率论我们想哎概率论嘛这个我们知道概率论是什么我们就开始在想一些可能让我们算一些可能比较复杂的不会算的概率不对第一天开始上来测读论测读论从这个从BorelSigmaAlgebra开始讲起从这个测读论背后的代数一个叫Borel的代数开始讲起我们就面面相觑我们完全不知道这个发生了什么然后这其实我觉得是一个很有意思的一个体验因为它不是一个竞赛环境下我自己一个人考砸了的这种失败就是有好几个这个同学们大家一块去去感叹一个事情很难然后在一个在解题小组里面我们一块去尝试就是群策群力去把这个题集MIT特别倡导合作去把这个题集做出来然后这个这个过程我觉得特别特别有意思所以你这次就是你的不舒适感是来自于你选了一个更难的东西对这个考试好像是满分试卷是40分然后这个期中考整个班的平均分就连带着我不知道是混进来了多少我们这种吃了雄心豹子胆要上这个课的本科生平均分好像只有9分哦就是平均分只有9分然后我们我们我们的分数都是5以下的个位数我们这几个大一的小孩所以我们肯定是拖这个平均分后腿的这个主力军哦那你的失败体验来自于哪里来自于你我从来没有在一个考试上看到自己一个40分的考试我能拿4分4分对但是你知道这是因为我选择了更难的事情我觉得它也不会触发你自己觉得自己很失败的这个极致对对我什么失败都不会触发我自己觉得很失败的机制就是我把这个失败当做是我的这个default默认项嗯对所以我就开始说那我要学分析这个课我学不好的原因就是因为我的分析的底子不好于是我就开始很认真的去重新把我可能十四十五岁学过的Rudin的识分析我又再学一遍嗯那你的自我奖励的机制是什么呀你在追求什么呢你在那个时候你这是你选自己选择的一些选项我自我奖励的机制其实这是一个很好问题其实它有很多重机制我觉得我有我在就是年纪比较小的时候这种社区感或者说我有这个朋友或者说我有战友们这个大家有这种comradery同志的这种友情一块去做某一件难事情MIT他特别倡导就是攀登就是登山队这个会给我很大的一个奖励的感受就是我们没有放弃就是我们期中考完了之后我们大家一块说要么就一块droptheclass就是都把这个课给退了那么就一块继续继续做反正就是也有这个保护机制了第一学期然后我们大家就决定一起继续上这个课就这个事情我年纪比较小的时候这种奖励的这种感受其实来源于这个社区或者说是小团队小团队然后呃我不知道是为什么反正近几年是不来源于人了近几年来源于就是可能这个非常难的这个事情本身就是近几年可能可能我觉得是年龄小的时候承受能力虽然说仍然说是就是经历了很多失败的你自己感觉到麻木对吧仍然不有没有这种失败的感受但是在近几年可能真的是对这个东西完全没有负面的感受所以就是这个难的事情本身我有种对painandsuffering这个黄仁勋老师讲的这个有更多的这种suffering反而对这些事情有点上瘾为什么我觉得大部分我知道的就是founder就是创业公司的创始人他们都对就是苦难上瘾嗯就是对苦难上瘾对就是其实这是一个不一定很健康就是甚至就是有一个有意思的我听一些风险投资人他们说他们找这个方的就要找这种对疼痛上瘾的方的我我听起来这个感觉非常的这个不可理喻对啊就是他们有一句话叫做chipontheshoulderchipsinthepocket就是说我感觉我的肩膀上有一些重量可能是我以前的一些伤痕这个chip就是在这个肩膀上的这个chip能够转化成口袋里的chipschip就是硬币就是钱就是就是可能说某种程度上对于腾腾的上瘾从这一些当然从这一些风险投资人的角度上来说能够转化成一个呃小创业公司的成功嗯呃这是一个我觉得比较激进的一个理论但是某种程度上它有它有一定的一定的正确性在里面嗯你从小团队的这种奖励机制到这种事情的奖励机制这个分析线要画在哪疫情骂上理工就你没有团队了就是MIT毕业了以后就是不是不是我我大一的时候下学期就疫情隔离了ok所以等会你零零几年我是我01年哦对我01年然后还没有到254对然后我24特别好一个数你可以玩24点哈哈哈对然后嗯就是对对对当时就是就是大一下学期所有人就就赶走了呀就不在学校就是呃offcampus了然后所以就没有小团队了那那课还得上对吧那你必须要去学会从这个这个事情难的事情本身里面去找找快乐的感受所以我当然觉得就是学习曲线是非常陡的他对我MIT对我是性格真的是有很大的一个塑造我觉得就是每一个呃我遇到的在麻省理工的同学他们都特别能吃苦他们会在雨天暴风雪里面去跑晨跑就是我前一段时间我上周末还去了波士顿一趟就看到又是一个下雪天那个暴雪风暴红色警报他们还在跑步这是一个非常有毅力的一个学校然后这种毅力它是非常有感染性的它让我终身可能无法达到MIT希望我们能达到的那种毅力的程度但我会希望往那个方向努力就是什么难做做什么什么痛苦做什么什么长期主义做什么然后对还有一个我觉得就是刚才讲到小团体这件事情就是呃他也就是训练了就是说在压力来临的时候其实对任何的人际关系都会有一个比较大的挑战就是可能说是呃有一些呃一对一的这些人际关系也可能是一个团体的这个人际关系呃保持自己任性和就是自己的内心的这种坚持和能够去影响或者说是不一定说是影响吧去促进一个一个团队他们都有这种感受其实我觉得这是一个非常非常非常困难的一个技能然后这种技能我记得当时就是呃巴菲特查理汪格他们就有在一个访谈中讲到说如果你看到这样的一个人一定要把他就是呃就是招进你的这个组织里他的他的信号是什么他标志是什么标志是一个嗯自己内核很坚持很技术派的一个人同时能够有领导力但是领导力这是一个非常满的一个词就是leadership在美国的语境下我觉得和中文的语境下它有一定的一定的区别我还是觉得就是你千万如果你想就是领导力里面领导两个词你就没有办法有领导力就是一定就是服务型跟随型哦对就是最好的领导力可能是服务最好的领导力就是别人就是就整个团队在登山的时候啊你不是前面那个拿着喇叭的那个你是就是后面递水的那个嗯你刚才说不想打零和游戏嗯那你觉得你当时也打的是一场什么游戏啊但是就是如果我去学高等数学的话我就可以就是有种就是你感觉有浩如烟海的不是你已经知道的这一些数学的这些概念它其实这是一个很有意思的点就是我在数学的竞赛中我是有一个就是syllabus就是有一个考试要领可能说每一年就是都是这些考点然后在高等数学里面我只要去新引入一个定义新引入一个概念我可以基于这个概念与以前的这些概念去呃发散出新的这种定理和问题然后这个某种程度上开始像搭积木就是其实有一篇就是AIforMath的一篇文章叫做LegoProver就是就是说像勒高积木一样就是你可以往上搭一个搭一个自己的小宇宙这个这个过程是非常快乐的这个过程是不受竞争所限制它不受竞争你就是在跟就是你可以在历史上的这一些站在巨人的肩膀上去探索一些事情对你为什么高中毕业去美国读本科而没有去比如说清华北大这样我是非常确定我是希望能够出国我挺喜欢麻省理工的就我可能也确实看了一些电影我在草稿纸上写MIT我可能不一定是想出国我可能想来MIT为什么? 哦,那个段子是真的,是吗? 这个故事是真的,我真的在草稿纸上写的对,如果说我想去另外一个学校,比如想去哥伦比亚大学,Columbia可能要写的比较长,MIT多简单,就三个字母哦,是在数学草稿纸上写的对对对,就是数学吧,就是必须要一张白纸,必须要一个铅笔,不然反正也什么也做不出来就是有一些数学家就是他对这个纸质和这个笔他也有一些挑剔我是这样的人然后如果你有一支非常好的铅笔然后你有一个白纸的话你就开始想画画然后你可能就是我还画很多图形我经常我直到现在我们Axiom的这个办公室上白板上如果你看到那种素描的那种立体立体几何图形就是我画的就是我喜欢Doodle所以我就是我Doodle的一部分我就会写MIT我对MIT信念感特别强我非常想去那里我看了比如说从这个就是GoodwillHunting这个电影对吧里面讲的就是这个MIT那个非常标志性的这个大大拱廊就是InfiniteCorridor叫无限走廊这些这些事情对于一个一个一个小孩子来说我觉得是有很多的理想主义在里面的这个是怎么种到你脑子里的MIT这个怎么我怀疑就是看电影就是MIT它可能就是在這個popculture流行文化中它成為了一個哦哦不還有很多很多的這個數學家物理學家他們是他們是MIT的尤其是還有還有很多宇航員他們是MIT的那你為什麼本科學的是數學和物理啊數學唄對肯定我要學數學這個我是知道我第一天他們還講說怎麼樣去探索你去學哪個專業我肯定知道我要學數學後面在物理和計算機裡面想了一下後來還是就是選物理就是某種程度上當時對量子比較有興趣然後當時上了很多量子物理的一些課然後同时就是我做就是数学概率那边的一些研究比如说ProfessorScottSheffield他的随机曲面的那些几何概率的这一些研究有很多东西他动不动就说这个东西在物理里面有一个意义这个东西在物理里面有一个意义然后我听他讲的比较多了我就想我也想学一下物理来了解一下这个到底在物理里面有什么意义我初高中我就是我小时候物理特别差所以这是一个大胆的决定哦ok你大学又拿了很多的这种荣誉这个是怎么做到的就是你面对你你你觉得你自己是里面最蠢的然后最笨的一个然后你也不是很想竞争但是你还是从结果来来说对他但他不是竞赛的那有点像是这种呃我大学的这些荣誉像是就是可能一个教授他提名你然后你自己也不用他不是说你要去一个考试去去去坐在那里多少分钟他就是你可能你做你自己的事情然后学校可能会希望提名你去一些去拿一些奖项所以就是学校为什么比较欣赏你或者professor为什么比较欣赏你我觉得可能就是是一个比较高产的本科生哦对然后我觉得他们也很有鼓励性的意味对可能说看我可能平常就是呃学数学学的比较比较辛苦比较累就是特别怕我就是就是可能说就是不不走数学了可能也有一些鼓励性的一些意味真的吗哦我觉得是的我觉得就是这个数学环境尤其我感受到MIT的数学环境教授们都是非常nice非常友善的人然后他们都非常希望每一个人好给每一个人最好的建议最好的推荐就是没有说你们这些MIT的数学的同学们是去竞争有限的名额的就是其实某种程度上每一个人有自己喜欢的数学你们喜欢的数学和别人喜欢的数学不太一样你们就是如果你喜欢这个领域的我就介绍你去这个教授这个世界非常大就他变成了一个无限的游戏了在大学期间还没有那么的竞赛和竞争了然后我的教授们他们是非常非常好的人就是我印象中当时有说当时就是疫情就是中美之间也就是停飞了就是没有航班啊后来就是赶紧就是有航班的时候就想飞然后那个时候要写一些信啊给这个就是就是说这个人可以回来我们的教授都是非常好的他们对每一个他们的这个呃mentee他们的这个辅导的同学都都非常的好非常的照顾嗯比如说这个北美数学本科生最高荣誉摩根奖是怎么拿到的摩根奖我觉得就是有我的教授他去提名我然后有另外的一些教授包括ProfessorCanono他们有写推荐信对然后接下来其实就是评审委员会的评审委员会的这个这个决定了30年摩根奖的历史每年说虽然有一个人拿到然后有大概两三个人是就是亚军和季军这些押捐和寄捐和拿到的这个人的数学水平没有什么差别然后可能还有很多没有被recognize到的同学他们都非常的好就是在我们的当时的那一个圈子里面我并不觉得我是数学最好的那一个人就我觉得某种程度上呃就是但有那么一波大家觉得就是可能研究还做的不错的本科同学其实谁拿到谁拿不到就是这这个这个事情的随机性是很大的对理解了你在本科期间在数学上有哪些新的探索你感觉你喜欢什么对我当然喜欢还是喜欢数论然后当时可能有就是一个抉择就是哪哪哪一个哪种味道的数论是做更代数数论还是做更解析数论这个中间有一些想就是决定我印象中当时还是做了很多的就是模型师对然后做了一些椭圆曲线这一些的工作是在ProfessorOno的这个我多于一半的文章其实ProfessorOno然后和在他的就是这个夏令营的里面的合作者我们一块去写的对然后硕士去了牛津?

硕士去了牛津为什么学了神经科学没有继续研究数学的路神枣? 但是也动不动往数学系跑就是数学系也离我们那个学院也比较不太远对就走十分钟然后呃神经科学那边是我其实当时出了一件事情就我可能非常想知道就是人脑是怎么样的一个一个构造就是当时家里有一些事情就是我可能想对呃我当时爷爷有一些对我当时想对大脑有一些有有更深的理解对然后呃到了那里发现你如果要对人脑有深的理解你需要做实验呃我之前做过果蝇的实验果蝇的实验是非常简单的你就是把它这个头盖骨一翘然后你就拿一个管子进去然后你就看它的这个neurodynamic就是果蝇这是一只一只小果蝇但是到牛津的时候你要考一个就是license一个证你才能去做很多的动物实验去考这个证的时候需要你去杀一只老鼠我当时就是那我我我我我做完了那一次实验之后我当时就是我要走计算神经科系不要去做动物实验在英国就是其实计算神经科学和AI他们的这个关系非常的紧密在有一个UCL的GatsbyInstitute里面他是原来的DeepMind的DemisHassabis在那里做了他的PostDoc博后的工作然后在这个之前JeffreyHinton其实是AI教父吧他是founded了这个GatsbyInstitute这个GatsbyInstitute他叫做Gatsby中心他叫做计算神经科学中心computationalneuroscience但它实际上其实就是大部分都是AI的faculty然后我跟就是AndrewSachs教授然后包括AndrewSachs他的一个collaborator其实就在Stanford叫SheriganGulley我们当时有做一些研究然后还有TimBehrens然后WillDorrellJamesWhittington就是有很多非常杰出的又懂数学又懂AI又懂一些神经科学的研究者然后我当时是一个硕士的一个一个一个同学当时我反正我记得我见到他们中的任何一个人我当时就觉得非常的激动我就觉得我我感觉这个人好像能带我做做研究然后觉得这是个非常好的机会所以你是被AI点燃你不是被神经科学点燃了最后我最后是就我的我的那个快乐来自于来自于AI不来自于神经科学然后还当时还就是要写那个硕士论文嗯就是这一些我刚才讲的这些研究员们他们要一起来协助我把它写成一个更神经科学的一个毕业论文因为就是全是AI后来怎么写的写了个啥就是有其实有找到说比如有一篇其实就是continuelearning的一篇去去去去看这个neurodynamics然后另外的一篇是就是去看一个假设一个onelayerlineartransformer这个理论理论机器学习能做的事情非常有限在这样的情况下你也找不出你也没有办法做exactneurodynamic你就可以去但当时我印象中非常大量的先进代数非常大量的矩阵运算就是在出現在前面那一篇大量的這種就是ODE對其實都是非常基礎的數學應用在這一些可以有AI與認知科學背景的這些項目上那你博士为什么又去读了数学和法学在Stanford? 我博士这个数学我是本来本科的时候就是defer了所以就是本来就知道自己要回去读所以我当时是本来打算可能本科之后直接去读数学博士就是没有去经过这个牛津这一层为什么牛津去了呢因为罗德教学金我觉得是一个非常好的一个机会OK我有另外一层就我从小喜欢打辩论所以我觉得在就是牛津的这个有这个OxfordUnion它有一些训练你去成为一个更好辩手的一些活动然后包括是后面到法学院去做就是Litigation诉讼相关的我不是并购那边的我是诉讼那边的就是暑假实习之类的其实都是由于这个辩论的这个很早的时候开始辩论的热情嗯所以其实整个的发展非常的综合那你这么说对吗可能但我差的也是实在是差就是综合一般意味着是没有短板就是我还是有很多很多短板你差的是什么短板是什么我很很多事情我都我就是做的不太好比如说我我印象中当时地理是非常糟糕我到现在啊没有任何的方向感我就是我我我觉得我是一个比较spiky又就是不太好的就是不太会的东西也非常spiky的一个人我是一个highvariant的一个人哦那经过了数学物理神经科学AI包括法学这多重学科你站在这个交叉路口你看到了什么呢就在你可能在站在博士的那个时候对呃当时看到了就是几件事情第一件事情就是我當時對憲法非常感興趣然後我當時就是憲法裡面它分幾種憲法去詮釋美國憲法的這個方式比如說originalism原典主義就是說所有憲法現在我們看到的是基於國父們就是建國的那一些人他們的原址原意來應該這樣詮釋憲法這是第一種然後第二種就是叫做textualism就是說憲法寫的這個英語字是什麼你就把它讀成什麼你不要去想他們原來可能想的是什麼你就是去一字一句的去解讀去看到一個定義特別像一個數學家可能會去做的一個詮釋第三個叫LivingConstitutionalism或者叫PolicyConsideration就是說這個憲法它會呼吸它會與時代一起成長原來的憲法是這樣寫的我們應該把它看到21世紀去怎麼樣去解讀它就是然後在我在法學院就當時對這些東西非常感興趣我是一個非常我是一個textualist就是我是一個按照它是什麼樣就是什麼樣的這樣是我的我的司法哲學judicialphilosophy然後當時他們就有人說如果你想去了解這個到底是什麼意思因為我們不知道這些詞是什麼意思可以去拿一個就是lm去给他一些data让他这些data可以包括什么在里面也值得商榷可以包括这些建国文献也可以就是包括现在的一些新的当代的一些政治与哲学的一些著作然后我当时就有一个想法就是如果我们已经到了一个能拿AI去看这个宪法是什么意思的这样的一个时代了我为什么不能拿AI做数学嗯我当时就在课上我在想这件事情我就觉得应该应该可以做数学然后我就想到一件事情就我最好的一个朋友之一就是呃他叫KennyLaw他是呃帝国理工啊imperialcollege他交换到MIT我们大一就认识然后我们一块上了很多的课我们是非常好的朋友然后他还教会我怎么下这个象棋他是这个象棋的这个大师然后他就是告訴我從20年開始告訴我他在做Ling他在做形式化證明他是最開始Ling裡面什麼都沒有的就是Mathlib是一個空空如也的一個Library他把它裡面所有的本科的代數本科的分析去把它一行行的把它打出來做基礎的這個建設的那五到七個學生之一是KevinBowser的學生所以当时我就在想一件事情就是说AI如果能去做法律是去看比较structure的东西就是这个东西到底是什么意思研究的是比较specification这一块而不是比如说让你去拿AI去判一个这个人到底有没有杀了另外一个人一个普通的trialcourt一个case而是去看这个constitutionallaw比较就是preciselydefine比较严谨的去去定义的这个那我需要数学不是英语而是一个更结构性的一种一种呈现而这个令这个形式化语言它就把数学变成了一个代码所以他就可能能够去我当然就有一些这样的一个想法然后当时同时和叔伯我们在这个一个叫做Verve的一个咖啡店我们一开始认识的然后接下来我记得在PaloAlto对就是Verve咖啡现在墙上还有我们两个当时就是照了一张拍立得相片他当时说你买了一共买了10杯咖啡你就可以照一张拍立得我和叔伯在那一定买过10杯咖啡对我们给这个咖啡店就是带来了非常多的这个营收我们现在整个办公室的每一个人他们每一天都在这个咖啡店然后然后我们当时也一直在聊这件事情就是陶喆轩老师有很多的不管是播客还是就是写的博客就讲这个刑事化证明然后我身边的就是Kenny他我知道他有多对这个令进行狂热他现在也在XM前职所以就是好多好朋友们大家现在就是慢慢的聚到了一起就是希望能做能做这件事情我当时看到的一个事情就是一切我们认为的不可能都有可能然后如果是这样的话对我个人意义最大的就是让AI能够帮助我进行一些数学证明尤其我不是天赋型选手我有些时候真的是花某种程度上你说AI能够帮助最大的是谁是那些蛮类型数学家就我可能真的就是我要每舉多少個可能性我要經歷多少天去驗證一個非常可能是一個標準的證明方式我按照那個比對我記得當時就有一個事情就是BenGrimm老師有一篇文章叫SarkozysTheoremforShiftedPrimes他講的就是說我有一个集合我要保证这个里面的集合的A和B两个元素中间的这个差值就是A减B它不是P加1或P减1P是一个素数然后我能够就是从1到N中数出多少个这样的一个多大的一个集合然后我当时就我看到那篇文章我想这个东西能够被证明多少的数学问题就同样的这一套就是老师的这一套这一套发明或者是发现你可以把它去做你可以把它去做当然说做shiftedsumoftwosquares没有特别大的意义可以做X方加Y方加减一这个没有特别大的不知道有没有特别大的意义反正就是这一套的东西是工具是可以用来做很多的事情的AI应该把它完全解决AI应该能够达到一个一个很熟练运用所有Davenport里面数论的工具技巧的一个博士生的程度我当时觉得这一件事这个事情一定能做然后我就开始想怎么能做这件事情就要算力就要我要想我有多少的这是哪一年2024,2024年,就是你跟shubo频繁的进入咖啡,出入咖啡馆那一年,对对对,204年,ok,2043年9月份到205年的12月份,去年12月份,啊不204年的12月份,ok,对差不多因为我当时还在我第一年其实我大部分的时间就是呃我在作为一个法学生的时候Ihadalotoffun就是我我每一天就是感觉特别的特别的神奇我我从来没有任何的呃就是作业是让我去阅读的阅读这30页这就是你的作业我我的我的本科是一个工程学校一个MIT是一个理工科学校我不是一个文理我没有接受过一个liberalarts的education哦嗯所以我就非常非常希望能够多读点书然后我可以我还想练练英文写作我当时觉得我都可以去所以我那一年就是但是就是第一次吧可能科学数学它不在你的生活之中就有点想念然后就是我想念的时候我就跑到那个咖啡馆去我坐那个校巴当时没有钱当时是是特别就是一穷二白打不起uber然后从这个这个这个斯坦福就是坐八分钟的一个你要走二十分钟你走二十分钟到这个大草坪你到了大草坪就可以坐一个就是校巴坐校巴八到九分钟你就到了这个火车站这火车站穿越一个隧道里面有一些流浪汉住在这个隧道里面你就可以到这一个Verve的咖啡馆舒佛就在那里你就可以去跟他聊这个科技与科学哦他那当时已经在Meta上班了他一直都在他是在Meta是89年的一个Meta的一个元老他是Meta的FacebookAIResearch的Director就是他当时跟他当时跟田园东老师差不多时候进去的就是可能还比田园东老师早一些那你们怎么成为朋友的呀我也不知道他是谁他也不知道我是谁那你们怎么认识的呢我们就在这个咖啡馆的这个桌子就是我一开始到那写作业我一开始到那就是我有30页的阅读每堂课有30页的阅读我就抱着这个这么大的这个法律书我就抱着这三三个法律书我就我就我就去去其实其实挺就是非常不不不不明智的一个选择你有那么厚的书你抱着他们去做小把但当时就是喜欢那你为什么一定要去那里去做作业在PaloAltodowntown啊就是我可能我们这个法学院的图书馆就是一般周一到周五呆的有点闷我说实话就是他有地毯然后有点密不透风环境你周末你就是想放松一下心情对然后我记得这个Verve咖啡馆的一个点他那个庭院有很多狗对然后他只有周末有狗就是他周周中的时候那些狗的主人可能没有时间带他们遛狗我我当时一开始去那里的motivation就我可以读书我可以喝这个我会点一杯抹茶然后我就可以看狗这是我的一个我的我的快乐就是就是读读法律案例呃做笔记看狗喝抹茶然后然后就是时间一多就总是我和发现我然后然后就有这么一个呃每一次看的感觉非常面熟的一个人然后我们一开始聊起来了哦是在里面还是外面因为他有一个区域外面一个区域在里面啊对你们可能共同坐在一个长桌上对一个一个六个人的桌子对然后唯一的一个六人桌这个六个人桌子里面其他人也永远都在那里哦对哦成了一个常客对谁开始先聊天的应该是一个就是没人打算聊天好像是他坐在窗边然后那个太阳特别晒然后我需要那个窗帘拉起来这么说上话哦然后呢然后接着就反正我就说我就我就我就like非常谢谢你就是拉这个窗帘然后他就说我经常看到你然后我就说是我也经常看到你然后一个谈话就开始了嗯然后那怎么聊的数学的呢发现他有他学过数学他的本科是数学他的硕士也是数学然后他后面他好像还读了两个数学的硕士我印象记得不是特别清反正就是然后我的那个呃就是他就很好奇我就是他觉得我应该是个法律学生因为我有这个书然后我们就聊这个我当时可能我不知道我在看哪一块呢我反正就讲这个这个案例是非常的离奇然后就反正两个人就开始做朋友吧就是我觉得还是感觉这个21世纪就是有很多事情都是在互联网上大家不太到一个咖啡店咖啡馆去聊天嗯你带我们多久我们聊了就是我们一两年我们是朋友我们不知道对方在哪但他不知道你是Stanford的学生他知道我是Stanford的学生但他不知道他可能知道我是法学院数学但他不知道我他可能不知道我有一个数学研究背景就是他可能他好像听说过摩根奖他听说摩根奖可能是因为有很多摩根奖的同学转入了AI比如说LevonAlpert在AnthropicGregYang在XAI的CoFounder就是摩根奖是AI的一件事然后他不知道我也不是个什么人物他不知道也没关系但是我我是真不知道他是一个这么厉害的一个一个AI你知道他在埋他吗他现在就是你知道他在埋他吗我当时不知道我一直不知道他在埋他后来你们是怎么开始决定要创业的呢就是在你们这种漫无目的的认识漫无目的的认识和聊天对对我有我有一天你们这种谈话持续了多久持续了一年半聊什么呢这一年半聊科学历史哦然后就有一天我印象是秋天204年的秋天那个时候我刚开始那个数学的PhD但我当时很多的时间其实在给XTX去做一些工作就是XTX是一个一个一个量化金融的一个我暑假就是后半段在那里然后我我当时就觉得我在那里就是觉得天呐这个AI更更有意思就是你XTX有卡呀对吧它他有卡所以你能做的事情就比你在蓋茨比做的事情多很多所以就當時覺得AI很有意思然後回來然後就我有一天我就跟我是去跑步我就是晨跑然後跑完之後我不知道為什麼我就覺得好像这个事情真的要真的要发生然后我就去找叔伯我说这个事情大概如果我想融资要融多少钱呢然后我们两个人在那算我们算就是多少张卡然后也待会就在位就拿了张那个餐巾纸在那算然后我们就说好像这个事情还是得做一个创业公司就是没有可能在学界去做那我那一个学期在做XDS我疯狂的往CS的那里跑有一个CS斯坦福CS我觉得最好的一门课是一个叫做就是firstyearPhDseminar每一个教授为了就是招新的学生他们就会去讲他的这个researchhighlight你每每一周去就一个学分你每周每周三下午去下午五点然后你可以认识你所有其他的一些计算机系的同学们我就坐在后排厅我是个数学系的然后然后完了之后你就可以知道我的天哪就是有这么多就是做机器人的他们在做什么做这个computervision的在做什么你就反正就是非常itsanintellectualfeast你是在哪一刻决定辍学要创业的呃其实我大概知道就我开始融资的时候我就知道我总有一天要辍学就是就是先开始融资才辍学的啊你是先开始融资再辍学我先开始融资再辍学因为这个我不能辍学因为我辍学了我没有身份我要拿到我的这个身份工作签证我才能够辍学哦所以我拿到我的工作签证我就辍学了哦因为就是一般来说投资人也期待你辍学就是你很难说是同事你的就是硅谷这个一般拿到融资就是开始要呃甚至有些时候辍学是融资的closingconditionok为什么不是叔伯当CEO是你当CEO叔伯当时其实还在一开始大部分的时间他还在Meta嗯他没有他到后面刻决定加入你的OK因为我们当时谁都不知道这个事情能否得到这个投资人的支持嗯这个事情是想不想不明白嗯所以从哪个月份决定的我从9月份就决定了但我不到1月我没有融资因为我一直在劝自己不要做这件事情为什么我不太喜欢就是我当然我觉得中国语境下的创业者是一种就是气质但美国语境下现在就整个valley都是founder就是创业者某种程度上辍学创业他就是浮躁我其实觉得如果我是一个本科生我绝对不会去辍学然后去ycombinator就我某种程度上我觉得我是最不可能创业的一个创业者我非常的喜欢向往学界我非常的希望能够去做更多的数学的一些探索我非常喜欢在大学的一个环境所以我就两个月是在劝退自己然后但是每天早上还在跑步然后跑步的时候想事情想得非常清楚到后面确定是非常非常确定然后到我非常非常确定的时候马上就感恩节了从感恩节到圣诞节的时候没有VC上班所以你要么就是那个时候到感恩节融完只有10天要么你就来年再融所以我当时就来年再融哦那两个月最后你是怎么经过了怎么样的COT然后决定一定要做我当时去读了这个科学史哦读了科学史读了科学史真的读了科学史全创业读科学史就是多少个先是从维基百科开始读科学史后面要找书读科学史然后有一个叫AIforMath的一个GitHubREPL这个GitHubREPL里面大概有几百篇文章每一篇文章的after我都读过然后有意思的after我就会把整篇文章看完然后我就做了多少次费办的过程在就是纸上去想如果说我这个东西要搭起来应该技术上怎么做我不可能说我自己觉得这个事情不会成功然后去骗别人的钱这个事情我觉得做不到所以我当时就到了一个程度我发现我觉得它不一定是一个研究问题它是一个工程问题它这个东西的科技的风险就没有我一开始看上去的那么高然后在这样的一个情况下我觉得是负责任的去做去做这个这个这个创业开始融资嗯所以你是在自我验证这个过程是在对我我觉得就是某种程度上你如果去呃就吸引一些风险投资你需要自己一定要对这件事情比较确定比较了解不然我觉得不太负责任但你质疑自己的点可能是说会不会我嗯这是一种浮躁这是一种跟风一个是是不是浮躁跟风这个我倒知道我我特别我特别反对做一个AIfounder所以我知道我绝对不是浮躁跟风反对做一个AIfounder是为什么就是我我从因为我在MIT然后在MIT就是有创业社然后我的好朋友们一起去打那个janestreet的那个啊就是量化金融比赛黑客黑客hackathon的这些同学们他们是创业社的社长我当时就两个队友他们两个就是这个创业社的社长叫我去活动说有这个freesushi免费的寿司我也不去我觉得我觉得创业不好它不是一件好事情我觉得还是要做教授这个有点无正业是不是呃对然后我觉得就是我总觉得比如说一个以非常产品为导向的这样的一个创业项目感觉像是昙花一现我当时也有这样的一个感受然后我希望做的事情是非常长时间的非常难的所以我觉得一般和一个创业的一个这种风险投资的一个周期可能不一定吻合所以我我知道我不是福岛跟风的那一批然后嗯我当时还有在在想就是我有没有什么别的办法能够做这个AIfor数学然后我当时还尝试去我要不加入一下别的做AIfor数学的公司然后就在这个Verve的咖啡馆这个我们现在的主要的竞争者这个公司的CEOTudor他也是常客你说我有一天还就见到了Tudor然后我就说你们你们你们招人吗然后我当时真的是想就是我是想做这件事情要是我能跟别人一块做我也不用自己去从0到1就感觉太复杂了就是然后这是主要的质疑点其实不是一个感性的我是不是浮躁我是不是跟风就是我到底会不会这个东西然后我就我就去研究这个AIformat真的当时就是看paper然后这个过程也非常的快乐就是非常非常的快乐非常快速的去学习一些主要的一些idea从比如说2018年一篇文章叫ATPBoost在没有AI的情况下去去做这个形式化的这个定理证明然后我看到Bartos一个波兰人是这个作者我们现在Bartos也就在Action然后我当时有另外的一篇文章叫PatternBoost就是是从很多的数据中去找里面的这个pattern找这个规律的一个去从很多的图中去构造新的图去为数学家去找例子和反例的pattern不锁当然看FrancoisCharton是这个作者现在FrancoisCharton也在action然后我当时看另外一篇AIforMath的文章叫IntoInt然后这个是拿这个一种translative的翻译的一种方法从问题能够翻译到解法问题能够翻译到解法如果看到了很多这样的例子下一次来到一个问题的时候是否能够直接翻译成解法也是做数学发现而不是数学证明这一个文献里面的AlbertoAlvarino他现在也在action就是所有这个美丽的过程就是我所有这当时我作为一个学徒去看这些巨人的肩膀这些这些文章他们现在都聚起来了都在action这是一个非常非常我觉得神奇做创业者我觉得其实这是最最高兴的一个过程你有形成你那个小团体对对对对对你去问那个竞争对手能不能加入你们公司有没有机会他怎么说他说你是你是你是什么的phd我说我是数学的phd他说哦我们只招计算机的phd哦为什么aformath对为什么呢我不知道他当时就是这么说的哦但是你们团队很多是math我们团队呃这么说去我们团队有三块我们团队有非常多AI的人就是强化学习agents就是appliedAI的这一些人我们有很多的做代码生成的人就是programminglanguage然后呃很多是compiler编译器的人比如说lmcompiler那个主要团队在我们这然后他们很多其他的工作compilerarena就是所有的这一些呃compiler就是深度学习去帮助compiler就是代码生成的这样的一群人然后他们当时也是呃杨乐坤那个codeworldmodel32个billion的那个模型的后面的里面的一部分团队然后都在我们这儿,然后有一群是数学,这数学里面比较tricky,数学里面有纯数学家,像KenOno,小野肯教授,像EvanChen,我说的这个IMO的这一个教练,然后也有做Ling的,做Ling这个语言的里面,其实就像Python里有PyTorch,它是一个图书馆和Python它是下面的真正的那个编程Ling里面也有Mathlib是一个数学图书馆和Ling这个作为一个编程语言两两拨人所以我们也都有我们又有这个做Mathlib像KennyLaw还有他的朋友巨健张张巨健就这样的一些非常好的好的同学们然后我们又有就是做metaprogrammingmetaprogramming叫原编程就是去把另当做一个编程语言来使用去创造出里面另更多的工具更多的抽象呃层这样的就是相当于你可以拿python去写一个autograph的一个一个一个著名的一个一个一个一个一个coding的这个这个呃编程的一个面试题啊你可以拿python写一个autogram我们来了一个同学他他他拿链写了一个autogram对所以就是在这里面也有很多块所以并不全是数学的人我们很多的就是招ml的同学他们很多背景我们我们队伍里面就是当然说算上实习生4个m5个mo所以说五个IMO然后就是他们会有很多数学的prior就是context就是他们理解这个数学过程是怎么样的但我们要求非常强的again这是一个工程问题尤其24年9月嗨你刚刚萌生想法但是在努力劝退自己1月决定要创业了然后要等那个是这个圣诞假才能融资啊等了圣诞圣诞假圣诞假你干什么了吗圣诞假干干了很多事啊和叔伯一起在读文章哦为什么是你们两个一起那你这个他已经说我要我要我要加入了吗他当时没有他当时就是在mela就是他当时呃他圣诞假闲着也是闲着我们两个人就是找一下像是一个readinggroup因为当时他当时在旅游他圣诞假感恩节他都在就是在不在一个地方我们在zoom哦哦你们还定期要开会我们我们发现我们就是讨论我们阅读的心得我们发现我们能够是很好的连创团队的时刻是我们发现我们两个都非常讨厌zoom我我没有办法跟人开zoom的会超过一个小时他没有办法跟人开zoom的会超过45分钟我们zoom了四四五个小时每次的这是我们发现一件事情因为我们思考的方式特别的又相似又互补所以我们就非常享受每一次我们的一些技术的探索他现在是他是一个他当然你看他20年的GPU经历10年的AI经历他是当时CUDA第一批就是开发者然后当时20156年201456年和温达他们这个百度这个硅谷AI研究室他加入百度他当时是20156这是他进入AI的他的第一步的AI哦,哇!

這些人後面是做了多少就是重要的工作多少個早期的OpenAI多少個比如說Dario就直接是Anthropic的這個founder然後非常好的一個一個他們當時就是ScalingWorks我们就是做这个deepspeechdeepvoice就是把大量的这些speechvoice的data去扔进去scalingworks他们当时办公室有一个就是一个一个一个理念叫我们绝对不招一个语言学家他们当时是做的deepspeech和deepvoice他们需要语言学家吧按道理他们不招一个语言学家有一点像我们当时我们现在公司的这个做编译器的这个团队他们当时167年拿就是机器学习要去革命这个compilercodegeneration代码生成他们就说当时就很多就是编译器的这些专家说你不可能做到的他們就說我們不需要你們我們照樣能做到就拿AI進入一個領域去革命這個領域某種程度上是我們這整一個現在30個人了但當時就是早期這個創始團隊的一個DNA我們希望我希望能夠拿AI去給數學去做一些革命性的一些改變你看他們說他們不招一個語言學家要用AI去革命语言学的命对那你们是不是也不应该招一个数学家我们以为是这样的我们我们以为是这样的我们当时定了一个事情就我们不招第15个人的时候不要招了一个数学家为什么是15个就随便说了一个数我们当时觉得我们钱也不是我们的种子论大家可能看起来数量很多对于我们要做的事情来说大家的普遍的想法是我们underraise了我们是raise的不够我们的种子论啊所以我们当时觉得人的这个人头是限制的到20个人我们可能就没有办法再招人了所以当时觉得那只能说那就那就以每15比1这样的一个数学家的一个比例去走但是他那句话的逻辑是我不需要语言学家语言学家背景可能对于这个团队是负分我们现在的想法就是我们招数学家需要他非常的思想开放呃早期的时候其实有一个叫做frontiermath的一个benchmark与这个benchmark相关的一些同学当时有希望就是我们有互相都希望能够一起合作让他们加入action但当时就发现一件事情就是一些数学家背景的同学他对scaling这件事情他有一定的呃的一定的犹豫他对或者说不是犹豫他就不愿意他不他不喜欢scaling这个这种这种哲学他觉得说我数学是一个工艺我是个手艺像日本师傅捏寿司你怎么能就是给我一个当时我们说我们要做internetscaledataset有同学就是接了我们的offer之后就是不来了就说我不要我不要做internetscaledataset我们觉得又是要scaling又是要更好的sampleefficiency就是当然说sampleefficiency这个效率是一个非常呃样本效率是一个非常也是一个非常满的非常非常多意思的一个词了但是我就拿Percy梁教授的这个话就是他是做惩罚嗯我们觉得来的数学家我們現在希望他是跟我們對著幹就是是他們做adversarial的就是就是與我們與我們相對抗的去做啊benchmark基準級的的的的的創造就我希望你能夠感觉我们的系统哪弱然后去就是当然是越做越来越难的这一些这些这些基准级所以某种程度上呃就是can就是呃小野肯他加入之后呃我们的这个基准级的这个集结是我们的第一第一号任务嗯我们继续把那个时间线来捋一下好好呃我们刚刚说走了就是呃当时已经说到了圣诞假期然后你们有一个readinggroup对音乐开始融资ok你们读了多少文章那个阶段读了好多包而且当时我记得圣诞节我们有一个叫圣诞大礼包杨凯玉老师他们写的一篇文章他们一篇文章叫做形式化形式化定理證明AI的下一個前沿是一個研究論文研究論文就是它不是一個研究論文它是一篇介紹其他所有研究論文的研究論文它就是把這裡面領域的捋了一遍然後我當時我記得我那篇文章還我記得他第五部分是有這個目標就是說我應該一個好的AI數學家能夠做到什麼樣的事情在這幾個象限上他能夠有什麼樣的能力我們就把它做成我們自己的表格这个之前就是从从第一行到最后一行我们我记得我当时就是就是每一个提到的就是直接和间接提到的这个文章不管是引用里的还是就是只是提到的一种逻辑我就是比我已经有的阅读笔记我想我还有哪些没读到的然后还真有一半没读到的所以那个AIforMaths那个Github整理的也不是很全然后就是所有的这一些当时就感觉就是我原来知道的像是12345个很好的做法现在这篇文章给我连成了一个面了就是他他让我理解这个这个bigpicture了我就是更更我觉得我的理解反应是当时有很很显著的深刻所以这个谢谢谢谢杨凯玉老师这篇文章对对对嗯然后到这个假期结束叔伯决定加入你吗他还没决定加入我们他到了就是后面再决定加入了我开始觉得跟你一起讨论很有乐趣对他当时因为他是一个元老他是一个AI的一个元老我们我当时都没有敢问他要不要加入我们就是我我我想着就是我那他为什么开始你们怎么开始这个閱讀的呢? 就是矽谷這個文化就是很多就是AI的這個元老他可以做你的天使投資人或者他可以去做你的advisor就是他會他會事情特別流通就是矽谷是一個非常有魅力的一個地方就是學界工業界老師同學就是年長的研究者經歷豐富的研究者和就是剛進入這個工業界的研究者呃他们就是汇集非常的流通非常的就是非常非常多的互动就是大家是谁不重要做什么事比较重要比如说比如说叔狗他另外的跟他呃他指导过的创业公司也有很多比如说皮卡对吧这个呃对呃文景就Demi他他们也是其实呃Demi他是当时进进入这个就是Facebook的时候叔狗还是密室哦面试官ok所以他也跟MistralMistral那整个foundingteam本来在拉玛就是是叔伯他们同一个org下面另外的隔壁的那一个team就是大家都包括其实Mistral这个队和我们队伍的这个Francois另外一个其实我和叔伯说加入之后第三个加入的这一个这一个人关系也也也很密切就是他们也是很多年的朋友然后你跟叔伯这种twitter的关系吗没有tutor就是两个人有不同的背景看这个事情的角度不一样所以我们就聊了很多比较哲学性的一些研究的一些想法我们当时就是觉得自己读的足够多的时候就想就是有哪些可以做新的事情然后就是做新的事情的话又其实可能连接到哪一个古老的AI的其他的领域的一个做法比如我们当时看到的一些我们想做的事情就在JamesDoe的那个AIforScience那里他们有做比如說JamesZhou這個實驗室一直有做其實可以對AI和數學很相關的東西然後包括比如說我們當時想做怎麼樣去做一個conjecture怎麼樣去做好的猜想當時斯坦福的這個計算機系就有同學在以希望能夠造一個AI科學家這一個願景去做怎麼樣去能夠去提出好的機器學習的猜想就所有的這些東西它混在一起比如說我們現在做的一些事情跟當時早期做棋的這個expertsystem專家系統這些都有關係所以就非常有意思就是所有的这些东西没有人去尝试把它聚焦起来在一个工业界盈利性的公司也就有更多的充足的资金和算力的情况下去把这一些从20年开始有一个爆发一个想法的爆发去把它验证下来就没有人去做这件事情我觉得非常可惜那這是有結構性原因的就是2016年的時候ChristianZagidi還有這個吳予懷他們在Google開始做比如說Holist這一些Hol是一個就是定理正名語言2016年很就是早期ChristianZagidi大概在2018、9年一直在改動的修改自己寫的一個他寫的一個白皮書就是這個未來就非常長的一個白皮書然後在20222020年我想说2019年OpenAI伊利亚带着人做了这些事情伊利亚带了他们去做这个GPTFminiF2F当时OpenAI还有跟JesseMichaelHahn然后StanPellew这一些后面都成为了其他的好的公司的创业者当时他们有做在OpenISO这件事情201年有这个一个实习生开始一个人去在GoogleDeepMind做这个AlphaGeometry他们发现哇这个做的是真好所有的资源进来scaleup做成AlphaProof然后做了你看201到204这是三年的一个耕运204一炮而红的这个AlphaProof拿了28分差一分金牌的银牌这个对我来说是一个是IMO被解决的那一个时刻它就是那两道组合体解决不出来205年反正也是就一道组合体大家都没解决出来204年的这个deepmind真的是kudostothem这是一个跨世纪的一个时刻就是AI在数学奥赛上达到了达到了好的胜利这是204年我们在205年12月做的这个普特南的这个满分是这一个他们开启的这一个序章的一个一个尾声而已然后我们其实马上希望做的就是研究数学所以呃就是这是这个整个AF数学的这个发展发展的这个历史舒伯作为你的第一个员工对是什么时候决定的连创吧对连创他是呃二月份吧二月份你融资融好了吗那个我当时有了不错的就是这事能做起来只要想做就是已经有了不是不是最终的价格但是不错的价格嗯就是你出去融资验证了一下这个对其实很快就是一月份嗯一月七号好像因为因为一月头是这个JMM就是数学家大会我当时到这个我记得是應該是西雅圖那一年205年居然美國數學學會說我們今天的主題是AIfor數學這個就是由於數學是一個相對比較保守的一個一個一個學科比較這是這是一個非常讓人就是雀躍的事情所以很多人都去了還有一些計算機學家我當時和deepmind的AdamWagner就聊了很多我們發現我們都是曾经在某一个英国的学院上过学还挺有意思的然后这个AlbertJiang也是在这个学院上过学的挺有意思的所以我回来了回来之后好像就是第三天就开始有offer了然后就开始不停的微信门开始去竞拍哦去竞拍对怎么竞拍的或者就是比如说你给了我一个offer然后过一周里有另外一个人给了我一个offer然后他们会尝试去把上一家的这个价格就是超过他哦所以最后从一开始的那一个offer到最后的offer翻了三倍的估值翻了三倍对你是怎么去pitch这些VC的这对你来说难吗啊就是一个非常融资的融资之门怎么打开的因为你是第一次没有人喜欢融资没有人喜欢融资如果说有一天有一个公司能把当然我觉得这个很难因为毕竟这不是一个技能的问题就如果有一个很好的AI融资员我希望能够让他去融资你要付他多少薪水我可以给他百分比这个真的我可以给我觉得融资是很难的一个过程他不是说难结果难他就是累嗯呃你是一个复读机一次一次的说一样的事情你一次一次的接到一样的问题真的我就能我我可以可以把它录下来然后我就给你们大家发对吧你们反正问题也是一样的这个但是呢就是从这一些大量的比较无聊的这个过程中有一些让人很激动的谈话通常这一些谈话是你最终选择的选择的投资人比如我印象特别深刻的我们最后的领头方BCapital我跟HowardMorgan就是有一个对话我当时在赶这个rebuttaldeadline就是有一篇就是文章的这个deadline然后我当时跟他在zoom上对话然后就是我发现Howard简直就是一个他比你更乐观他比你更觉得你的商业模式有前景他告诉你这些是你的商业模式他是文艺复兴的cofounder和JimSimons一起然后他也是另外一个硅谷老牌的一个VC叫firstround的联合创始人所以他既是他是一个数学家他住在住在纽约他现在有时候还去纽约大学上上课然后然后当时我就觉得HowardMorgan是一个非常让我感到就是很跟他聊天我很激动我当时在MIT的时候JimSimons先生还在的时候有来我们MIT网上有一个两小时的一个围录谈话我当时是本科的那个数学社就是我们那个活动我就跟他去去聊然后所以今天见到不是今天就那一天见到Howard然后他还在那个硅谷的那个TVshow里面就是出现过对然后然后他就给我介绍了另外一个一个人然后这个人其实是这个呃表哥表哥或者表表兄弟反正反正还挺有意思他们俩长得还一模一样就是有一些有意思的谈话你可以见到很多不同视角的人然后你可以我其实觉得我不是一个特别厉害的呃fundraiser就我不是我一般就是这个事情是什么我就讲然后我一般还把很多就是风险啊什么的我全讲出来然后是什么你讲的风险我当时种子论我就说这个我们商业模式并不是非常的确定的这个我自己做过这个量化交易员我不知道我们这个东西是不是量化交易我觉得可能不是吧对我听说这个还还是有差别的跟量化还效果到现在不如量化好的对对对我当时就说我我虽然我自己在量化中做了一些数学我觉得你就是作为一个商业模式来说它一定不是一个一个最终的商业模式我拿这个的举一个例子是说一个数学比较好的一个AI大部分大概率上是有用的就这是一个例子这不是我们要具体要想的第一个市场我们具体要想的第一个市场我也不知道是什么我们现在是一个种子轮目前的还是希望把这个东西科技给给做出来当时反正是这样的一个就我讲的都特别保守然后我后来才知道投资人们一般来说他们见到的创业者们讲的比较毕竟是一个pitch嘛他讲的都是比较乐观的然后所以他有一个打折他比如说你可能讲说感觉这个东西是十分他心里就给你讲一个八分他有一个这个conversionrate我如果当时讲的是一个七分他就给我打折就可能打没了所以就我会是后面才知道的事情哦但是他们都给你sayyes对你有被拒绝吗嗯有被拒绝拒绝多还是yes多没有人想拒绝我们他们就不告就就没有没有没有人回你的消息了因为他们其实在希望做的一件事情是说呃如果有有别的人要领头你了就是他不太确定他不想拒绝他拒绝你你可能以后不理他了他就他就拖着你拖着你完了之后看哎这个人给了你哎那我也给你就是他是一个这样的一个群体groupthink的一个过程所以他们后来都跟了吗挺多的就是那一轮其实挺多挺oversubscribed的所以你核心是需要找到一个领头愿意sayyes我们当时有好几个领头方的金牌的一个offer哦几个金牌三个你是怎么让那么金牌的我没让那么金牌我其实这是几月份就是一月份到二月份到三月份嗯对差不多一个月一个一个月一个领头方因为就是价格从一倍到两倍到三倍就持续你都在聊你来了多少投资人嗯我不知道大概几十个几十个对我觉得呃这有一点就是可能说以前做数学一个职业习惯就是总觉得希望有一个很optimal的一个outcome就总觉得说希望能够把这个呃这个轮做的这个结构好一些对然后呃也不太知道怎么融资对对后面就学会了一些道理后面就后面的融资就顺利的多一月份有一个零头说我愿意嗯然后你没有听你为什么没有直接接那个offer然后还在继续聊因为他要带路掉我50%哦我不可能让他带路掉我50%啊你当时sayyessayno吗我当时说了no哦但是一月份你就确定你这个事情有戏对所以叔伯答应加入了呃是二月份的那一个更真一点的一个offer就是然后那个时候他加入的就第二个offerok但是他还不是最终的offer你还在聊我最终对我还在聊你聊到了但是我当时二月份那个我是想接了的于是我后面我就跟所有人说嗨这个这个我是想跟他们走的就是你可以加入我这一轮但我可能不会去看其他的其他的offer了哦然后到三月为什么又变了呢呃因为我觉得就是这个HowardMorgan效应这个完全就是我作为一个呃就是我我我我对文艺复兴有非常大的一个这种这种就是这种崇拜然后而且价格也确实很不错嗯就是二月你已经觉得有一个不错的offer但是你还在聊对然后你聊到了三月份是那个bcapital对他是怎么offer你的他他他的一个风格就是你每一天都会接到他的电话他他就是他他非常看好你我当时在那个做rebuttal我没有时间就这个为什么这个过程中拖了很长是因为我还在我还在上课我还在考我法学院的考试我还在那个我还在上我的数学课虽然说就是我去的也少一些但是就是我还在我有事情我当时还有X天就我当时非常的忙2月份不就应该准备辍学了吗嗯对但是我有这个offer然后当时我就开始我还没incorporate呢我去找这个律师去建立一个公司有很多很多当时什么都不知道没有人完全什么都不知道什么都不知道我没有任何的这个孵化项目我也没有我我真的什么都不知道就是到最后是说他们说我要给你写这个termsheet了我这个你这个公司我写什么我说我还没有一个公司就是哦所以下月份开始成立公司二月份其实其实一二月份你问我还在做一件什么事情我在招团队啊就是我大量的时间比如说就是在吸引一些我非常渴望能够得到的AIformath的人才嗯叔伯肯定是第一个对吧对对嗯但叔伯其实他像他是战友对然后去去在就我们两个再去找一些找一些同学们对嗯所以你是几月份出去的我是夏天辍学的夏天辍学那三月到六月在干嘛那个时候我的那个就是我的工作签证下来了所以我可以我可以辍学了哦对三月六月在干什么就是你签了一个一个termsheet之后你要做很多的这个法律的duediligence然后他才能把这个钱汇到你这里你要找这个办公室然后你又去找人当时有很多很多的AI人才在流动同时AI人才市场的这个价格非常的高我们这个创业公司无法去支付一个10个million这种这种package所以我们当时花了很多的时间与精力在希望能建一个好团队对那一轮融资是3亿美金的估值对融了多少钱融了64个million就是640万美元是比预期低的吗是比预期高的预期是50个米连是预期高的对嗯你觉得作为一个华人女性在硅谷好融资吗这个身份会给你带来任何加分减分吗我觉得我倒没觉得华人女性我觉得就首先我比较年轻这应该是一个我加分减减分减分年轻做product是加分年轻做deeptech是减分啊我没有我确实不像说是我们团队里面的除了我之外的所有人我没有一个带带带带一个tech队伍的经历嗯我没有这个trackrecord嗯这是这肯定是减分然后我觉得华人女性这个没有什么我我我没有什么这不是一个加减分对年轻是一个减分对嗯我有时候我我有时候倒是觉得说呃我有时候觉得就是呃就是年轻这个事情吧呃做做产品的话一定是加分的但是做产品性比如说consumer就比如gofacebook这种对嗯对对其实我觉得就是真正应该加减分吗年轻就是我觉得作为一个创业者来说呃你要你被要求的是长期进行重复的呃高就是非常highstake非常非常重要的决策而你的每一个决策给到你的时间是非常短的所以如果你没有一个很好的一个我是一个是一个worldmodel一个一个一个就是第一性原则的一个一个体系的话你这一些决策容易不太不太最最最最直话所以我觉得还是我还是希望说我如果再来一次我希望我能够再再再多多多几年再就我觉得太早了嗯没准备好还对我觉得就我我我刚才听一些在在哥哥19岁他19岁开始他跟谁他种子跟谁聊他跟peterdeal聊peterdeal跟他在一个餐馆见面手上拿了一张termsheet说这是这个我的termsheet然后扎克伯格说好的谢谢你我什么时候就是什么时候给你答复他说我们这餐饭不吃完你不签我这东西我现在撕掉就这是一个19岁的一个创业者就没有见过这一种大风大浪的事情他这个故事就是他就去了洗手间他去洗手间哭了一场回来签了这上面肯定有他不喜欢的terms他放弃了他去其他竞拍的机会我觉得就是年轻创业者真的还是挺就是当然创业者这个事情就难就是年轻创业者这个事情就是你大部分时候你并不知道你自己的这一个决定它到底是对还是不对的你可能等一会儿有更多的信息会能够让你对你自己的决定感到更加的自信但并不一定让你决定更对或者更错而你去等这个更多的信息这个过程中是一个高风险低收益的一个过程所以就是有些时候你还不如就直接跳下去就是我记得我们有一个有一个投资人他拉我们一群女性的一个创业者去一个一个活动找了一个那个森林然后在那个森林里就是ziplining就是你你抓上那个东西你就你就你就晃过去就是一个树还有一个树中间有个绳索你知道自己栓在这个绳索上我当时我第一次我人生从来没有做过这个ziplining我就不敢下去然后呢但是就特别尴尬因为我是第一个人后面有一群就是女性创业者她们都玩过这个好像她们以前可能去年就有这个活动然后呢她们就有点等得急然后我就只能就是一闭眼一咬牙我就下去这个过程后面她们跟我说我希望你能形成这种肌肉记忆就这就是你每一天需要去重复的麻木的这样的一种taketheleapoffaith所以我觉得呃对这是我我希望可能说我希望我如果说就是再来一次还是这个年龄的话我希望我以前就是能够把阅读再再抓紧一点我可能希望能读三倍的书我可能我所有所有所有我学过的东西都不够用这是一个非常有挑战性的一个一个事情其实就是因为这种高压快速决定呃的的这样的一个一个一个nature因为不管怎么样你在那一刻你得跳对你有遇到你要绳栓的不紧吧就就完了嗯对你有经历像小扎那样跟peterteo那样的时刻吗然后自己在卫生间去哭一场回来欠了我有一些呃我倒没哭但我有一些各种各样的感受到比较艰难的可能我现在做的这个决定我以后会后悔但是我也得做这个决定的时刻比如呃比如说就是大部分的人才的人才的早期大部分的人才的情况就是人家手上有六个offer你你得敬佩对我成了那个但我又我没有人家有leverage你做不了PeterThiel对吗嗯嗯但你是决定出还是不出你肯定得出呀你你你你就这个这个事情为什么他痛苦就是你其实只有跳一个选择你你只要biastowardaction每一次你在执行与不执行做和不做中选择那个乐观的选项你就能够有一天走到那个终点嗯这这其实是一个但是对这这其实是一个我的一个一个一个一个感受就是有些时候其实没有办法去想了有几次这样的情况很经常很经常很经常对硅谷的AI人才的价格已经非常高了对但也不单止全是人才的这些就是有很多很多类似的时刻对除了人还有什么除了人还有什么嗯我们又有一轮融资啊在这一轮融资中也有很多的一些故事对啊或者说是嗯就是很多很多的情况下我觉得就是要让利吃亏嗯啊每每一天的让利吃亏让利吃亏让利吃亏这样才能够做到一个呃一个一家一家伟大的一个公司让利吃亏对就是让利吃亏嗯种子轮是25年的1月到3月几月close呃到7月close准呃夏天close然后与此同时你辍学了当然等那个签证等了等一会对对对然后第二轮就是A轮是二五年底开始的吗不A轮没想融A轮在圣诞节的时候我们已经有的一个投资人说我们要preempt你preempt的意思是我知道你现在不融资我知道你没有PPT我知道你什么材料都没有我要给你一张一张termsheet然后我希望你能够直接现在像Petershow希望你能够尽快的把它签掉这样你就不用再去融资我省掉你这样的一个这是他们的这种就是firstmoveradvantage有这样一个我有这样一个感知1月5号我被叫到了一个呃外地的一个城市然后我给了一个pitch然后呃我拿到了当天晚上拿到了这个这个这个这个这个这个offer然后接下来的一个星期之后还是一个半星期之后拿到了另外的一个offer我们最终签了哪一个offer这是我们的A轮所以是从7月15号到1月15号这个差不多是6个月嗯为什么选了第二个呃是一个很好的问题其实主要的主要的呃原因是就是呃哇我觉得就是后面我们也让就是第一个让他也投进来所以并没有一个他没有特别大的一个一个一个取舍对对对就我反正也能够得到就是嗯很多非常长期以来支持我们的这个投资人的这个这个支持与帮助最终有一个boss的一个一个一个一个解法哦就是领领领头方是谁啊领头方是manlo为什么你觉得他跟你可能更契合对manlo的这一个partnermattcranning是一个从我们种子轮开始对我们提供非常多帮助的一个一个投资人然后他也是本来是他是一个啊电气工程的phd和物理的本科啊然后他是一个非常technical非常呃有一点nerdy非常有意思的一个一个operator他非常的就是founderspirit然后同时Manlo又是Anthropic的最大的institutionalinvestor然后我们是ManloVentures在这个Ventures这一部分继Anthropic之后第二大的AI投资他们为什么愿意为什么愿意我觉得他们其实种子轮可能就像头但我们当然种子轮就认识的时候比较晚嗯就是已经差不多是就定下来了对然后我觉得我们在六个月里面这个团队嗯执行的快转很这个这个团队在这个六个月的执行中持续表现没有失误而且他们在从零从什么都没有就是第一个月搭所有的infrastructure然后完了之后开始去train模型搭系统然后去做这些决定就是deterministic确定性的tooling而不是写用另这个编程语言去写所有的这个东西是一个非常我觉得是spectacularlyexecuted的一个非常完美的呈现的一个工程项目然后在四个月的时候拿到了普通人的满分然后在六个月的时候去做出了许多研究问题没有许多一批三四个研究问题的解决然后是没有人类干预的第一个自动形式化证明系统达到这样的一个里程碑然后又又发现了一些在代码证明中的一些神奇的transferlearning就是呃原来这样的一个AI数学家能够在代码的验证中呃达到一个非常好的一个表现呃在一个verenabenchmark中deepseekprover达到了1%当然这是老版的deepseekprover了我们达到了98.3%啊对就是原来的这一个呃解决普特南的这个数学系统嗯所以他是主动批评的你我们就是大家都经常有时候会定期会见面毕竟他们是我们种子轮的一个小的一个他们种子轮放了他们是我们种子轮1%的投资人然后现在是当然作为领头整个过程整个过程当然会更加的更加的多几步对这一轮融资的估值是16亿美金对已经达到一个独角兽的标准融了多少钱呃我们融了呃有至少是两亿美金两亿美金嗯这个过程中其实你们团队很多人都就是看起来经验都比你丰富很多对然后包括也有非常知名的数学家的加入为什么他们都愿意让你来做ceo你刚刚也说你是一个最年轻的一个然后也没有任何的techleader的背景他们为什么对此没有顾虑我也不知道哎我也每天在想这件事情就是可能他们也没有意识到我也没有意识到反正就是大家就一起在执行然后现在的一个设定就是所有的一些比较strategic的一些事情其实就会就是route到我和叔狗这里对所以我们其实能够使得研究者和工程师们有很好的一个环境可以去就是在没有任何politics没有任何人事纠纷的情况下去纯心的去就是纯纯粹的去最新在技术上然后就是去执行所以我觉得这是一个很好的一个frontierlab的一个环境然后嗯我觉得还有一个就是这个这个问题它是一个非常有意思的问题它非常的宏大它也非常的困难然后这个事情又有很多很明显的12345为什么这些技术上会难做但为什么这些通过好的就是engineering都能够去解决所以呃我觉得大家其实是被这个问题这个北极星去吸引嗯对我只是那个地水的人嗯对你们也算是现在的一个NewLab对吗我们是在那个TBPN和这个滴滴的这个NewLab名单上确实是嗯对你怎么理解也就是在相同类似时间内成立的这一波NewLab对我当时融资的时候还没有NewLab这个概念所以第一轮融资的时候对对对所以就是他们就觉得我疯了就是投资人就是他们就是可能就是觉得这是什么呢就是当时而且还有一件事情二月份的时候deepseek出来了当时大家对模型这两个字就非常的恐慌大家一听模型哎不赚钱不要投就是模型这个感觉模型还不如一个consumer产品有mote但当时大家是这样的一个市场的一个为什么因为deepseek把价格拉的非常的低对他commoditize了模型所以说大家都不想投模型了然后但是大家没有意识到一件事情我们不是一个模型公司我们是一个deeptech公司我们是一个深科技公司我们做的这件事情有点像SpaceX为什么你们不是模型公司你们相当于训练一个数学的数学家大脑啊对就是另吧他有一个很古老的一个背景就是这一些做programsynthesis我查了一下这个中文怎么说叫做程序综合我也不知道这个对不对呃然后呃programverification就是程序验证就是它来自于这样的一个古老的一个领域然后另作为一个形式化语言他目前就是在呃公开的这个呃的呃domain的的领域的网上的这个这个总的这个tokens这个就是字符串的这个这个这个这个就是不太大就是它是一个非常小的一个一个数据数据集所以说就是会遇到很多的问题比如说你怎么样能够做一个internetscale一个一个互联网这么大的像有多少Python就有多少Ling这样的一个数据的这样的一个扩充呢这是一个不太清楚的一个问题Ling它作为一个编程语言又带有自我验证的这样的一个性能有点像既是一个C编程语言又是GCCcompiler和Cruntime两者合一它是一个非常finicky也就是说非常脆弱的一个语言它的这个它有很多的限制它有很多的就是作为里面的这个object它必须要符合一些种种种种的这个限制它所以它是在作为一个另它本身又带来了这些挑战然后呢另里面又比如说我想去验证一个东西它真的是在证明没有给我就是作弊作弊比如说我假设公理n加n等于n证明2加2等于2你知道2加2等于4这一定不是一个合法的一个一个一个运算那么我如果要去找一个东西能够去证明它是严丝合缝的叫VerifyProofVerifyProof这个东西原来叫做Community里面用的叫做ComparatorComparator这个是比我们现在我们自己的这个VerifyProof慢一百倍的也就是说在我们刚开始的时候我们必须自己要造一个快的东西不然我没法跑我们造了大概十二十三个这一些这一些能够辅助这个令能够更好的去去去去执行的呃的不管是生成还是验证的的的这些工具然后呃我们知道说AlphaProof用的是这个蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙蒙我没有理解你为什么说你们公司更像SpaceX因为我们有很多的这些技术壁垒而其实某种程度上如何去训练一个模型当然说更高更快更强然后又有很多的一些大家的一些secretsource我们这个问题可能在就是他遇到的这个科技挑战上时间会更长我们至少在种子轮的时候是觉得我们的RDcycle是会拖得非常长的我们主要的这一个竞争对手我们刚刚开始的时候是他们五分之一只融了他们五分之一的资产我们的估值也是他们的五分之一然后他们比我们早开始两年就是Tudor的这个公司然后他们用了两年的时间才到IMO的这个这个六道题里做了五道题我们觉得至少得花我们很长的一年半一年但我们没有想到说四个月我们就往这个普特南冲我们做出来一个满分然后接下来冲这个研究的一些问题其实都是世界各地的数学教授给这个小野肯老师他发邮件说就是以色列有一个Technion这个大学的LGFel这个老师给给Ken发了一个邮件然后这就是FelConjecture然後那個KenRibbit和Ken又有一些交流然後有這個ParshaVandiver大圍城這個波士頓的一個一個一個一個代數幾何學家他他又有這個一篇文章反正就是我們其實某種程度上在很大的壓縮這個事件這其實導致我們也有一些infra上的一些債要還所以我們現在也有在還一些infra的債小野肯老师对你们团队来说是一个非常有呃标志性意义的人对他像是一个他的性格是一个高中的篮球队教练哦他的性格是一个就是他会给所有人就是就加油助威然后让大家就是非常呃兴致勃勃的呃乐观向上的去去去去去做我们手上的任务的这样的一个人是你找他还是他找你啊他是你之前老师对吧对他给我发了一封邮件几月份就是你上个月融资已经公布了对吧但是对但是1月我们去年我们之前就有邮件的一些就是交流你当时邀请他了吗没有不敢对吧不敢我也不敢我也说过我我不太敢就是对啊你说我自己告诉你他要来的吗其实我觉得融资也是这样我不太敢要钱就是我是我是说你我没有办法去说服你你只能自己说服自己如果你想做这件事我也想做这件事我们可以一起做这件事哦对但我不希望我万一开始引导你我有可能会误导你就是这个大家要大家都是成年人自己做一些有趣的选择然后一起去去去去去承担这个选择的风险所以你跟舒伯的过程更像是我一直在告诉你我在创业的进展然后你等他自己说我要来我知道他是一个工业界元老毕竟你在director这个level上我觉得可能也有很多项目我怀疑交付的时间会是比较长的对但后面这个Fair他后面就是这个组织很多的人都离开了对对所以他是自己跟你说他要来对他是怎么跟你说的书包就是在worth咖啡店说的他怎么说的呢他就说好多好的人都走了感觉这个地方不太像是以前的地方然后呢往后就是你要一起做吗我说好那个时候你已经融当了呃对二月对吧对已经有一个offer了对嗯然后他有跟你谈条件吗就正常吧就大家就是按照标准的来你当时什么心情我挺高兴的我觉得挺高兴的因为我觉得感觉一个人做这个事情比较孤单你有预感到他会来吗我有预感到但我我们当时我当时想如果他来应该一年后来就我们可能我我总觉得就是其实我现在对我们的公司现在的一些新加入的一些成员我总一直我总有一种就是我感觉我们就是我们希望我们能够把我们做的做的最好让我们能配得上他们的这种价值所以我当时想一年了这个可能做出来一些小成绩然后这个书我可以来指点江山把我们就是往往上再做一步但是这样一个想法那你的老师呢老师对他给我写了一封邮件1月底非常怪的一封邮件他大概意思说他要来湾区我说啊你要来湾区然后他说嗯如果他加入了OpenAI或者是DeepMind呃的话我不应就是他他希望我有个心理准备然后我心想你要加入OpenAI和DeepMind那你为什么不来我这里然后我就说你可以来我这里然后这个时候你之前没有跟他说过这个话是吗没有我我我但是我但我也就觉得你如果能够去加入openai和dman我觉得你可以来我们这里我觉得我们他说那句话是在暗示你吗就是说他是真的我觉得需要一些建议哦他他当时openai可能给了他一个offer哦那为什么他说的是你要有心理准备就是因为我们他我们知道我们知他知道我有这样一个公司吗有可能会可能会有一些竞争关系对吧openai的aiformath的这样的一个division可能和action会有一个战略竞争关系他可能作为我们的我们是朋友吗他不希望我很突然的听到这一个消息就是他在给一个竞争对手进行工作哦所以他希望他能告诉我说可能这是他的一个选择也希望我能够理解然后我说那来action哎然后结果就弹得非常快非常好他是来玩去跟你谈的还是线上自由谈的没有就这么谈的我当时就是我当时飞飞的乱七八糟1月底12月从我是从这飞到了呃飞到了阿斯维加斯是reinvent然后飞到了这个neurips我们在那个neurips赞助这个AIformath的workshop然后我们有一个就是活动可以就是招聘的一些活动我就在SanDiegoSanDiego回来然后是这个出了就一堆一堆事嗯哦你怎么说服他呢在你那个字幕会上你说你对你对比OpenEye你的优势是什么我我倒没sell他我就说我们非常的就是呃我们也open你来然后你可能还是得去OpenEye看一看如果你能有时间来我们这边看一看结果他没时间来我们这一看我觉得肯定凉了你想他来弯去他就直接去OpenEye然后就飞走了他没有在我们这那可能说明我们没有什么机会结果他来了哦他来你公司了对他是来你公司跟你谈好的对啊没有他没有来我公司谈好就是他他在zoom上我们就就定了你截胡了openeye对嗯你怎么说服他呢他被什么打动了呢我觉得首先他觉得我们的嗯就是这个团队更数学这是一个事情嗯就我我怀疑发生的事情就是他去了openai之后可能觉得那边比较呃做数学的同学不是特别多来我们这边的话可能有更多就是数学的一个氛围这个这个公司的DNA和专注点就是数学而不是一个general的AGI然后数学是其中一个部分可能更有marketing的成分小野肯贝鲁认为是继承了拉玛努金精神的现代数学家之一而且他之前说他根本不相信AI会超过自己然后后来他内心发生变化可能这是他联系你的一个契机我觉得是对他有跟你说过他这个认知是怎么发生变化的吗他有说对然后我我其实记得就是我们当时聊的特别的仓促因为这就是一个截胡哦对多长时间呃就是两三天内OK因为那边那个offer要爆了就爆炸explode了哦但我们这边我觉得还有一个很大的原因看加入是因为FrancoisChartonFrancoisCharton是AIfor数学的这个呃的2019年Francois和GillianLampeauMistral的这个ChiefScientistCoFounder他们一起写了一篇文章叫做Transformer可以在呃微积分上在在Integration上能够比一些像MathematicaMathLab这些电脑系统要电脑代数系统要做的好然后从那开始Francois就一篇又一篇的去去做了非常多重要的文的的工作去去让这个AI解决各种各样的就是specialized的就是特殊的数学问题然后在AIformats这个领域里面我觉得就是Ken还有Francois他们肯定是对对方也非常惺相惜然后Francois作为我和Suber之后第三个来加入我们的就是我们我们这个团队的他们就有很多的共同语言然后事实上现在Ken加入之后又有Evan啊Kenny啊GGen就变成了一个ItscalledaMathClub就是我们这里有一个数学俱乐部大家都有很多可以聊得来的东西然后他也给了我们这个ActionPool去解决哪一些问题选择这个问题给了很多很不错的建议嗯我想多问一个关于小约肯的问题他是一个什么样的人他就是高中篮球教练他就是特别特别乐观特别嗯特别就是让人你跟他聊你就会觉得哎呀我本来就很想做这件事情我现在够想做这件事情了所以他是我们特别好的一个文化上的一个一个一个一个增加然后他也是当然是一个非常好的数学家他在这个划分函数领域里面就是非常年轻的做出来非常好的成就然后他也是一个很好的研究导师他带我做了很多文章然后还有很多其他他这个REU的同学都成为了不错的数学学者他是个直觉派的数学家吗这个我倒是不知道这是一个非常好的问题我觉得他应该比我更直觉派嗯对但是我比如说我们就是合作的过程中像我一个合作者张盛桐他就是比肯定是比这个我和Kent他比我们两个都要直觉性所以就是看我觉得在二者之间看哦看的这个我我理解了看的这个神奇的能力在于他是理论建造者数学里面大概分两种一种叫解决问题者一种叫理论建造者他能够把不同的领域的东西去去去连接起来然后有一个完全全新的视角看一个问题他能够去发现很好的问题并且给其他可能更善于解题的同学们去做他会觉得他从学校放弃了终身教职加入一个学生创业的公司他会觉得有某种奇怪的感觉吗我没觉得我觉得Kent反正和我我们两个都是比较就是叛逆的人对就是我觉得Kent这把这个他在数学教授他同时又是美国这个奥林匹克游泳队的这个教练去给他们分析这个游泳的数据怎么样去把表现更好的提升他又去拍这个好莱坞电影拍了拉玛努金的那一部现在又要拍第二部拍这个米爾扎克哈尼的這個第一位女性費爾茲獎得主的這個電影然後他同時又做很多的就是他有一個慈善基金會就是以拉馬努金命名的去給一些很年輕的世界各地的希望能夠拿一些資金去買數學課本的同學們一些輔助同時他又是美國數學學會的前任副主席然後又是在白宫又有一些政策上的就是咨询顾问的一些职位所以他是一个非常全面的人他作为一个数学家然后加入一个AIformath的公司建造一个类似于AI数学家会替代自己吗? 他倒不覺得會替代自己我們其實大家都覺得就我覺得他就是思想非常開明作為一個數學家有一些數學家可能真覺得就是AI去代替自己不是一件好事情但是我們見到的越來越多的比如說Ken比如說AndrewGranville那也是另外的一個很好的加拿大的一個數論家Andrew也是我們他也是著作等身的一個數論學家他們其實一個想法就是隨著AI的進步人類數學家會學習在不同的抽象層面上進行邏輯推理這是一個非常有意思的一個點就是我們某種程度上在編程這一塊以前編程我記得如果你去這個計算機博物館就在這附近以前就是电脑计算机就是有那个小卡片然后你在那里打洞就是那个那是很很早以前的一个computerscience的一个雏形后面有一些更lowlevel更低层的这些编译器语言然后一直后面到python现在到可以拿自然语言进行webcoding编程然后数学其实某种程度上数学家也会学会有更更高高层的这个抽象的这个思维比如说我刚才讲的有可能他们就是去说这些问题是值得去探索的然后让这个AI去帮他们探索我们希望我们真心的希望我们的AI能够有具备一定程度上的猜想能力能够让这个猜想的这个部分与证明的这个部分进行某种向上螺旋就是我希望他能够随着这个actionprover能证明的东西越来越多我们每一天证明的东西都会进入到明天的明天的这个应用中不管是作为一个skill一个技能就像legoprover的skilllibrary这个设计或者是去作为未来的训练数据我希望他一定是selfimproving的某种程度上selfimprovement甚至说你可以叫他continuelearning当然这是一个最近很火的一个词一个buzzword在一个能够有验证signal的验证信号的一个领域像数学来说是可以去试验的这些很好的很前沿的AI的一些东西包括subagentsskillsmcp这些东西全部可以在我们现在的这个数学作为一个操场一个playground上可以去试验你们在普特南的那个对对那个故事可以给大家讲一下好就是大概就是在205年12月6号这一天早上我们收到了呃就是普特南大学生数学竞赛当天的考卷然后我们是拿到那个考卷之后就我们要做的第一件事情就是我们需要把它呃变成形式化的这个题目让这个actionprover我们的这个AI系统去去做那我们这个呃题目当时其实挺有意思的早上六道题下午六道题如果这个题目本身是一个证明题的话那么就可以直接就是把它变成形式化如果是他说要求解的话那还需要求解所以其实还是一个挺有意思的一个过程我们所有人都在这个办公室的一个Poncurry庞加莱这个会议会议室是我们的这个WarRoom我们的战争战争室我们就是在他们数学家有些人就在解题所以其实就是解题的这个过程还挺有意思的就是我们可以看到说有人类的解法和就是我们最终这个ActionProver产生的这个完全是不一样的一个思路我们在大概当天下午3点58分的时候我们是发现我们有八道题然后我们有八道题的话就是80分80分是一个什么水平80分一共120分去年的80分是世界前五然后呃但是往年他80分可能不是世界前五前前十前二十差不多这样然后我们然后我们就希望能够拿到一个90分因为我们当时就有一个选择我们是否告诉世界我们做了还是我们再等一等然后我们最终确实是有就是12道题就是全部满分然后这个过程还挺有意思当天我记得就在解题的时候就是呃小野肯教授他有在有一些非常有意思的精彩语录然后我和舒伯我们两个人就是笑的就是前前后后和他说嗯不要在现在不是说数学纯粹之美的时刻不要去精确的去搞这些东西现在是战争状态就是在大家在求解的时候他就说能怎么快捷的去去去做就怎么快捷的去做就得到那个数之后喂进这个actionprover也其实是和IMO的这个其他的这个标准是一样的就是说如果有需要求这个解法的题把这个数就是一块的喂进去因为另只能做证明嘛他不能够帮你说是去求解所以求解是人做的是吗求解这个东西是人做的求解在IMO的那一个就是IMO的那个考试中甚至是204年其实这是AlphaProof他给的先例就是有6道IMO题然后有一些题要求有一个得数这个得数的话就是要把它一块放进去变成一个证明但是后面我们发现一件事情就是我们其实可以不求解就我们其实因为我们这个系统里面也有一些就是informal的这个model其实我们是可以直接让他就是做出这个解法的最后其实我们发现我们的每一道普特南的题其实我们并不需要做人类求解内部但我们以为我们要求解所以还挺有意思的小野狠小说为什么说现在是战时状态啊因为就是时间紧就是我们大概估计说一般早上六道题和下午六道题加在一块十二道题最多不超过三道题需要求解因为确实是少数的大部分还是证明题早上那道试卷下来就是六道题四道题要求解然后我们当时只有就是能做得动这个数学题的人呃就是基本上就是我普特南成绩也不怎么样反正基本上就只有EvanChen然后EvanChen就一个人在那里就是一道又一道题的做还是非常非常有意思的我们其他其他同学有些人就是在就是把这个数学题变成0然后啊看他自己其实也没有做出来多少道就是普特南的题因为就是研究型数学家和就是这种打竞赛在一个最最短时间内的还是很不一样的一个数学家的一个一个一个特性你们公司为什么叫原理啊啊我觉得action是非常美的词就是我自己很小的时候有一本书就是叫数学天书中的证明就是说如果说上帝有一本书这本书里面会有哪些题数学天书中的证明就是说有一些这样非常好的数学结果呃我觉得就是公理给我的感受就是首先把它跟另这个形式化语言它是呼应的就是从一些有限的一些公理中可以推导出新的一些结果就像是有地基然后你再往上建高楼呃另外一个我觉得就是action这个词就我觉得很美它很数学它很它很克制它很理性嗯它又很sharp它就反正我我非常喜欢action这个词他就感觉来自那本甜书对然后我们公司里名字开头是a的人也特别多我们alexalbertoarm反正一堆这名字开头是a的我们是action你觉得ai会把数学的历史推向一个新的阶段吗会我觉得会我觉得这是非常让人激动人心的一件事情就是随着这个我们以前的这个世界能够做到比较顶尖的数学思维的人是很少的我们现在会成从一个masspoor到massrich的社会我们会从一个数学数学的匮乏到数学的丰富的这个supply这个供给会爆炸这是一个让我个人来说非常激动的一个野心就是你想一下所有没有被解决的理论问题所有可能说是应用科学家们他们遇到的希望有一个数学家帮他们解决的问题全部可以解决就是一个时代的我觉得一个可以被定义就是说指数级的数学发现的增长这个我觉得一定会发生然后数学家们会扮演一个什么样的角色数学家们我觉得会扮演的角色就是他们能够提供最好的直觉他们会是能够提供到0.1%的直觉说哪一些数学问题比起哪一些数学问题更值得我们去集中算力去解决我可能会讲一个这部分会听起来显得我非常激进我觉得这个就好像说是很多不同领域的数学家他们比如说三四十个人或者说是十几二十个人会聚起来去谈论说我们的wishlist我们未来希望的这些问题被解决然后这些问题的重要性这些问题的连接性也就是说如果你解决了这个你应该能够把这一些都解决这样的这个过程可能会是他们的主要的数学工作然後實際上是由這個AI數學家去解決這些問題比如說如果我們當然是兩種情況我們人類有可能有有限的算力能夠去我們人類決定花在數學的發現探索上另外一種情況是我們其實某種程度上有很多很多的算力我們可以花無限的算力在這個數學探索上这个当然也包括说比如说现在我们可能能够用更少的算力做更好的事情如果是有限的话数学家其实他们某种程度上就是这个资源分配者他们的直觉告诉我们说我们应该比如说20个H20花在这道题上80个H20花在这个题上某种程度上算力就会成为去与这个数学家对于这个数学题的重要性某种程度上划一个等号這是個資源分配問題如果我們現在在一個無限算力的這樣的一個情境下的話那就是像是那個ThinkingGame思考遊戲那個紀錄片裡面有一刻他在一個這樣的一個會議室裡面他說AlphaFold已經做出來了他們剛拿了那個獎現在下一步是什麼呢他的手下的一個科學家就說我們做一個平台吧讓這些結構性生物學家可以去提交他們希望被折疊的這個蛋白我們折完了我們給他發回去Demis坐在這個桌子上就問說有多少個蛋白然後人家說有20個million2億個蛋白然后Demis就把笔扔在桌子上然后就说结束会议吧就是foldeverythingthatwasastupididea那个平台为什么你去做一个平台呢你可以把所有的东西都折了如果我们在一个无限的算力上的情况下我们就要做这件事情我们要把所有能够人类想到的好奇的数学问题全部解决所有与应用科学家物理学家他们就是在意的一些问题比如说很有意思的一件事情中国剩余定理现在被MIT的这个Elaphate去用在研究这个有多少个神经元能够叠起来这个neuralcapacity这个空间里能够有多少个神经元这样的一系列的研究中我们做梦也不会想到数论会与初等数论会与会与这个计算机神经科学理论神经科学产生关系另外一个例子比如现在整个的这个法律与经济这个文献都是两个人一个是斯坦福法学院的这个MitchellPolanski我当时上了他的LawandEconomic法律经济seminar然后另外的一个是Steven他是在这个MIT我忘了他的lastname但他们两个人就有非常多的就是关于法律与经济怎么样去想比如说我有一个刑罚有多少是用来让这个社会不要犯罪有多少是实际上是对这个人他个体的某种程度上的修正与惩罚这个过程可以拿就是微分方程去他就是有非常非常多的我在法学院的时候就是还帮他算了挺多微分方程就是能够去去去去解就是数学其实可以被应用在这个TimGowers菲尔兹奖他有一个非常著名的一个一个一个话就是为什么我们国家基金委什么的需要去继续给呃纯数学去提供这个经费呢是因为数学是一个生态系统你有纯数学你就有应用数学你这个纯数学你如果死了你应用数学也就没了你你可能确实觉得你作为一个呃一个政策上呃这些应用数学更与实际的这个市场啊与社会更有关系但是如果你不去做这些基础科学的这个当然这个也与其他就是学科比如说生物的基础科学也是一样的一个一个一个一个一个一个一个一个一个论点嘛就是说你一定要去进行通过理论层面上的发现我认为从数学mass然后到code到这个这个编程去在软件层面上去做一些甚至就可以到realworldtesting实际世界上的一些验证数学和代码某种程度上是孪生兄弟mathiscodeandcodeismathmathiscode因为有一个叫做CurryHoward对应就是它是一个Lin就是基于这个我每一个数学证明可以变成一个一个计算机程序codeismath为什么因为code现在我们发现为什么backend甚至是整个distributedsystem的webcoding没有办法做到像就是做一个网站这样这么好其实就是因为它有很多的一些没有办法backtrack没有办法做很好的就是hierarchical就是分级的这种拆解对这些能力其实某种程度上数学能够给到它然后数学和编码的这一对孪生兄弟是一个你能够在我们现在这个人类世界上有这个验证的验证信号的一个方面另外一个部分其实就是实际世界里的这个实验对吧比如我扔一个鸡蛋它的重力会到这个地上鸡蛋会碎就是这些实际世界里给我的reward所以我觉得我们的AGI的这个work就是数学然后编程然后实际的这些rewardtesting然后everythingelse嗯对你觉得在AI4Math的领域会诞生类似于XGBT的时刻吗我觉得会然后我觉得就是如果有这样的一个XGBT时刻它不单只是数学它一定还会有一个就是coding代码的这样一个部分其實這個事情挺有意思的就是我們做的這個東西很多人覺得是它對驗證有很大的意義然後對另外一些人覺得這個對超級智能或者說數學推理有很大的意義它其實某種程度上這兩者是合一的嗯这个我觉得比较就是这是一个可能不太明显的一个一个点就是我们我们是在做一个就是AI的一个数学家但是我们又同时是通过形式化证明就是加入进传统的比如说就是LM推理这里面去去做的所以我们产生的这个输出是可以比如说几几千行就是另的这个代码然后这个东西它完全可以就是自我验证如果我觉得有这样的一个TryGBT时刻的话它某种程度上产品一定要加进来就是这是一个我觉得我们时时刻警醒自己就是作为一个就是在把这个系统就是能力见到越好的时候其实要要记住就是说某一天这个东西一定是要尽快的去产品推出和落地这是一个点然后我其实觉得就是有一个GPT时刻然后前年可能一般有一个比如说有点像当时早期的时候大家说就是AlphaGo时刻其实我觉得AlphaGo时刻对我来说是两个时刻第一个时刻其实可能是这个GoogleDeepMind在204年拿到了这个28分银牌另外对我自己个人的一个AlphaGo时刻其实是在今年的就一月份的时候Axiom他去能够AxiomProver证明像fileconjecture,partialVandiverconjecture这些包括同时Ithink就是deepmind有一个Alythia那是一个非形式化的那是一个就是自然语言的一个他也证明了一些研究问题其实我觉得是这这两个时刻吧一个是outside数学一个是研究数学你觉得AI4MAP它会沿用就是大语言模型的这一套整个的技术范式吗还是会在下面上面做新的创新我觉得就是它是一个很好的你想试什么试什么的一个环境就是我们环境它是一个它是一个就是它是一个很好的一个设置就是你可以在上面去试你认为一些会成功的一些事情然后这个可能在别的一些没有那么clean的一个domain上不好做就是在我们这里我觉得我们可以做然后比如说我觉得差不多AIformath有一套范式对吧就是从draftsketchandproof开始20年的一篇文章首先呢你让这个informal的模型给你列个提纲其次呢你把这个提纲变成formal的变成lin的然后呢你再把这一些中间sorrysorry是lin里面的一个一个一个tactic一个一个一个语法它这个sorry的意思就是说我这一块我不给你正但是你你知道就是它一定是对的相当于是让你把它takeitforgranted的这样的一个就是第一步就是draft提纲informal第二步sketch提纲formal第三步proof把中间的sorry全填上其实填sorry有好几种方式可以填你可以拿这个AI去填你可以拿一个就是有neuralnetwork的你也可以通过一些就是原来ATP的那些纯规则的没有这个rulebased的没有这个AI的这个去拿这些东西去填就是让它自动的比如说hammerLynn里面有一个东西叫做hammer就是hammer就是顾名思义一个斧头斧头就是我一斧头下去这个story就没有了这个Lynn这个hammer的这个历史其实特别有意思很早以前其实有其他语言像Isabel是另外的一个定理证明的语言然后另外一个定理证明的语言叫做COQ后面改名叫ROCQrock他們就是有hammer了比如說有一篇非常matchedhammer它是我如果記得沒有錯的話它是Isabel的一個hammerLynn裡面一直沒有一個hammer直到我記得去年六月有一篇文章就是CMU的幾個人出來一個Lynnhammer但是Lynn的hammer它並不足夠他的这个就是功能并不够涵盖所有其他的Hammer的尝试所以大家就是我们当时就有跟Lynn的这个创始人LeoDeMora我们说Axiom希望能够就是做一个就是我们给你basically我们给你赞助你能帮我们找人做一个全部开源的给所有社区的一个Lindhammer嘛后来这个他们可能是人力上就是不够人他们不是说没有这个资金所以这个事情没有做成但是到就是今年的时候有一个新的一个东西出来了叫做GrindGrind这个其实某种程度上它能够解决很多的数学的问题我曾经见过一些其他的AIforMath数学公司他有做一些demo其实那些题你如果grind一下甚至他都能直接给你做出来这里面没有任何AI的一个成分我们觉得的这个世界是AI和這個formalverification兩邊就是兩股力量合在一起去解決一道題就是能夠用deterministic不上這種probabilistic概率性系統的我們就拿這些東西把它解決然後另裡面自己能夠做出什麼樣的抽象層能解決一些也能盡量解決一些就是我觉得一个很好的一种系统设置就是说先是最简单的最便宜的能解决就就解决掉不然然后剩下的再去上这一些呃就比较大块的这些这些这些就是呃大约模型系统有某种让你觉得非常啊哈moment的时刻吗对我觉得我们每天都是啊哈moment我觉得这个这个团队还是挺快的他们就是其实我觉得有几个呃东西我觉得可能是比较比较前沿可能就是其他人没有就是第一个就是你如果觉得呃montecarlotreesearch这个蒙蒙地卡罗树搜索太太太费钱了就是太效率太低了的话你有什么别的办法你我们希望能够scaleinference吧inference这里就是去呃做做做大呃这个的一个一个我们觉得可以尝试的一个办法就是可以看一下anthropic他有最近讲的一些subagents这样的一些方向其实我们觉得subagents用来做afms其实做的很好这个是一个然后DavidSilver和这个RichardSutton他们写过这篇文章就是AI后半场这个learningfromexperience从经历中进行学习这个东西其实某种程度上在一个数学题里什么是一个经历这个经历就是一个数据的trail一个一段到达你最终解决这个题目的这个部分这个过程全部可以作为你的这个experience经历然后随着你能够让你的这一些subagents能够应用的skill而skill就是learningtousetool学会使用工具那随着这些种类选择种类变多你可以去做scalinglearningfromexperience这些东西我觉得我们做的比较前沿这是这是一个一个我自己个人的一个ahamoment所以一个数从比如说40个40个node40个顶点的一个一个一个数一个一个一个一个证明就可以把它转化成一个数这个数从40个我们已经现在scale到40个就是它是一个更深更广的一个数这是第一个我觉得我们可能做的不错的一个点第二个我觉得有一个我们的AHAmoment其实是就是我们发现这个数学的这个定理证明的很好的一个AItheoremprover能够转化到它很强的代码验证能力对有一个我觉得就是在这个verinabenchmark上的分是我们看到了一个让我们都很惊讶的一个事情然后同时可以生成代码和这个证明其实这是一个很有意思的事如果你想就是正常的一个代码是python然后证明是英语就是自然语言那如果你去做就是强化学习的话你相当于它指着你往两个地方走你到底是python做的好还是自然语言做的好那你如果说是你把这两个目标函数把它就是聚拢起来你让你的这个代码和这个这个代码的正名它都是lin或者说甚至代码不是lin吧它是rust它也是一个它也是一个就是lin是dependencytypetheory这个rust是一个stronglytypedlanguage它可能就能够让它这个收拢反而能够能有更好的一个verifygeneration就是一边验证一边生成的这样的一个一个时刻这是我觉得第二个我觉得我自己觉得比较美的一个东西對為了更好地理解AI4Math能不能給大家講一講就是在你的心目中AI4Math它在整個AI的大地圖上它應該畫在哪個地方能不能給大家一個買品好AIforMath我觉得现在就是convert收敛到大家差不多其实是一个做法就是我先拿一个opensource的一个开源的一个先讯号的一个模型比如说我拿这个Quant或者我拿这个Quant的一个模型然后我在上面去做就是做后训练然后做后训练大家做法不一样有些人就直接上RL有些人是SFP然后RL然后做好了这样的一个model之后把它就是去可以说是放到一个系统里面去然后这个系统里面有各种各种各样的model有一些model还可以做一些就是非常specialized的一些东西然后这一个系统差不多它去call一些tools然后这些tools一些tools其实还蛮难做的就是要做很多一些lean的metaprogramming然后这整个的这一个这一个系统的这个设计有不同的不同的方法我觉得差不多是现在是这样的一个大家其实都是差不多这么做然后我觉得还是有一点点不同可能我觉得我们和像SeedProver,HilbertProver的做法都比较类似然后我觉得好像是比如说Aristotle他和这个AlphaProve以前的那个做法有点类似其实大概分两派然后基本上我们比如说就是邀请加入我们的同学的这个AI的这个过往的的工作都是后训练呀就是强化学习呀然后就是做reasoning做推理呀然后也有招一些做agents甚至swarmofagents的一些同学然后就是非常fullstack的这个engineeringskill也非常需要差不多是这样的一个一个东西我看了很多研究资料我会觉得如果AIformath突破了它应该不会是只解决math的问题它应该是具有放滑性的这个观点对吗对这是一个很有很有意思的点我觉得AIformath大家其实讲的一般讲一个核心科技叫做proving就是证明其实我觉得AIformath它能做的东西也就是说能达到一个更多用处的其实是一整套一整套东西我觉得你需要有一个非常好的一个prover一个证明的系统你需要有非常好的一个conjecture提出猜想能够提出数学问题的这样的一个AI然后其实某种程度上这一个能够证明的AI是你能够提出猜想的这个AI的reward就是我能够拿它去拿这个证明这个prover去做这个conjecture的这个rewardsignal其实有一篇文章叫selfplaytheoremprover就是自我自我對弈然後這個其實是董克帆然後馬騰宇他們就是這篇文章斯坦福的一個文章然後呢他其實就是其實是所有人開始想就是conjecture怎麼做猜想的模型的這樣的一個一個起步點猜想模型的难点是我不像证明模型我证明出来了就是一没证明出来就是零我没有这个reward了我怎么去说我这个猜想是好还是不好然后除了说拿这个能够证明的这个东西去做一个grounding去做一个呃呃呃去给他这个这个信号之外啊还需要加一些其他的东西比如说怎么知道你这个猜想是否在数学上是非常无意义的比如说你完全猜想出来了一个不是那么重要的东西就是一点也不重要我也不知道为什么你会让你的prover去证明这个结论那就可能会有一些东西叫elegancefilterelegancefilter叫做去去判断这个东西是否优雅然后在这个STP这篇文章里面的这个优雅这个优雅不优雅是靠长度决定的就一个东西它的题目比起它的这个正名来说是长还是短这个是优雅不优雅然后但是这个感觉上就很粗糙因为他们其实他们的那个数据集是叫LinkWorkbook是一个比较是高中数学的一个数据集完全這個東西如果做到更高級的比如說本科或者說是就是博士研究的的話你沒有辦法去靠就是長度來就是絕對作為一個唯一的一個優雅的一個過濾所以沒有沒有沒有什麼就是沒有特別没有特别强的延展就是难度提高的时候这篇文章不足够所以就是怎么去做这个猜想目前是一个我觉得比较就是前沿的一个研究问题然后这个猜想的这个猜想家和这个证明家他们俩就是要聊天他们俩就是通过就可以selfimproving就可以自我提升然后呢他们他们还有一个很重要的一个部分是叫做由于由尤其是我们在做形式化数学证明叫做就是啊知识库这个知识库为什么很重要是因为大部分就是存在的数学在英语里面存在的数学或者在中文里面存在的数学它都不存在另里面它连定义都不在另里面所以说我需要一个很好的去嗯我需要两件事情第一个我需要能够很好的搜索我什么是已知的已经被证明的什么是需要被证明的然后或者说甚至说如果你让我证明一个东西我在已知里面找到一个反例那我就直接可以证伪对吗然后另外一个需要的就是说把这一些浩如烟海的数学转化为形式化的数据转化为形式化的数据的话这个过程就是我说的第二个核心科技叫做AutoFormalization它就不是证明了它是转化嗯它這個轉化其實某種程度上一是被忽略了因為大家比如說你如果證明了很多普特蘭的問題或者IMO的問題你就可以到推特上你就會說嗨我證明了我是一個非常偉大的AI數學家但是如果你只是把這個人類已經就是發現了的寫好了的數學轉化為了這個形式化的你會得到更少的這個讚美但是這個科技它其實比這個證明要更難至少是一樣的難度我其實覺得是更難為什麼更難就是如果說我要求比較嚴格我的輸入是一個archive上的數學文章而我的輸出要求是把這個數學文章裡面所有的定理證明的這個對一對東西變成另的這個代碼成为了我的一个另的这个输出那我需要几步我第一步我需要把这个呃文章变成拆分我要拆分出什么是呃什么是呃就是单个的定理和这个证明有一些文章它结构性的比较好拆但有一些文章一个大的证明里面可能能拆出好多东西这个东西如果拆的不够细的话拆的非常细的这个东西叫做什么叫blueprint蓝图陶哲軒啊還有說是KevinBuzzard啊AlexKontorovich這一些數學家們他們用人手寫出過藍圖他們曾經就是在Polymath還有就是後面的一些大型的形式化的這個項目上他們人手寫了這個藍圖之後去丟出去給全世界的本科的一些數學的這些學生去每个人领一个小任务然后所有这些人小任务加起来星星之火可以燎原就整个的这个东西就形式化就就就就就就就就就写好了然后如果你需要让一个一个一个计算机不管是AI还是一个就是Rubix的一个电脑系统去进行把一个从一个pdf一个archivepdf到这一个非常细的蓝图拆分譬如說20頁的一個文章變成一個20頁5的這樣的一個藍圖拆分使得我能夠把這一些藍圖非常細化的東西轉化為lin的話這一步是非常難做的這個需要很強的這種就是分解這種分解推理能力然後所以這其實是一個難點然後所以我其實講的這整個在AI4Math這個島嶼上是一個證明家一個猜想家一個知識庫然後這個轉化的能力就是貫穿著他們的始終這是我們認為的這個这个这个科技愿景然后其实你就会问一个问题说这其实不就是翻译吗把英语翻译成这个lin但是实际上它是不是的因为比如说我把英语翻译成法语英语和法语他们多抽象其实很类似的有多结构性或者多不结构性多松散多严谨它都是很类似的但是Ling作为一个跟Python更类似的一种计算机代码语言这个转化的过程尤其由于AI没有见过多少Ling现在全世界的Ling加起来没有多少的tokens所以这是非常困难的转化回去叫Autoinformalization就是反方向的转化从Ling到英语这个反而是简单一些因为这个他见到了很多的英语但是这个的话比较难的难点就是你如何确定你转化回去的这个数学完全是正确的你如何就是确定它没有错误这个我们一般就是让它再转化成另一点就是做这种就是转化去转化回来再转化去看一不一样这个叫cycleconsistency用这个方法来去做形式化语言和语言是什么关系啊形式化语言其实就像是呃像是比如说PythonPython然后它它某种程度上你可以把它理解为它有就是执行能力对吗它可以就是我可以跑它然后跑它完之后就会看到一个沟那个沟就说我这证明是对的或者我看到一个报错就告诉我第几行出了一个问题呃如果说在哲学层面上一点的话其实我觉得数学作为英语的一个子集数学是英语数学这些里面的词吧比如说数学我表示一个定理我有这些英语的词汇它这些词汇所出现的distribution概率分布与英语语义里的是不一样的比如说在这个代数几何里面有一个词叫做germ这个germ在英语里面的意思是细菌我記得當時特別有意思在疫情的時候我學這個代數幾何所以就是大家就開這個Germ的玩笑就這個Germ它出現的這個概率分布它一定與英語裡面的是不一樣的所以某種程度上如果你希望AI在英語裡面做數學這不是一個非常好的至少他絕對不是事情的全貌而如果你把這個數學轉化為了代碼的話其實我覺得就是他由於剛才我們講的一些可驗證性他其實我覺得更更更更有道理嗯我举一个举一个例子比如说就是在这个另里面你如果去看他这个怎么一个程序是怎么写出来的其实还蛮有逻辑性的他这个他对一些逻辑推理的一些处理还比较好另他作为一个就是自动化自动化形式化证明语言他有一些兄弟姐妹他又有一些其他的这些语言比如说horockisabel甚至原来更老的一些smtsat对吗这些都是就是基于逻辑的这些呃就是证明语言然后我们现在这个世界上我们所有的芯片的一些验证基本上要用Cadence这个公司的JasperJasper是一个基于SMT的一个语言然后Jasper就有很多的局限性就会有一个很有意思的问题或者说我们可以头脑风暴如果全世界的SMT挣扎着的struggle的SMT全部可以被另代替我们会是一个什么样的世界另外的一层问题是lin和python之间的关系是什么样的其实我们就回到刚才的那一个点就是lin可以去作为一些python程序的验证其实还是挺有挺有挺有意思的我听下来我会有一个问题因为像coding也很火对那用math作为手段和用coding作为手段去执行任务的区别会是什么呢对其实这是一个很好的问题他们某种程度上是互补就是coding的话他可以帮我计算出一个output可以帮我计算出一个输出然后呃数学的话某种程度上他可以帮我验证一个性质验证一个property呃我比如说你给我一个问题这个问题我可以拿一个呃编码的这个这个coding去去给你解决我就给了你一个电脑程序然后呢但是然后我就需要去知道这程序写的对不对是否解决了你的问题我现在需要很多输入输出这把这就我的testcase如果这些testcase都可以不需要了直接我可以验证在我写的时候同时验证你的这个电脑程序真正解决了你要的这一个问题通过另那我觉得是一个非常非常全新的世界但是这里就会出现一个难点这个难点其实我我喜欢拿正面的事情去讲我們相信的一件事情就是任何你能定義的你都能證明任何你能写出的或者是任何你能specify就是英语里面programspecification任何你能表达的你都能执行这是我们对于coding未来的一个愿景就是这个事情的难点在于比如你告诉我你的这个问题我无法确定我是否能把它写成一个比较艳丝和缝的一道呃在这个形式化语言里面的这一个这个题嗯所以我其实其实这个可能讲的我不知道观众我可能讲的也不是特别好就是可能再再去orient观众朋友们一点就是呃我觉得这个softwareverification是如下的一个一个布局你有一个啊program这个program就是你的这个电脑程序乘以这个specificationspecification就是你要达到的这个目的你的这个目标嗯映射到VerificationCondition就是验证条件乘以Proof也就是这个证明而Accent做的是这个Proof的这个部分然后能够就是就是所以其实但你要看就是Program有对吧就是我们可以现在很多AI可以写很多的这些就是电脑程序这个Specification反而变成了难点verificationcondition这个东西就是做这些形式化语言的这些他们给我们提供我们解决proof这中间差的就是这个specification任何你能所以这个这个梦想就是像数学一样我举一个数学的例子任何我能写成一个数学问题的问题都会被证明嗯在这个coding里面就是呃任何能够定义的都能够被被执行被做出来对被执行如果难点是specification它应该怎么解决这就是为什么说在这个数学里面这个猜想很难就是做这个conjecture猜想家这个块很难就这就是这其实是难点定义与猜想是难点就是定义比如说我比如说我们之前有一个很火的叫firstproof的一个一个一个一个挑战对吧有一些数学家他们跟还上纽约时报就是讲说给AI出十道题这个openai做了好像做了五道也不知道对不对然后这个deepmind做了六道好像是对的他们当然都是拿这个自然语言做的为什么比如说我们action就没有办法去参加这个挑战呢因为这十道题我甚至都没有办法把它转化成另的这个就题目我放不到另里面为什么我题目放不到另里面题目涉及了很多定义这些定义完全不在不在这一些就是library不在这个mathlib里面然后我如果要去定义这些的话这一步目前机器很难做所以由于我无法定义导致我无法证明所以这是这是我目前觉得的第一个第一个难点对然后在在这个定义之上当然也就是这个这个这个这个命题对吧所以我们还是希望的一个未来是当然一定是有局限性比如说我们知道就是从我们那两道没做出来的题比如floatingpoint这个这个非常难做这有一些就是计算机程序的这个任务非常难去拿我们这个link去进行验证但现在大家都有尝试去各种各样的方法让就是不能够验证的那一些那一些情况变得越来越少其实我问这个问题是想说AIformath它是一个更垂直领域的一个AI的事情是的还是说它能够泛化成一种通用的智能它泛化会泛化的比你这个垂直感受到的效果更慢也更不那么戏剧化我觉得在垂直领域上我觉得你就是是有可能有一个cursorlikemoment的是你能够感到就是就是你能有那种感受然后某种程度上呃他和就是通用的智能有一些关系但在某一些情况下肯定是某种程度上他们还是在在在战斗的比如说我们发现就是数学做的好的AI这个跟人谈话就听起来非常傻就是好像这个这些这些这些这些性能是在互相互相相斥的但是比如说从数学到到到到代码生成从数学到这些就是代码芯片验证这些很明显是是转转化的你说这个cursorlikemoment它会是一种更产品化的moment吗其实某种程度上我觉得是一个概念我觉得好的产品其实它是来源于一个比较深的一个概念就是1980年的时候我们知道1980年代DonaldKnuth这个计算机学家他提出的是什么事情他提出的就是我希望让所有能够我希望让所有计算机科学家都能够vipcode整个所有的事情我能够在像数学家一样在自然语言里面去做推理然后这个电脑就直接执行但不单只是我们现在讲的这个vipcoding因为我们现在还有codereview他希望能够把这一些直接代码直接到这个deployment直接可以ship然后我们目前可以在前端做但我们后端做不了整个的这个系统我们也很难webcode比如说我怎么webcode一个controlflow我很难去很难去做这件事情嗯这是这是一个一个一个梦想然后比如说你可以猜一猜第一个提出形式化证明的这个人是谁其实比这个download还要更早就是就是AlanTuring他就是讲说我我就是希望我能够一边编程这个编程完全背后的这个逻辑不单只是就是这个逻辑和就是它完全能够与我的这一个想解决的问题完美的这个这个这个契合而不是依赖于有限个测试的这个输入输出对但是我这有限个输入输出对它其实是有它的有它的好处了你知道它能帮我什么吗它能够帮我去specification它可以帮我去做这个定义就是我比如说小俊你给了我一道一道题让我去就是去编一个程比如你让我做一个排序我把这个排序的题怎么样从一个英语的题转化成一个呃在我这个另里面的这样的一道题就是这个过程由于我还没有去解决出也没有去证明出这个另的这个这个命题我需要这些输入输出的东西来帮我去做一个验证的信号嗯嗯我在想因为科学他这个某某他是让很多不会编程的人也能够做了那你说这个math领域的curiousmoment是不是会让更多不会做这么高等数学的人也会做数学了呢我们可以用它做什么呢呃我们可以拿它比如说我们公司呃虽然呃有一些同学他们以前做过芯片硬件大部分同学没有做过芯片硬件呃我们现在可以去用另去呃证明芯片的性质所以他还是一个非常专业化的有一个专业门看的人去做这个事情不是不是不是我们我们公司的就是一般的软件工程师可以去拿另去去知道一个芯片是对的对我觉得我表达有问题是我想说的是它还是一个非常有专业需求的一个事情对吧因为这每个人都需要就可能更多人需要编编程但是并不是每个人都需要去证明一个芯片的性能呃我觉得就是在这些芯片的领域上由于可能说之前做不到可能之前的解法是这个smt这个就是基于smt的解法做不到呃我觉得就是在我们比如说每一天就是更consumer更更daytoday或者proconsumer的这样的这个市场上可以就是以下的一个想法就是你一边编程的时候你一边就是他告诉你整个编程不需要任何testcase已经完全解决了这一个coding问题这个我觉得会是有意义的我只是觉得在这些芯片这些领域上它目前就是感觉这个痛点更大比如说这个亚马逊在过去的他有一个世界上最好的自动推理自动推理团队之一没有AI的就是那个纯就是他有很多的这个形式化语言的这些专家他们花了三到五年去写了26万行定理证明的这个代码去验证他们的這個我實在不知道怎麼說一個用於去最適化CPU處理的一個Hypervisor一個工程的一個東西它的一個ComponentMemory記憶MemoryIsolationComponent我不太會說這個中文它去確定這個東西寫的是對的他花了三年人寫了26萬行這個AI沒有改善這些工程師的生活AI沒有改善那些必須要手把手教著幾千多個license的去驗證芯片的這些人的生活我觉得就是可以在这些领域上你会有更好的pricingpower你会有更好的定价格的这个这个这个空间作为我们这一个我们的公司这个这个这个提供方科技提供方但是我们觉得就是在更广广泛的每一个人都要coding的这个这个情况下我们会意识到verifygeneration的重要性就你会希望某一天在我要一个callaction要一个函数的时候他给你是百分之百不需要验证的函数嗯对所以这也算是你们之后可能会探索的商业模式我们觉得就是验证是我们最好的第一个市场这个市场会在什么时候打开啊你预计就什么时候是你们要做商业的时候我觉得我们就是我们还是比较坚信说就是一个是专注就是说这一些比较顶尖的这些科技人才要继续把我们的这个系统的这个能力往前变强但我们同时又觉得说可以去开始进行这些小的探索尝试其实某种程度上就是你如果就是有更多的资源然后能够有更多的人在这个团队里能做的事情就可以越多所以我们其实我们还比较某种程度上有点好奇心驱动的去想这个商业模式我们其实还挺好奇这个东西它能证明哪一些芯片性质电路性质它不能够证明哪一些它能够去证明哪一些程序不能够证明哪一些我们其实更关注就是它不能做的这些事情然后其实我们觉得去解决一个有意义的失败比很多个肤浅的成功来得更有价值嗯对有时候在我们讨论大圆模型的时候我们会说语言是模型的一个拐杖对数学是吗数学是然后没有之前大家把数学当语言了就是把数学当语言来做拐杖这个我觉得不对我觉得就是真的是要把数学变成另这个它就能够成为一个更更更更就是更另外的这样的一个很重要的一个拐杖所以它是独立于语言之外的一个关系数学跟语言应该是平行的关系某种程度上是的我们可以看到甚至在我们的系统里面就是更偏有一些问题更适合偏语言的解决比如说你列出这个提纲就是很大的一个一个一个部分的胜利那进度条就到了很多另外的比如说适合就纯粹的在这个形式化空间里面去证明它肯定是相辅相成的我们其实觉得挺有意思的一个点是一个就是一个形式化做得很好的一个一个一个模型系统啊他他能够比如说在这个芯片验证上做的比一个更多语言一点的要做的更好但是在一些其他的比如说这个通用的这个代码生成的这样的一个一个一个情况下嗯是我需要我也需要这个就是语言这一块的因为我需要理解这个用户他可能无法自我表述的很清楚的需求我们觉得把这个语言的这个部分和这个另的这部分放在一块最有意思你们是基于大语言模型的吗我们这个系统里面有不同的模型这些模型他们一般就是经过了大语言模型之后的后训练然后是以数学为主另为主以另为主就是输出都是另他目标是输出就是另代码然后另代码他自己带了这个程序语言自己带了这个验证的这个性质所以就是这个有意思点就是假设我我什么都不懂密钥学我完全不知道密钥学是什么然后你写了一篇密钥学的文章然后你把这个密钥学的文章就是就是你写的英语的这个文章里面包括一些数学符号你你打印了然后你给我看我我是看不懂我也不知道你写的对不对但是呢你这个密钥学的文章可以通过actionprover把它变成link然后我不需要看得懂我只要把它一跑我看到一个勾我就知道你这个密钥学的文章是对的嗯这是一个很有意思的点就是我们好验证过程对我们我们我们接受了我们盲目的接受了这个非常强大的AI会犯错误但是我们相信在一些领域上这些错误将极度的昂贵我们相信能够去做一个尽量perfectAI所以它能相对于就是在现有的AI之下它可以帮助解决幻觉的问题吗它对是帮助解决幻觉的问题解决所有的幻觉问题还是只能解决一个会有两种情况它要么就说这个事太难了我做不到要么它会给你一个正确的东西所以可能是语言是突破边界的那个数学是在把它往回收的那个约束它的对其实某种程度上这个呃我其实觉得人类比如说好的直觉是什么好的直觉其实就是一个配比配比其实就是幻觉和这个呃这个呃规律规律推导的这个patternmatching和这个呃这个幻觉的一个配比这个会比较合适其实某种程度上语言能够做很好的conjecture这个猜想家我觉得其实跟语言它会有一些很它会很需要借助一个很好的语言系统它可以帮你去突破这个边界然后这个某种程度上generation就是生成然后verification验证这两个就是一个来回的这样的一个一个一个过程但我们又有其他的方式可以去突破边界并不一定非是要语言模型比如说像FrancoisCharton和AlbertoAverino他们这一个数学发现AIformassdiscovery的这些工作他们是通过去找有意思的数学物品object数学数学的东西呃去例子去去去去尝试呃去找到一些直觉然后去把它变成一个猜想的比如说我有很多很多的图我可以让他在做一些就是呃local本地和global整个图全图的这些这些这些呃扰扰动我可以用这些方式去突破边界然后我甚至比如说另外一些方式做猜想我可以去呃我可以去看一下呃怎么样去做一个嗯可以做embedding然后可以去做一些其他的方式也可以去根据这个语言的这些相似性去反正有很多东西可以做但它确实是跟语言更相关然后而证明是跟证明其实跟两者都有关系嗯对你们接下来的一些呃就是想要达到的目标会是什么样的对當他承接提示向前推進的時候我們希望能夠我們也解決了一些研究問題我們解決了交換代數的代數幾何的然後代數論的然後還有是一個比較更理想數學比如組合概率意味的我們解決了這些問題希望能够选一些就是目前没有多少这个定义的这些领域比如我们希望能够看一下动力系统我们希望能看一下这种呃概率和随机曲面我们希望看一下没有这个基础建设的这一些地方我们能不能去解决一些问题我们想知道这个前沿到底在哪里我们本来不知道我们大概两两个月我们就把高中的那个基准期miniF2F这个也确实是一个比较古老也被打得千疮百孔估计不知道多少人训练在他上面训练的一个基准级就把它就是饱和了然后接下来饱和了普特南然后接下来就饱和了这个呃这个这个代码就是验证了这个这个基准级然后我们在研究层面上比较缺基准级说实话因为没有多少就是研究级数学的这个benchmark题不好找然后所以我们只能说找一些未解决的这一些问题在每个领域找那么两三个试一试现在希望能找一些完全看起来没什么希望的领域这个可能花的时间会长一些我觉得接下来就是就是这个A轮之后就是我觉得希望嗯我们可能会更多的往工程往研究上这里去去转换可能解决一些光是工程没有办法不足以就是摘起来的这一些这一些lowhangingfruit嗯对数学家的意义是不是在出题上他要数学家的意义很大程度很大程度我们的数学家的意义在出题上我觉得他们因为尤其你现在机器出题出的不怎么样刚才讲这个猜想家非常非常糟糕目前的表现所以就是确实需要人出题但出题非常难我们现在比如说我们要到哪里去找比如说八百道就是未解的研究研究题呢你一个教授有这个题你是给我们还是给他的这个学生呢就是这是一个非常复杂的一个过程所以我们也是希望能够去通过我们的数学家的网络去大家去看有没有题愿意给这个AI试一试吧你们想把它往哪个方向引导呀作为出题的我覺得他一定要就是滿足一個以下的這個性質就是他一定要就是robusttodistributionshift就是說不管你是哪一個領域的這個他都能做一點他不能是一個只做因為你要比如說只做歐式幾何那你就是一個几何几何几何引擎对吧但是你希望它能够做更多的领域尤其是那些目前没有基础定义的领域的数学题比如我想让这个东西去做一个代数数论代数数论里面的很多的东西其实都在这个MathLib这个图书馆里面已经这个定义已经打好了我只要就是我就很容易的就可以去写出我的命题如果你連定義都沒有譬如說在這個動力系統或者說是一些比較高級的組合它就沒有這個定義我連這個題寫都寫不出來這就是這個firstproof這十道題的這個挑戰我們很難去甚至嘗試的這樣的一個問題目前这个能力那你可以说为什么就像你拿AI做猜想你能不能让AI去写定义呢AI写定义的能力他们这个社区管它叫librarylearning就是图书馆学习图书馆学习能力大概的意思就是说让这个机器能够去搭出一个图书馆也就是说从定义包括上面的定理包括上面的去证明这些定理然后去衍生出新的定理加更多的定义这个过程是一个建筑理论的这个过程这个蛮难的就是所以说librarylearning是一个大家目前可能卡在这里的一个地方因为我也不知道这个定义我首先我很难给他验证信号我没有办法说这个定义是对还是错向我一个证明对这是一个一个点然后另外一个点就是是否是faithful的faithful的意思就是说是否与我这个人类给出的人类在数学里面已经创造出来的定义相同的如果未来这些人类的定义都已经对假设我们全世界的人类就是无穷猴子定理无限猴子定理我们什么都不干了我们就把人类的数学全部打成这些定义全部打进来假设就是上帝给了所有的已经存在的这个定义在另里面了就会出现一个问题就是当这个当这个系统要做新的猜想与新的证明的时候它会发现我可能引入一些新的定义能够让我的生活变得更容易但是在这样的一个情况下如果那个定义是一个人类没有写过的一个定义的话我怎么样能够保证这个系统的这些定义不相违背因为我可以定义一个图是好图然后过了一会之后就会发现这个东西可能会呈现一个悖论在这样的一个情形下其实是是比较棘手的嗯对就是这些都是比较就是呃比较远的的研究问题但是我们最近我们会在想的事情如果AIformath实现了AGI嗯你觉得它的标准是什么它能实现什么哎这个Demis他有一个非常DemisHassabis他有一个非常著名的就是说你把这个AI训练到一九一一九一零一九一啊看他能不能就是去发明发现广义相对论这是一个很有意思的一个定义首先我觉得我不太喜欢AGI这个词我觉得我们可能更是做ASI就是确实这个我们不能够去声称我们做的数学是general的數學它並不一定是那麼general的它不一定能帶來放寬性我是這樣想的就是我是這樣想的就是我們比如說有一個盤子其實我和之前的一個同學就是我和任宏宇聊過這件事就是中間你是一個點就是1加1等於2然後打印helloworld所有的這些非常簡單的這些任務在這個盤子我們當時還真在一個中餐館這個盤子的外緣是譬如說證明黎曼猜想找出治療癌症的秘方這個的方式的方法然後寫出一個像莎士比亞一樣的或者說像能夠拿諾貝爾文學獎的著作所有的這些就是人類的超人類的任務就是有一些前沿的这些实验室像OpenAI他们他们的想法是说我一点一点的我要做AGIA什么意思就是我一点一点的把这个圆环撑大撑大最终我到我接触到了所有的这个边界我们不是我们是我们从这儿然后往这个证明黎曼猜想这儿打我们就往数学这个代表数学的这一个超人类任务打打完了之后我们觉得它会发散出一个扇形就可能说这有个代码验证这有个物理我是发散出一个扇形我绝对不会覆盖到这个拿诺贝尔文学奖这里但是我会有一个比较大的扇形而我这个大的扇形在我这个B2B的这个市场上是有意义的嗯这是我们的一个想法所以我们觉得它是一个ASI其实人类的智能怎么定义AGI和ASIASI就是呃区别ASI我觉得是specializedsuperintelligentok对对然后AGI就是general当然S一般大家的意思是superintelligent对我觉得我觉得superintelligent就应该是specialized这是我的一个好题都为什么呀听起来AIS应该在AGI之上那比如说我我讲一个例子比如说就是我可能我数学还可以吧我我自己都不会做饭洗衣服就是就是就是以这就是人类的这个智能也不一定多generalok嗯嗯那有没有可能AGI实现的非常好他把你这个给取代了这有可能那我觉得我会更快嗯我觉得就我们现在看到比如说拿这个强化学习做到这个coding上我们看到了就是takeoff我们看到因为你拿强化学系能把coding做出来我觉得codeverification我们在做的是很重要的一环所有这些东西做好之后就是你有这个基于你有既有这个数学去做这些algorithm的能力又有呃如果把猜想能做出来你就能够达到一件事情叫做recursiveselfimprovementrecursiveselfimprovement是一个我们包括很多其他人都非常相信的一件事情我相信这个大家也很熟悉就是说你就可以持续螺旋上升就是我希望一个世界就是AIscientist人工智能工程師所以AI4Math的盡頭可能是一個AI4Math是一個我覺得AI4Math它比較哲學的一個看法是這樣的就是AI4Math能帶來很多的東西它能夠帶來你非常的smart它也能帶來你非常的right也就是說它既能夠帶來一個超人類的一個表現也就是我們可以看到甚至像OpenAI它們能夠做的AI4Math也做得很好但是另外一个很重要的是它能够给你grounding它能保证你的百分之百正确所以在这两个向线上再往上推然后我觉得AIforMath是我们公司的DNA或者Math是我们公司的DNA验证是第一个市场可能未来会有一个市场是AIforScience所有科学他们需要的理论finding可能未来还会有一个市场是最实化就是最实化就是某种程度上我们经常讲一个词叫就是diminishingreturn就是说我花了很多的力气我最后就只有那么一点的收益所以不值当但这个世界其实很多程度上并不是是diminishingreturn的反面是这种沉默性付出沉默性沉默性付出成本的反面是你最后花了很多很多的力气能够带来非常大的最后那一个mile会有非常大的一个收益某种程度上比如说能够去把所有的edgecase边缘性情况都覆盖的搜索引擎比如说像Google它就会赢得这个搜索的这个市场然后比如说像我们这个一些文艺工作者们他们能够就是好和非常好的区别是天差地别的所以在某种程度上我觉得像验证一个这种边缘情况很耗费很多的钱和人力很多这些资源和这种比如说最直化我需要目前大家花了很多的工业界的资源去探索这个小数点后一千位是什么比起小数点后第三位是什么雖然在一些其他的情境下小數點第三位比小數點第一前位要有意義但某種程度上我們是既需要這個median又需要這個outlier的數學我覺得給了這樣一種DNA我很好奇啊你們公司就是有數學家的公司和你那個競爭對手他不要數學家的公司他DNA區別會是什麼我覺得我們公司既要數學家我們還要一個他們不要的就我們我們要很多就是代碼生成的人就我們有很多就是編譯器代碼生成的這些同學我們其實我們相信多元產生智能其实有两句话是多元产生智能就是两句话我比较相信一个就是降维打击另一个是多元智能就是我们觉得就是这是为什么我们比如说你刚才说AI4Math的意义是什么AI4Math它其实在探索推理的一些非常难的问题它某种程度上能够与其说是泛化不如说是比如说你现在有你有一个吹脸一兆的这个自服串的这个爬虫的数据然后你很明显很难就是你基本上通過就是pattern就是這個規律的這個找尋能夠做很多的事情了你很難撞牆你很難碰壁但如果在數學這一個就是目前linkdata非常少的一個情況下你動不動就能夠遇到一些就是攔路虎所以你hit這些roadblock是更快的所以某種程度上我覺得我們做一個更難的事情希望能夠垂直下來給其他的一些領域就是某種程度上能夠去去降雷打击呃我讲这件事情的原因是比如说我们现在ActionProver能够生成一个20页的一个数学证明对吗但我然后我可以非常快的去验证一个目前在芯片验证领域是一个比较复杂的一个一个puzzle因为那一些需要的是一些比较可能说高中数学家呃高中数学学生或者初中数学学生会的每一句法分离讨论而不是什么like呃我想想啊不是什么numericalnumericallikesemigroup对然后这是我的一个想法噢我刚才说三个不好意思我说忘了一个就是三个这三个背景的人他们联合起来其实能有很多想法比如说AI和这个就是有这种compiler背景的人他们可以用一些方法去做很多的syntheticdatageneration去做这个合成不是合成不叫合成数据就是拿AI去生成这个Lin的data而不是靠人去打这个Lin因为你想就是我去找一个数据提供家比如说MacquareTuring这一些做这个数据商,他们可能就整个平台25个专家,然后可能链台打的不怎么样,那我这个东西是没有办法去大规模的去做的,所以我必须要拿AI去做,那怎么样拿去去做需要代码生成,我可以用Foxing,我可以用Repair,我可以用就是FailureCategorizer,我可以有很多很多的方式是这些人能够给我们的不同的视角。 AI和数学这里当然也有很多我可以想就是正向推理反向推理就forwardandbackwardconjecturing我可以去想很多一个数学家如何去有点像当时就是早期其类的expertsystem所有这些东西可以连在一起我觉得我们是一个idearich的一个公司就我们有很多很多很好的想法然后我们人不够去执行它所以我们现在在我们12月份的时候当时Ken加入了他第15号员工现在已经30人了嗯竞争对手多少人不知道,好像50到75吧还是比我们大,好的对怎么理解数学是现实世界的沙盒数学是现实世界的沙盒因为你既有验证的这个信号又能够有更规律性的描述更结构性的数据某种程度上比如说我们要在生活里咱们俩现在来想个猜想然后咱们俩再把这个猜想证明我好像只能想到一个数学猜想和数学证明不然的话我们可以说猜想一些生物的东西然后来一个实验室去做一些动物实验这个任何与现实世界更有关的这一些验证的过程其实可能会比数学的这一个比较简明的这个沙盒要困难和复杂的多也就是我为什么非常就是respect我的一些朋友们他们在做就是AIfor科学的公司比如说PeriodicLabs连Fides他们在做然后原来是叫FutureHouse现在叫Edison这个SamRodriguez就是我们MIT的这个校友他们在做就是一个AIscientist很多很多人在做各种各样的这一些这一些尝试但是就是如果你想要很快的一个验证然后你又希望又能计算又有逻辑我觉得数学和代码是好的选项嗯对AIforscience和AIformath不是一個overlap的賽道,對嗎? 不太是。

AIforscience他們其實很多在比的是這個iterationcircle有多快。 因為你想如果他們出現了weblab出現了實驗室我身邊很多朋友有各種各樣的實驗室我的這個知道這個LilaScience這個公司Jeff他們還有GeorgeChurch在的那個公司他們有個什麼robot實驗室機器人實驗室這個聽起來非常的自動化但是他們所需要做的前期的投入是很多的LiamFides他們最近這個實驗室又搞起來又有其他的一些實驗室像MajraMichelleLee他們都有很多的這些他們是一個賽道我们某种程度上如果他们有想要我们解决的一些理论上的一些问题我们希望能够帮他们解决但我们某种程度上只停留在一个数字世界我们不走到他们这个实际世界去但是你可以帮助AFMScience对你也可以帮助大学模型其实你们是一个拐杖是一个工具对对我们觉得也不能算是我们是拐杖和工具比如说我们可以去验证他们生成的代码来帮他们减少幻觉这个蛮重要的我们可以去我希望的一个世界是每一个就是物理学家他们都有能够找到他们的理论物理学家就是他们都能够每一个神经科学就是做一些真正动物实验的人都能够找到他们的这些理论的这些计算神经科学学家而这些过去数学家们他们停留在比如说自己的学术圈子里面他们可能去很少的一些合作他们很少去与这些应用科学家进行合作我觉得未来就是希望能够Axiom的AI数学家能够去帮这些AIforscience的这一些科学的这一些探索去解决一些理论上的问题然后他们可以去进在实际的生活中去做验证你刚才说了很多AI4math它的验证能作为验证的手段对那它能有一天像一个天才如果你走形式化证明你就有验证如果你不走形式化证明你就没有验证你们现在走的是形式化证明我们走形式化嗯那如果不走形式化证明它通往的是哪里呢不走形式化证明它可能是我觉得可以去尝试我覺得就是他可以嘗試一些怎麼樣做通用的推理吧我覺得AIformath有可能有一天像一個天才型的數學家一樣提出非常好的問題有非常好的直覺他能成為那個創造的人嗎这就是这个最最难做的这个部分但是我觉得可能我们和那个竞争对手的一个区别是我们打算做这件事他们不太打算哦对他们好像直接要落地了对他们落地成什么就是就是他们打算直接做这些商业的这个东西他们觉得imo金牌可能就是就是这个终局了就是可以就我们还是希望我们真的能希望把猜想做出来嗯这个我觉得我们目前有很多的一些试验和探索然后也碰了碰了不少碰了一鼻子灰对但我觉得这个碰了什么一鼻子灰就是就是有做不出来的情况比如说就失败了你这个失败到底是当时我记得这个失败发生的时候我们的这个证明家这个还做的不太好所以我们分不清到底是哪一块出了出了问题呃有很多的这些想法都可以去做但是我觉得我们要做这个猜想之前希望能够把我刚才说的这个核心科技二也就是把这个转化能够做好这个autoformalization把这个自然语言倒令这个转化我们希望能做好我们觉得能做好这个的话能够有更大的既是一个能拿更多数据的手段又本身能够对证明做做一个很好的一个一个帮助然后我们才会去做这个猜想嗯当然当然我们现在可能也在做一点但是就没有完全的rampup没有说整个公司打猜想嗯对猜想其实是数学最有魅力的地方是吗猜想其实是就比如我作为一个数学的一个一个学者我我是很难我很难去提一个好的猜想然后比如说给到比如说假设说现在有一个readingcourse有一个本科的一个大一的同学希望能拿一道题对吧作为一个readingcourse最终的一个我觉得我很难给到这样一个题就我觉得需要猜想所需要的数学能力是蛮难的所以我们特别高兴就是Ken能够加入我们其实他是他是非常他是猜想家他是高产的猜想家他跟拉玛努金的关系是什么我听说的故事是这样的就是首先故事一就是他的父亲是当时一群要就是筹钱众筹给拉玛努金修这个在印度修这个雕像的数学家之一他的父亲是一个非常非常非常出名的著名的一个一个杰出的一个数学家也是做数论然后当时是印度政府说是要给这个拉玛努金立一个雕像但最终没有实现於是這個拉瑪努金的遺孀這個女士她就給這個拉瑪努金的合作者世界各地數學家寫信於是他們就是一起去做然後他還回了信就是建成這個雕像之後所以Ken的辦公室裡現在還有一個他父親給他的這個留下來的就是拉瑪努金呃呃呃的一双写的这一封信然后另外的故事二就是当ken他是一个我印象中当他是一个本科生他好像是在芝加哥大学他当时呃就是有很多的社团活动然后可能科业呢也没有特别占据占据他所有的时间所以他的记点也不是特别好然后他好像高中也没有毕业反正就是呃是吗对反正他就是一个非常叛逆的一个少年然后他的父亲就是拿拉玛努金的故事勉励他就是任何时候开始也不算晚你不需要像你的这些已经上了多少数学课的同学一样你才能够做数学你完全可以自己现在去追赶上来于是他进入了他的这个数学博士项目之后就开始非常努力然后就是做了很多非常好的数论研究对,Kent的父亲也是前不久今年年头去年年底去世了所以也是非常值得纪念的一个一个数学数学title之一他的他的兄弟们都非常的都非常的就是他来自一个数学家他他来自他的他的两个兄弟一个是著名的小提琴还是中提琴某个提琴提琴家另外一个原来是密歇根大学的校长对他和拉玛努金都被认为是那种直觉型的数学家对不对我觉得就是拉玛努金是更更尖锐的直觉型解题型然后而Ken我觉得他是擅长他提出猜想的方式是连接很多不同的视角他是一个发散性思维的人但他不是那种嘿这就是一个公式这个东西一定是对的那是拉玛努基对所以我在想如果AI做的是验证的这个事情是形式化数学那他其实训练的是一个更能验证的人而像拉玛努金这样的天才他能够被AI训练出来他会不会是两种类型这是一个很好的问题大家说拉玛努金为什么就是essentialAI也就是当时这个transformerpaperattentionisallyouneed你需要的只是注意力这个注意力機制這一篇文章的作者叫Ashish他有一個公司叫EssentialEssential是做pretraining先訓練的一個公司他們先訓練的一個模型就叫拉瓦努金人家說拉瓦努金的那種渾然天成那種直覺其實是有可能是預訓練的產物所以我们现在并没有做预训练我们现在主要做的是后训练我们有一天可能会做中训练但我们可能很确实你说的对就是拉玛努金并不一定是一个能够通过后训练诞生的一个一个一个一个数学家他是怎么预训练的他就是我不知道他不是他好像是有很多他的这个宗教仪式然后他呃原来是会计然后他在喜欢电电影里面反正是拍他有时候祈祷的时候能够看到一些数学的这个其实我觉得对对对这个这个感觉没有办法就不是说我们能够后训练一个ai能够做做到这样的但是但是拉玛努金到了这个剑桥之后他接触了就是证明他知道如何写证明了然后他就使得他的这个数学的这个影响有有更指数级的爆炸他有更多的更多的他想到的直觉他可以进行证明然后变成了新的直觉我们可以训练这个AI去证明所以说还是会对这个东西有帮助的哦小野肯是后训练中训练还是预训练的场合他有说过这个这个不知道我肯定不是预训练的成员而且你看他的预训练好像不只是数学对就我们现在大家的预训练也都是什么都有目前其实预训练我觉得能够去往下去就是做的能做很多东西我觉得预训练有大量的可以基于数据能够去走的研究方向但是只是某种程度上也没有大家没有在做比如说你觉得有哪些可能呢呃我觉得就是在就是你这个就是其实就是一些数据的一些bet我知道的就是怎么做的可能涉及一些其他公司的一些这个这个这个秘密所以可能不太能讲但我们也没有去很深的去想先训练的事比如我做预训练对吧我们不做我们我们没目前没有做的打算为什么你们不做预训练太费钱嗯然后我们也觉得大部分的另的这个东西可以从后训练甚至是我们会做一些我可能会做一些没吹你那有些人可能就把中训练化到这个预训练里面了对嗯其实我们确实是认同说是有一些基本的这个能力是需要通过预训练中训练来来来来来来来提出的我能理解你们是一个创业公司你们要做的是AIformat那那些大厂OpenEyeDeepMind包括DeepSeek自己他们为什么要做AIformat我听说的就是比如说Gemini就花了非常非常多的的想法在这个域训练在域训练上面然后他们的这个甚至说他们的甚至说有些有些公司会希望从LinkData里面去把希望能够买LinkData去做一些一些域训练嗯就我们现在的这些形式化的数据甚至可以更多的在于训练他们要去做什么呢他们为什么要做他们他们是要做一个垂直的专家还是要做一个他们可能他们就是AGI啊哦他们是general的就AFM是一部分AFM并不是每个公司有些公司没有对对目前我觉得比如说OpenAI走的是Informal这一个他其实是KevinVile他的个人的科学雄心啊就是要做啊科学发现然后嗯我好像就是DeepMind里面有几个队伍同时在竞争做AIforMath有一个formal的队伍有一个informal的队伍嗯XAI5不太确定有然后Anthropic我觉得他们有但是呃只是作为只是作为帮助他们提高推理推理效效果的就是说他比如说我有一道题吧一道数学题他先把它informal变成formal然后在另一面验证完之后再回来提升他的推理分数但是并没有把这个作为一个一个专注点其实我觉得作为这一个如果我是这些就是玩家之一的话并不一定会去做我们现在做的这件事情的原因是我一样的人才的这种这种高密度人才的队伍我可以把他们再继续在代码生成或者说在一些更鸿海的一些目前竞争咬得比较紧的的领域去去去去去做的更深去把他们的护城河住起来然后完全可以就是和我们或者是我们竞争对手这一些做的还可以的这些创业公司去进行去成为去合作然后这有点像比如说OpenAI他们就是会在搜索这一块会CallXR或者是CallParallel这些搜索做的比较好的公司所以你们这个行业现在目前是蓝海并不是烂海我觉得这个东西是嗯比较难嗯嗯比较难不太像烂海其实也大比如说就像是机器人的foundationmodel一般比如说pi和skill的两家然后我觉得现在就是创业上就是我们和我们竞争对手两家就是估值也差不多总共融的也差不多一个新一点一个就是比我们两年前差不多是这样的一个状态对你来说挑战是什么呀? 执行的速度与学习的速度我们现在会有一个对我个人来说我执行的越多我学习时间越少这是一个非常痛苦的一个过程就是你我以前可能说我每天有多少的时间能够用来阅读我现在可能少了这些时间但我又有那么多的事情需要执行所以某种程度上这是一个挣扎然后这个挣扎容易就是会我相信就是我们其他的一些很好的科技人才他们有类似的researchengineeringratio的一些挣扎就是一些tradeoff我们希望能够执行速度很快我们也希望探索商业模式的这一些从一个技术的角度去探索从技术和好奇心的角度去探索商业模式但同时我们要做的这些事情确实是挺多然后也也也困难还挺大的所以我们就是担心这个速度我这是我觉得最大的一个苦惱因为我们现在是我们现在是呃七个月成立七个月的一家公司我觉得期待也由于这个A轮吧可能也期待比较大我们还是希望能够呃还是能够做长期主义的事情我们有点怕说是一个是怕执行的不够快另外一个是怕由于要执行的快导致焦虑导致这些就是方向上出一些战略错误嗯对对你来说实现AIRFORMAT的终点更重要还是说成为一个更成功的商业公司更重要我觉得作为一个就是founder来说你对你的这个员工和早期团队你负有责任所以这不是一个某种程度上我觉得这不是一个这不是一个纯科学项目就是我们必须要成为一个一个一个一个能比较长的一个一个一个企业一个公司但与此同时我觉得这个公司的DNA就是登月其实我我非常温顺对我非常喜欢温顺他们这个名字天哪这个名字简直是太好了这是这个公司的DNA如果我们就是太去逐利商业化的话我们会其实是一个平衡然后我们可以看一下我们竞争对手的公司他们公司的起源其实是因为Robinhood的这个founderCEO他可能现在还全职在Robinhood他可能希望有另外的一个让他感到比较有激情的生活有热情的这样的一个项目所以他们可能在早期的时候更讲这种科学雄心我们认为是我们认为是科学雄心然后但是我们我觉得理想的现实主义者和现实的理想主义者两种都是不错的不错的不错的这个这个这个落点但是不能是太远就不能是对有一天你们公司如果创业失败了你觉得可能会是什么样呢是因为什么嗯呃我觉得这个事情其实挺有意思的就这个事情它的结果一定是极好或极坏就这个公司其实没有一个在中间的一个可能性要么登月成功了要么登月失败就是登月成功登月失败某种程度上为什么说像SpaceX呢要么火箭发上去了要么火箭坠毁了可能火箭要坠毁几次才发上去可能每次都差那么一点其實這是為什麼我覺得就是像伊隆·馬斯克他作為一個就是企業家尤其你看他早期的時候還是一個非常銳意進取的一個值得學習的這樣的一個企業家的一個模式比如說好幾次就是憑死對嗎他的公司也只能兩個留一個但是就是他很堅定的說Bose永遠是魚與熊掌都要兼得这样比如RayDalio在principle里面也是这样我自己也是这样的一个认同我觉得这个公司是一个binaryoutcome然后我觉得如果我们是失败了或者我们很成功其实都是有可能发生的事情如果失败了你去干嘛这是一个非常好的问题我自己有一些个人的雄心看吧当数学家我觉得我可能会去希望看一看我觉得我那一年的神经科学的学习的一个心得就是我们基本不理解人脑我们完全不理解人脑我可能会希望做一些跟人脑相关的事情不不是跟人脑就是跟神经科学相关的事情可能是动物脑就是我可能会我可能会希望看一下这些嗯我觉得就是brainandmachineinterface的这个vision目前的implementation都不太足够就是人机交互的这个目前的选项我觉得太太不理想嗯你今天怎么看待硅谷这些模型公司的竞争啊不管是这些大的模型公司还是这些new了我前几天还在跟一个就是我的一个XI的朋友在讲就是其實為什麼說為什麼說我最後不想去做一個就是金融或者說是一個量化交易員呢你會出現一個問題就是你的你的你的盈餘輸是一個短期內能夠決定的一件事情我觉得这个事情是就像PeterThiel讲的就是这个我是比较激进的垄断导致创新竞争导致平庸这种竞争会导致平庸会导致没有一些长有一些很有长远想法的人他就要自己出来做做NewLab这其实NewLab的产生就是因为好奇心与创造力是我们人类的基本需求这就是因为可能说是在一些前沿的一些大的公司里面无法去做这一些满足他的burningpassion的事情他就要出来然后我觉得可能是一个很有意思的点就是刚才说到这个好奇心为什么是人类的基本需求可以我们可以假设一件事情就是actionprover非常的成功或者說是我們競爭對手的這個他們的非常成功反正就我們中有一方非常成功然後所有的數學題你給我一個千禧年問題我這個AI就把它全部解決了這個時候還會有數學家嗎這是一個非常值得去思考的一件事情我答案就一定会有就是你给我一个一百万行另代码的一个我一定要去看里面是怎么做出来的你你不让我去看我都会去看这就是人类的这个好奇心的体验体现由于这个证明最后被产生的方式这些去看懂了他的数学家们又会有新的猜想新的想法这就是整个这个发明发现的这一个这一个循环其实就是就是然後就是AI做了可能AI做了這個發現讓數學家更好地發明然後然後這種好奇心和這種探索的這種願望意念是一個我覺得人類無法被壓制住的一件事情所以說不管是現在是10million1億美元的大包也無法去壓制住這一些青年研究者的這個好奇心所以他們就會去做出来我们看到做出来多么多么有意思的东西比如说StefanoOrmond他们做了这个DiffusionModel更快更好的这个推理模型我们可以看到就是比如说就是Periodic我们第一次把这些顶尖的这些AI人才就是去在一个就是现实世界他们要做这个MaterialScience这是一个非常有意思的一个一个一个方向他们不怕这些Messy的这些Data然后他们其实就是然后比如说我们看到有recursive他要做AI与这个这个硬件之间的这个AI提升硬件硬件提升AI这是非常有意思的一些方向我觉得嗯这其实是一个这背后是一个基本作用力这个基本作用力就是人类的好奇心然后我觉得可能最有意思的点就是有些人说现在是一个泡沫吗还是说现在是登月就是你有一些公司他成了他就登月了然后有一些公司登月了人家真的试了很努力大家真的是每一天96一块去朝那个梦想努力结果没成那就是泡沫其实我觉得就是我特别希望的一个一个环境有点像我我也知道说有一些好的学府的一个环境就是不怕失败MIT有一门课就是learningtofail你如何更好的失败就是但当然这个每一个这种登月项目的失败它都会在资本市场上会掀起涟漪对吗我们会從這個就是私有市場一直到這個公開的市場會有連鎖的反應你有可能說這是非常不負責任的就是為什麼這個一些可能說PensionFund一些大家的退休資金最終通過好幾層的投資到了這個私有市場去給這一些有想法的研究者去滿足他們的好奇心呢這是一個我覺得很公平的一個問題但是就是如果说这些好的有想法的研究者不是由于他们自己的这种虚荣心或者说是我自己要站山为王不是由于ego而驱动的而是由于使命而驱动的所以导致他们不是碎片化的好几个比如同样的一个问题吧就是八个尝试他们真的就是在一块了他们从不同的背景不同的技能不同的这种不同的对于这同一个理想的解读聚起来了去朝这个东西我觉得这就是一个比较比较legit的比较比较靠谱的一个尝试我能理解这一波的Neolab他们都有different的信仰都有不一样的bets对那当有一天他需要跟这些大的frontierlab竞争的时候怎么应对这个竞争呢刚才我们说了你们AF和MAT之间的竞争对吧对那当你要遇到OpenAI你的竞争内容是BigMind的时候你怎么竞争对我觉得这是一个非常好的问题我觉得首先第一个就是会有一些结构性的问题会导致如果说他们需要一个单位的创新是需要有多少单位的资源的而这个比例的话在一个早期的创业公司是非常高效率的这是第一点我觉得我们公司就是在做的一些事情我觉得可能在另外的一个环境会更难的去达成也就是为什么许多人从脸书来到了我们这个公司的原因然后这是一个点然后第二个点就是其实吧你作为一个underdog这个黑马你好像除了这个效率之外还有这个人才这个之外人才是人才密度因为毕竟他们会有更多的人才你没有什么资源能够和这一些大的这些玩家抗衡但同时这更有意思的一件事情上是OpenAI曾经也是对着Google的那一匹黑马他也是那个就是在Google要把Illia就是最后counteroffer抢走的时候焦头烂额不知道怎么办的也是那个曾经一度发不出工资的这样的一个一个小玩家所以这其实是一个很有意思的一个点就是我觉得历史的钟摆来回摆动它就是大家螺旋上升但是又有很local的这种扰动某种程度上是有thereisalwaysaway这个东西我没有办法证明thereisalwaysaway就是你得信嗯对然后信的可能就是喜欢加入早期创业公司的这一批人譬如说HumansEnd的这一个公司最近融了很大的他们的这个cofounder是Google的第七号员工嗯他到了现在的这样的一个人生阶段仍然认为好奇心是他就是所拥有的最珍贵的东西嗯值得他倾家荡产嗯也这么说我能理解很多包括我去跟赛宁聊他们其实有different但他们甚至是一个anti硅谷的收集了一波anti硅谷的这个派别他们也非常反感这种剧烈的红海竞争然后觉得也阉割了研究员的创造性对其实是我是这样想的就是嗯可以就是就是在一段在所有的这些就是local的扰动之后你看到的整个的这个宏观的这个局面是什么样的一个竞争的结果就是能力在飞速的上涨另外的一个结果就是好的且快速不只是好的好的且能快速驗證是好的的東西被就是被做到最scaleup的一個狀態但是完全有一些可能可以時間長一點的東西沒有被實現這是一個機會成本對但所以說競爭它也不能說不好它就是確實它這個讓我們人類在這個AI的這個進步在非常短的時間內達到了一個一個非常高的一個一個一個進步速度嗯你刚才会说到你的自己的自我奖励机制从从团队里面获取这种能量变成了从事情中获得能量现在呢你是从事情中还是从团队中现在现在我是从事情中嗯现在我是从事情中然后但是我觉得团队是一个很好的一种他会给你一种安全感他会给你一种就是你有一个你有一个你有一个能落地你的脚还在地上他让你觉得grounded但是你事实上能够让你就是breakout的那种那种冲动的那种能量有可能是愤怒有可能是有可能是悲伤有可能是就这种卯着一口劲我就要去达到一个一个让我们这个队伍达到一个什么样的一个一个一个目标的这种的这个能量他不由团队中来他有事情的本身来嗯对那个让你最本人那个是对终点是什么我觉得就是呃这个事情就讲起来就是有一个莱布尼茨他有一个想法他叫做universalrepresentationtheory就是说所有你能够表示的这句话听起来很怪所有所有所有大部分你觉得能表示的东西你都能表示就是我觉得我目前非常期待一个让推理能力成为最顶尖的推理能力成为一个默认状态的一个这样的一个情况然后且是能够自我验证的推理能力这是我目前个人的一个理想其实就是有些时候就可能说人一辈子他能剩下什么有一些数学家他一辈子解决了一个非常困难的问题他被這個問題就是人們因為這個問題記住他他可能這個墓碑上就寫著他解決了這個問題一個人一生這一個問題你想這個加羅瓦21歲他就覺得我就掛了然後拉瑪努金他是因為這個營養不良還有各種各樣的身體疾病也早也三十幾歲就掛了人类要多少人出一个加罗瓦多少人出一个拉玛诺金然后你如果说是能够去用AI去复现这样的一种数学家然后你又有那么多已经存在的数学家能够与他互动然后去有新的这个这个这个就是呃对吧就是就是我也不知道中文怎么说他的意思就是说当你把一个呃一个工具变得能够你做出来让他更便利更普遍的时候就会有更多的用处比如说我最近我们公司好久就是第一次找了一个找了一个能够帮我去处理一些呃每一天就是杂事的这样的一个一个一个一个同事他来了之后我们就是一块做的杂事反而变得更多了就是这其实就是指王是paradox就是这些科学家这些物理的生物的化学的他们能够与这个AI加洛瓦或者說是所有的這些數學家總和他們能夠有多少的科學的理論能夠被被被被被發明發現就數學家們和這些AI數學家能有多少數學的就是基礎數學的這些東西被發明發現這其實我覺得這是我的一個一個你想从算盘到会计师就是当时是商务贸易从这个微积分到这个物理各种各样什么力学然后是thermodynamics就是然后然后到到到工业革命对吧然后从这个当时一个叫Babbage查理斯·巴贝奇他这个能够去算这个log对数算的更快的一个Babbageengine就是电脑的前身当时在哈代写我作为一个数学家我是一个数学家的道歉这个mathematicsapology好像不是这么翻译一个数学家的独白他就说我这个东西反正也没有任何的实际价值后面就有就密码学就有对吧我们看VictorMuller他是一个他也是Shubo当时的同事也跟Axiom很多的互动这个椭圆曲线基于椭圆曲线的密码学密钥学的就是泰斗之一的这样的一个人物他是一个纯数学的一个背景然后就是在CS看了一眼然后就看出来了这样的一个理论这对于很多纯计算机的这些同学们有非常大的一个价值这是终局但是有人家说这个终局之后怎么办呢这个就不知道终局之后我觉得还是要我觉得其实就是钟摆的摆动又会卡但我觉得AIformath没有像AI模型被scaleup一样被scaleup而我们希望能做这样的一个人这样我们能知道天花板在哪我们可能又能回到research然后又能这样就是钟摆的来回摆动我见过很多的70后80后和90后的CEO你应该是第一个0后的CEO是吗我不想就是画这种代际但是我还是很好奇就一个0后而且是女生的公司会和之前的这些公司或者是就有任何的不一样吗你觉得特点会是什么呢我这个其实是非常好的一个问题因为我自己最快乐的一个状态绝对不是CEO的状态我自己最快乐的状态就是我能够当一个researchscientistintern为什么是intern呢就是这个我说的话如果比较愚蠢这个大家认为是正常的这是我最快乐的一个状态我是真的想做这件事然后我如果能够有另外的一个很明显我可以加入的一个地方我就会去加入它而不会把这个事情单独做起来所以我这是我的一个舒适的一个状态嗯所以我我不太因为事情本身而创业而并不是说你想当一个创业者而创业我我特别不想当一个创业这个能理解对对我反正就是所以我不太稀有这个可能大部分对所以但但也有时候有一次闹一个笑话就是我有一天特别就是想做这个呃Benchmark我想做一个就是好我我不是说吗那个基准级就是到博士级别就很难搞我当时就把我们办公室有那个数学背景的同学们我就是说我想搞这么一个东西我也不知道就是现在搞这个是不是优先须上是对的你们都是搞数学的你们要不跟我一块我们分一下就是你负责这个领域你负责这个领域每人找个二三十题然后完了之后我们这个之后我就后面就被我们那个一个比较元老的工程师就说了说你让这些这个实习生的同学们就是还有这些比较年轻的工程师觉得这是一个非常重要的一个任务这和优先叙事是相斥的我说为什么是重要的任务呢我说这不就是一个side一个hobby的一个project吗他们说但是你是一个CEO所以你跟他们讲的时候他们就会觉得这是一个正儿八经的一件事我真的要去把这个当做我的前几件事情去做从那以后我就我就更handsoff了所以就是这是一个非常非常有意思的一个一个一个事情嗯还有什么不同吗你觉得可能和我觉得就是呃我觉得我我觉得我做这个ceo的一个好处就是这是一个technocratsrule的一个公司就是我们的技术人员他们是整个公司的主干且和定向和锚点就是他们有可能由于我并没有一些stronglyheldbeliefs所以导致我觉得我们就是很多ideas都可以被由于我没有一个特别我自己其实我有我有一些特别坚信的方向但是很多其他的一些就是很lowlevel的一些东西就是一个bottomoftheculture所以我觉得这个公司的文化是一个是一个比较比较有意思的一个就像一个呃比较呃texar梦工厂对你们公司的会议室好像都是用数学家来命名的有什么有特别的就就如果你想如果这个梦工厂这个或者迪士尼的这一个CEO是一个已经假设ok一个梦工厂的CEO已经是一个就是拍过多少个这个的好莱坞或者迪士尼的一个导演的这样的一个人做CEO这个地方就成为不了梦工厂为什么因为他们会觉得这个人是对的应该听他的所以我觉得反而是这种bottomup的这种这种culture对创新来说是最好的需要一个实习生对我觉得实习生挺好的我非常愿意给Action当实习生你们的会议是有任何有意思的吗有对这不同的名字他们就是叫做高斯对吧高斯庞加莱希尔伯特Loveless还有呃图图林这个中间大家差点打起来因为怎么命名为什么差点打起来就大家喜欢的数学家不一样嗯大家说你你有了这个你有了图灵你没有church哎这个不行然后你有了这个loveless你没有nother不行就是反正我们还接受到世界各地的邮件说为什么不把Emilynother作为一个一个会议室我们说我们不好意思我们目前只有五个会议室后来是怎么选择的取舍的嗯好像是先就是我也不知道最后是怎么取舍大家反正就是还是在slack里面经过激烈的争辩大家认为庞加莱希尔伯特高斯这些都是polymath他们在数学里面不只会一个领域他们会好多好多领域所以所以拉玛努金就是这么落选的他只会数论呃所以所以说就是大家要找这种就是我们觉得要是做一个AI数学家希望他什么领域都会没有distributionshift这样的一个问题所以要找这些polymath图图灵是跨世纪的啊当然这个shugo他也liehisbodyonthetable说如果你不给其中一个叫图灵我就走了我说行行行那就是图灵然后完了之后我们希望能够有有有一个女数学家然后这个女数学家我们觉得loveless其实就是在babbageengine这里也也不错嗯是其中有你的偶像吗我的偶像是高斯他哦他在也对对他在哦对对然后龐克瑞其实庞加莱和弗朗索舍尔汤他们家里是是就是法他们都是法国人然后他们家里那个族谱还是连着为什么高斯是你的偶像为什么高斯是我的偶像就是他是就是解题里面的天才对吗他这种他这些故事什么正时期持规划求正时期变形然后包括就是我喜欢数论然后高斯在数论里面的这个都是非常基本的就是fundamental的一些贡献高斯比如二次互反律然后各种各样反正高斯在初等数论他是他有点像是我学数论刚开始的时候初等数论里面的好多高斯所以然后又他又是一个年轻数学小王子然后反正就整个我还是挺喜欢高斯的对如果可以穿越时空和历史上的任何一个数学家共进晚餐你希望选择谁你想问他什么问题我觉得就是去跟儿童共进晚餐的话他给你讲的那些描述毕竟是组合学你晚餐这个就是table上能听懂然后儿童是有又是那么一个就是peculiar非常古怪的一个一个有趣有趣有趣又古怪的一个性格古灵精怪的我觉得跟儿童会共进晚餐会比较有意思另外一个我觉得我觉得跟Grossendick共进晚餐的话如果不是我的话就是说另外一个人他跟Grossendick共进晚餐应该意义会很大因为但是我这个代数几何学的不是特别好所以就是跟Grossendick容易浪费这个宝贵的机会嗯你看当你说到这些数学家的时候他们都是这么有趣的人对那如果有一天AFOMath能做到所有数学家能做的事情会不会是一件很无聊的事情我有想过这个点我觉得我其实我一开始觉得是一个非常就是非常非常我不希望让这个局面是一个非常遗憾的局面因为可以说数学家们他们之间的这种友谊他们的合作的这个关系他们的文化社区是一个非常有意思的一个一個文化就是比如說有一個數學家生日大家會給他辦一個生日的一個峰會然後所有他的學生他的合作者們去輪流去去去講一個這人所做出來的數學的貢獻或者是一個跟他們合作的一篇一篇文章我曾經就是作為一個碩士生在這個牛津去過這個HeathBrownRogerHeathBrown的生日峰会然后像BenGreenJamesMaynard他们都在那里然后当时就觉得是非常的感动就是这是一个非常好的一个一种传统然后所以这人的这一个元素我觉得在数学中它永远不会被磨灭我覺得AI會把就是數學的很多證明可能能夠幫數學家們去很快速的解決但是這個猜想然後以及直覺以及構造以及這些方面我覺得數學家們仍然會有非常多的樂趣然後他仍然是會他們會成為智力的燈塔所以我们刚才说的那个当然这个也不一定我们能解决这个当然是有的时候你做做梦想着自己能能把它解决了会不会反而是一个呃不太好的一个一个一个一个一个一个添加因为比如说这一些数学家们非常珍贵的这一些legacy他们的他们的他们的对对但是呃后来觉得哎他们他们就是会有更多的问题他们会难倒AI像他们已经在难倒AI一样做基准级他们他们会永远永远是智力上的挑战以及打击这种互动应该会很有意思所以我们刚才说那个问题拉玛努金和做一个验证的AI对他其实还是偏这边对吧他验证他并不是那个天才型的选手对这个我觉得直觉就太难做了我觉得真的直觉可能5到10年有可能对但是我有一个很我有一个比较又有一个比较激进的一个想法就是我觉得大家现在如果看有多少解析数论里面的问题是被一遍又一遍的在一包很标准的证明方法里面去抽这个证明牌就是一个卡牌一个卡牌一个卡牌就这么重复的熟练的去运用比如说我看这个MajorArc,MinorArc,HeartyLittle五元法这个这个circlemethod就能解决一些一些呃一些就是bonding的就是上线下线这些这些方式解决一些呃一些概率法解决一些然后比如说你去上seaftheoryseaf筛法又能解决一些筛法也在被就是有一些人他们不解决任何问题在提升筛法能做的筛法作为一个工具我觉得就是已经能有的这一些工具能解决很多很多的问题然后我们会说一个人直觉很好可能是他很快的能够想到怎么样去重复的我们现在讲的这种直觉我可能讲的是说给大家一个完全不同的一种一种一种一种方法和机制这个我觉得是5到10年嗯你有过一个说法就是说热爱数学就是看到了上帝的面容为什么会说这句话我是这么觉得的就是我很小的时候就觉得说有一些基本的这些真理然后我觉得数学家科学家他们存在的这个意义之一当然就是去把这一些东西进行发现和探索其实这是我16岁我曾经写过一篇文章我当时至少是这么想的然后后面就是林耀开这个就是创立这个action的时候就是不是说老跑步吗早上斯坦福那有一个那个就是教堂叫memorialchurch就是纪念教堂然后如果你去从那个就是我们PaloAlto这边往那跑然后如果平常我都是绕着跑因为就是特别晒那一天就是往这个草坪底下去跑然后就是突然我就在那个教堂的下面了然后当时那个阳光也特别好然后那个教堂上有壁画有天使十字架其实有那么一点spiritual的一种感觉一点灵魂的这个感觉就是觉得可能说如果那个就是一个人的这个墓志碑上可能印了一个他曾经证明出来的这个事情是他的智力遗产那么如果能够让这个东西乘以一亿你会不做吗可能不会所以当时有这么一个想法当然这个我觉得也自己就这是一个出于ego的一个想法就是说我我可能说想我这个公司能够去作为这样的一个AIformath的一个unlock这个想就是我希望登月也希望登月的是我们这个肯定是出自于一点这种这种ego或者是就是自私的雄心壮志但是总体上这个事情我是非常希望它会它会实现的对就算我们是失败了可能要谁其他人登上去了也是一件好事嗯虽然你现在还很小问你这个问题好像不太好但是还是想问你希望你的墓志碑上写的是什么呢哎呀你是希望你是一个数学家还是一个别写就是其实我是一个比较就是觉得体验比较重要的人就是我反正要活过了我也有体验这个就无所谓我都不知道我要有什么墓志碑不重要就不重要对你会希望你自己是一个数学家吗呃也不重要不重要我觉得我我曾经是觉得很重要的这是这是这是这是我曾经觉得就是我一想到我可能就没有办法成为一个数学家我有时候一开始我就还哭就是我我还是一个比较比较比较emotional有时候会有这种对对对那个时候是是这么觉得啊然后后来觉得其实就是我想当学徒对我记得对其实就是你要非写一个什么就写学徒就是我想去呃在尽量多的一些智力领域上能尽量多的去学一些东西比如说这为什么你看我跳来跳去就是数学然后跳物理为什么要跳物理因为我高中初中物理可差呢我想着怎么着学一下吧然后嗯去去学点神经科学也学的生物那一块学的不怎么样但是我觉得跳这个计算神经科学学的挺有意思然后AI挺有意思然后学学这个量化交易前沿在XTX真的是很感谢那段经历然后又去学学法律然后法律喜欢各种各样的从反垄断bytheway反垄断是一个非常就是antitrust是一个非常就是像树状的一个逻辑的一个一个非常非常像数学的一个学科合同法也是然后又有那种完全不像数学的比如宪法就是哎宪法其实这个这个或者说是这种民事诉讼这一些就是庭审这个最初级的庭审这些都是讲故事的一些一些这个这个这个领域然后呢嗯就是所以我还是希望能去学很多的东西就我觉得AIforMath其实对我来说我人生最快乐的时候是我拿到那个我找到那个GitHub的那个link然后我把这里面的那个文章的afterall全读过一遍那是我人生最快乐的几个月然后那个时候最快乐的几个月那个时候叔伯就跟我一块在读然后现在跟叔伯一起做然后当时最快乐几个月那些作者他们陆续加入了Action我们现在有如果你说前30篇AIforMath的文章我们就是大部分都是作者都在我们的Action这里所以又他们就是每天和你就是一块去去去冲这些目标的战友又觉得非常的快乐其实我觉得就是这这可能是不错的一个一个定义你现在是什么的学徒我现在是怎么能够让一个呃一般来说创业公司都会死掉怎么样不死的一个学徒一个创业者的学徒一个一个呃创业者这个词听起来太好了就是就是创业公司9%他都会死掉所以就是怎么我现在是呃就是dontdie这个BrianJohnson有一个好玩的dontdiemovement我现在是dontdie的学徒你看你的第一个自我奖励的方式是通过人来获得的第二个是通过事情来获得的你说你今天今天钟摆已经到了事情这一边但是人能给你提供一个安全垫让你觉得grounded对那有一天你作为CEO嗯当这两个事情发生冲突了对冲突过呀这个怎么冲突过我们也我们也那个也开过实习生对就是我们我们我们也冲突过但就是嗯这个事情我觉得就是你任何的乐观主义收起来你要谨慎的做决定你要想很久就是因为毕竟是要对就是可能人就是要负责然后但同时我有另外一边就是很多时候你觉得为什么要想很久是很多时候你觉得人与事冲突了的时候其实是你自己不够好就是你可能这个人可能都跟你关系很远但是你总是有一些由于你自己技能点和能力的问题是能够让这两个事情不发生冲突的就是他走到冲突的那一刻一定是因为你自己本身曾经有做过一些错误的决定就算这个人可能是一个你不认识的如果公司很大这是不认识的员工他一定是有一些管理层的一个决策他一步一步的尽头trickledown到出现了这样的一个问题嗯所以我还是比较相信一个词叫Authorship就是Authorship就是作者就是你是你自己人生篇章的书写者和作者所以你你不能够有觉得是可能不能够觉得说就是一个情境它就能够决定你的一个决定是你决定让这个情境决定你的决定的所以你也可以决定用其他一些方法去使这个情境不要这么走我是这么想嗯那我们最后还有一些小问题好我们会让每个嘉宾给我们观众推荐一本人生之书你会推荐哪本它要真的对你人生产生过很重要的影响它不能是数学书你也可以说是数学我数学书的话我如果是年龄比较小的观众我我推荐数初等数论里面对数论讲的真的是很好如果是数学书其他数学书我觉得呃德文普尔的那本分析书论我觉得很好然后呃对我还是比较喜欢书论如果不是数学书的话我是那个我挺喜欢《红楼梦》的就是我确实是挺喜欢《红楼梦》的甚至是《红楼梦》很多学者他们去研究《红楼梦》这个是一个曾经在我小时候对我比较有震动的一本书然后刚才也讲到《大雅宝胡同甲二号》对我人生产生影响比较大的其实有挺多关于一些企业家的一些故事比如说伊隆马斯克的故事就是说还是他之前的一个人太太他讲的是他晚上睡不着翻来覆去然后就痛苦的咆哮马斯克痛苦的咆哮然后包括说是一些其他的说是华人先说就是painandsuffering这些东西我觉得就是由于就是可能看到过他们的这些故事会让你有些时候比较难的一些感觉像嚼玻璃的日子里面会觉得哎这就是一个正常的一件事情你觉得现在训AI跟你当年训自己有什么不一样这是一个很好的问题对我觉得有时候你会觉得有点像啊比如说就是看到他这个表现刚刚好了一点马上给他更难的提这种curriculumsampling对吧这这是一个很有意思的一个事情比如说呃让他能够去嗯给他给他哦比如说看到他做不force的时候又觉得是跟跟跟自己曾经的那个数学家的那个那个感受有点像呃没有说特别应该有区别但我目前没有特别能够想得起来的点就是你感觉你看到相似的时候你就会特别有这个你的大脑里的神经元就在发射假设Axon的AI在未来证明某个重大的猜想但在证明过程中使用了一个新的公理这个公理不是现有数学的一部分但是看起来非常的合理你会接受这个证明吗能想象到所有的数学家们就是感觉就是世界末日的一个思想实验我們看到了AI在嘗試用各種各樣奇怪的功力去幫他作弊這個事情已經發生了對嗎就是我剛才講的其實這個事情DeepSeek還為此受害他當時說DeepSeekProver我忘了是哪一個Version說做出來了PenPen上的當時600多道碰壇班上的题就是SOTA在各位数然后那个DeepSeek说我们做出来了49道事实上只做出来了47道有两道题其实就是这个AI在作弊我觉得如果这个公理大家觉得是自然的大家就会接受它但是这个事情我觉得就可能是一个大家以前没有探索的很足够的数学领域不然的话你可能会认为存在即合理或者不存在即不合理这个公理可能已经被被假设了所以它可能是到了一个有点像我们看代数几何混这个组合除了君赫的这个代数组合学这个我们可能未来有一个我瞎说啊probabilisticanalytic这个这个真的是瞎说可能我们未来有一些就是混的混了好几个领域的这样的一个东西大家再往里面加东西我觉得就是是可以按照接受和不接受两个世界照样去运作的当然你这个branchingfactor现在是2你如果继续这样你就会有无限多个世界然后就会一团混乱然后有一天大家可能就会说回收我们把它tighten但这个其实是数学某种程度上是一个是一个人类文明的一些构造所以我觉得大家是可以的就比起比如说物理你要加一个什么定律这个可能大家会觉得其实还就更不可接受一些其实挺有意思的刚才我们其实也谈到了DeepSeek你会怎么看中国AI现在的发展呀包括DeepSeek包括自己包括KimiMinimax等等公司你觉得在未来的AI宇宙里中美会是什么样的关系和角色我很respect就是这些中国的这个AI玩家就是比如说我很诚实的说我觉得就是豆豹SEED他们做AI方面做得非常的好非常的好然后他们也是非常短的时间非常执行力强的一个团队跟他们的一些同学比如说袁正跟他们聊过就是非常好的一个团队我觉得就是他们然后他们可能会呃选择或者选择不发发一些文章然后我觉得就是这些ideas可以就是流通还是挺挺好的对但是当然大家可能最核心的一些东西还是会可能不在文章里写然后可能会做一些他们没写什么的decipher但是就我还是觉得如果是要做纯粹的科学与创新的话就是稍微往学术一点就是少一点就那种商业的一些顾忌多一点学术的就是信任与纯真我觉得是好的一个希望大家一起啊是一个好的就是工业界的一个practice对中美呢中美的话我也不知道就是我觉得好多反正人才不分世界对吧但大家可能有就是有些同学愿意在中国生活有些同学愿意在美国生活之类的就不知道你觉得206年你对AI发展会有哪些预期2026年我觉得大家应该能把这个会看到很快我觉得我们能看到第一个continuelearning的一个小模型啊我觉得我们很快能够去啊看到一个非常好的multimodalreasoningmodel我们很快所有的这些就是什么agentseconomic全部会被scaleup我觉得我有一些个人大胆的预测我觉得很好值得做的一个orchestrator是很好值得做的然后我觉得subagents刚才讲过是很好继续做的哦我觉得formalverificationtooling应该作为RLreward完全是underexplored这个和我们做的也很有关系对你刚才说的第一个和第二个分别你说的是谁做出来第一个continuelearning持续学习我知道有一些不错的团队我感觉他们很快就能出贸的是小公司还是大公司小公司全是小公司哦都是Neolab都是NeolabMultimodal也是吗Multimodal也是Neolab他们应该很快就会就是很快就会问世了啊在South的一个公司也是我的好朋友对当时也希望他能来加入Action就祝福他嗯一些快问快答嗯一个全球范围内你喜欢的食物全球范围内喜欢的食物啊喜欢就是寿司任何的寿司一个全球范围内你喜欢的地点啊喜欢地点心理为什么我小时候第一次出国是去悉尼一个少有人知道但是必须知道的知识点可能是一个冷知识你可以自己打cpu你最近对于生活的一个非常新鲜的鲜活的认知是什么或者体验我可能我最近过得也不是特别我每天早上就是几点钟起来然后一直工作到晚上几点鲜活的认知和体验就是我觉得还是每一次我去就是在跟就是新希望能加入Action的同学聊的时候就会觉得未来无限好未来无限希望然后觉得感觉到那种自己曾经做这件事情的初心并没有因为就是反复日复一日的执行感觉被打磨掉就是觉得非常的快乐感觉像是两只鲸鱼又在找到了彼此的这个聊天频率这个还是挺好的所以招人是一个我非常快乐的事情鲸鱼找到了自己的聊天对就是有些鲸鱼它那个就是频率跟别的鲸鱼不一样然后如果说你遇到一个人然后你们都以前是学数学的然后可能你们现在都对AI有些理解但你们又同时有一些新的理解然后你们聊一些东西的时候还挺有意思的另外一个我觉得比较鲜活的体验是我们就是发现非常多古老的一些技巧对我们现在的这个比较前沿的研究有这个有这个有指导价值然后这个有点像这个24视频它有一个叫如江不进与古为新还是挺有意思的每一次有这种callback我觉得特别有意思像世界是一个世界是一个云我们又回到了原点你心目中影响AI进程的几篇论文我覺得第一篇我覺得是其實是ChristianZagidi的那個白皮書都不是論文就是他想未來應該是什麼樣的這是第一篇第二篇我覺得是可以看GillianLample和FrancoisCharton的那個就是發現說可以去讓transformer去做一些task然後後面當然這一篇論文是他們開始很多的嘗試後來拿這個東西去找其他的構造第三篇DraftSketchandProof这个讲过了第四篇其实就是一堆bundle就是从KeymanApprover到DeepSeedProverGoldoProverE和RSeedProverHilbertProver所有的这些就是真的在拿RL把它做起来了的因为我们刚开始的时候连就是从来没有一个RL做的formalprover我们刚开始的时候连这个都没有我们在融资和这个做这个法律使得这个钱到账的这个过程中出现了KeymanApprover基于当下的认知,一个你最关键重要的step是什么? 我betsystem,我不betmodel,我bet就是这个system有非常多的事情可以做然后包括orchestrator,然后我另外的一个基于与这个又相关的一个bet就是我完全相信recursiveselfimprovement是很快就能够做出来的然后有一个问题就是如果你做出来之后就是然后呢你是然后做什么这个东西就是能否就是我觉得可能会出现一个呃这个需要一些forwarddeployment的一些东西我觉得forwarddeployment的东西还没有在AI的时代得到一个革新然后我觉得传统下次会我们工作室叫做语言及世界工作室当你第一次看到这个名字的时候你会想些什么我第一次看到这个的时候我想的就是说我觉得数学家们他们在几千年和或者几千年几百年他们都是在拿英语写代码或者说拿中文写就拿他们的那个本国语言写代码就是他们在进行的是逻辑的推理但是他们是在自然语言里面去进行的逻辑推理这是一个让我觉得非常神奇的一件事情然后由于这个特质现在我们可以看到说是比如说就是就是做这个计算机的同学们可以拿自然语言去写写代码但数学家已经做了就是几千年了所以數學它所有帶來的這一些結構啊這一些邏輯為什麼說和這個代碼驗證它有幫助其實是有這樣一個特性這是我當時在想的一件事情然後另外我在想的一件事情就是說如果你去把这个世界想象成一个manifold一个比较高维的这样的一个几何拓扑的一个流行你这个语言它这个带来的或者说是基于textbased的就是nexttokenprediction这个AI它到底在这个上面有多少探索了多少然后又flatten了哪些呢我反正就在我曾经有一段时间在想这个因为我在想怎么调lossfunction但是这是我的一些感受字幕by索兰娅✿好了今天的节目就是这样这里是商业访谈路是一档由语言及世界工作室出品的深度访谈节目你可以到公众号关注我们的工作室获取更多的信息我们的公众号是语言及世界languageisworld我们希望和你一起从这里探索新的世界wellexplorethenew