从硅谷创业现场到数学的震撼时刻
访谈开始于美国硅谷——扎克伯格最早创业的所在地，一栋淡蓝色的可爱小屋：Facebook House。主持人小俊迎接了本次访谈嘉宾洪乐潼，一位零零后华人女性、Oxim（原Axium）公司的创始人兼CEO。她所专注的方向是 AI for Math，其公司刚完成 16亿美元估值的A轮融资，引发广泛关注。这一融资背后甚至出现了“五十七岁美国终身教授辞职去给二十四岁华人女孩打工”的戏剧性新闻。
在聊到数学本身的魅力时，洪乐潼回忆起自己被数学“击中”的时刻：虽然自己解题时较少有闪电般的顿悟，但在阅读他人成果时，常被数学的‘美’震撼。她举出两个典型例子：一是模形式与椭圆曲线之间的对应关系（即谷山–志村定理），它将代数表达与几何对象联系起来；二是概率与物理交叉领域中那些令人惊叹的结论。她特别提到在罗斯数学夏令营的经历：每日题集像游戏打怪，完成才能解锁下一关；当学到二次互反律时，面对多种简洁却深邃的证明，她真切感受到数学的创造力与优雅。
我印象中特别深，其中一个例子就是说，啊，第一次看到这个，啊，模型式椭圆曲线定理……相当于是把一个比较代数性的一些一个一个表达式和一个呃更几何性的一种几何物体，联系起来。
我就是自己解题的过程中，这个稍微就是低频率一些，但是我经常在看别人结果的时候，有一种哇，这个东西怎么这么美的一个感受啊！
数学：被发现还是被创造？
当被问及“数学到底是什么”时，洪乐潼认为它既非纯粹发现也非单纯创造，而是一种介于艺术与科学之间的文明建构过程：人类选择一套公理作为契约起点，再在此基础上层层搭建理论体系。她强调，数学研究往往始于对具体例子（如数列、集合）的观察，从中归纳出自然的猜想，再通过证明将其确立——这一过程“有点像艺术”。
她进一步探讨了数学中“直觉”与“证明”的张力。拉马努金的案例尤为典型：他凭直觉提出大量未证明的公式，却由哈代与Littlewood等人用严格逻辑验证并接受。这说明证明是数学共同体的‘说服机制’，而非真理的唯一来源；一旦证明被认可，无论其风格多么另类（如张益唐关于素数间隔的证明），都会被纳入知识体系并引发后续传承（如James Maynard的菲尔兹奖工作）。
证明其实某种程度上它是影响力：我只要能够去把这个东西严丝合缝的逻辑证明出来，我这个数学的发现就是可以被接受的。
所以数学不是人类的特权，对吗？
蛮力型选手与AI的共生进化
洪乐潼坦承自己并非天赋型选手，而是典型的“蛮力型选手”：在数学竞赛中，她无法像他人那样用几何直觉快速解题，只能用复数法将几何问题强行转化为代数运算，“大力出奇迹”。这种策略虽耗时更长，却让她在MIT等天才云集的环境中坚持下来——“你只要看看左边看看右边，就知道自己不是天赋型选手”，但她自比“打不死的小强”，用持续数月的反复尝试攻克难题（如Sphere Packing问题）。
她指出，AI在数学中的角色正呼应这种“蛮力”路径：Google DeepMind的AlphaGeometry通过将几何图形符号化，成功解出81%的IMO历史几何题；而她的公司Oxim开发的Action Prover AI，在普特南竞赛中以人类历史上第六个满分成绩脱颖而出——其解法是数千行Lean代码的枚举与逐步验证，与人类天才Evan Chen的“一张图解法”形成鲜明对比。她总结道：AI系统内部其实包含两种‘数学家’类型——一类擅长提纲挈领的高阶策略（如Tactic推荐），另一类则专注底层严丝合缝的机械推理；二者互补，共同拓展人类的数学能力边界。
所以其实 AI 这系统里面两种就是类型的 AI 数学家，它也能相辅相成。
它可以看到这个机器，他会去，就算是一道很明显可以去做创造力解法的一道题目，他可以去通过他自己擅长的东西去给出给出一个完全不一样的解法。
童年：自由注意力的沃土
洪乐潼在广州出生并长大，童年记忆里最鲜明的是这座城市浓郁的烟火气与丰富的美食。她住在学校附近，每天步行十分钟上学——这段路常成为她自由注意力（free attention）的流动空间：思绪漫游，偶尔回神时已偏离路线，却并不焦虑，反而视其为一种非常快乐的状态。这种状态与她后来创业时接触到的“bounded attention”（被框架的注意力）形成鲜明对比：后者指被截止日期、待办清单等任务驱动的、高度结构化的注意力模式。她指出，自由注意力是区分普通执行者与顶尖策略型创业者或数学家的关键能力；它看似低效，实则为灵感与直觉的孵化温床。
“某种程度上，就是人家说爱因斯坦的洗澡事件，这个过程中其实能够有很多很有意思的一些，就是大脑能到一些很有意思的地方去。这可能是灵感和直觉来到你的大脑里的时候。”
她强调，自由注意力与限制性注意力并非对立，而是应动态配合；但若一味追求“军训式”的每日任务清零，反而会丧失宝贵的 opportunity cost（机会成本）。她怀念童年那种“像玩一样”的投入感——做题不是苦役，而是沉浸其中的探索游戏。这种主观体验（“我在玩还是在工作？”）比客观耗时更能定义注意力的质量。
从竞赛到高等数学：零和游戏与正和世界的切换
尽管童年充满自由探索，洪乐潼仍参与数学竞赛体系，并坦言自己并非天赋型选手——入学时被分到四班（靠近洗手间），远非楼顶的二十四班（重点班）。她曾努力向上攀爬，但随着年级增长，逐渐拒绝被驯化，对排名与竞争产生疏离感。初中起，她转向高等数学（微积分、实分析、复分析），发现其中不再是零和游戏，而是正和游戏：没有统一考试压力，可自主探索深度与广度，也能与志同道合者合作分享。
这种视角转换深刻影响了她的策略选择。例如在竞赛中，她明知应优先攻克几何与代数题以确保高分，却因对数论的热爱，执意从最后一道数论题入手——结果常因时间分配失衡而吃亏。她坦承自己并非强竞争者，而是拒绝被系统规训的visionary（前瞻型梦想家），更愿追随兴趣的内在节奏。
“你要是做出来，你就进省队了……但我当时由于我就是课外的这种非常浓厚的兴趣，加上我非常的喜欢数论……我就会先从这道题开始。”
她观察到，当身处群体目标高度统一的环境（如竞赛集训），人会本能地寻找“tribe”（部落）——与拥有相似非功利性求知欲的同伴结盟。例如她与朋友沉迷于“骑士巡游问题”（n×n棋盘上不重复走满所有格子），不仅为胜负，更在共同证明中获得纯粹的智性愉悦——这正是她心中数学最本真的模样。
创业者光谱：Visionary、Executor与Salesman的互补生态
在创业语境中，她借导师观点梳理出三类核心创业者类型：visionary（梦想家/前瞻者）、executor（执行者）与salesman（销售者）。她自认属于visionary——极度乐观、目标驱动，但非强执行派或销售型人格；扎克伯格是典型的executor（“执行狂”），而马斯克是visionary，Sam Altman则是salesman。她强调，成功团队需兼顾同类与互补者：扎克伯格身边既有梦想家（如CTO Shrap），也有稳健执行者（如前COO桑德伯格）。
她所在公司大量早期成员来自Facebook，因此继承了其标志性的bottoms up文化（由下而上），与Google的top-down文化形成对照。这种文化根植于扎克伯格自身对色彩的感知差异（色盲），催生出充满活力的办公环境：全天候冰淇淋店、乐队排练区、鼓与吉他……紫色成为Facebook的象征色，也隐喻着一种打破常规、鼓励表达的组织气质。对她而言，这种文化不是刻意设计，而是由创始团队的集体基因自然延续而来。
马步棋游戏与协作式数学探索
在初中时，作者与几位数学好友沉迷于一个类似“骑士巡游”的棋盘游戏：在n×n棋盘上，用马步（日字形）移动，不重复地遍历尽可能多的格子，并为每一步编号。他们起初比拼谁走得更远（例如8×8棋盘上尽量接近64步），后来转向更深层的数学问题——是否对任意n≥5，总存在一种方式能走满整个棋盘。他们推测可用数学归纳法证明，但需构造大量小规模棋盘（如n=5,6,7）的可行路径作为基础案例。由于构造过程极其困难，他们组织起一个约三到五人的“小部落”，成员均为数学班尖子生；课堂上不听课，转而传纸条画棋盘、共享新发现的路径。这种高度协作、集体攻坚的模式，让作者联想到现代形式化数学的实践：例如陶哲轩与Alex Kontorovich团队对素数定理的形式化验证项目，将复杂证明拆解为数百个可并行处理的Lean子任务，由全球数学家与程序员共同完成。这揭示出数学远非“孤独天才”的神话，而更像大型软件工程——依赖清晰的结构分工与集体智慧。
“这个过程其实我觉得是很有意思的……合作性就需要一个比较好的一个结构和把它就是把这个呃任务去分散分散成不同的小任务，呃，这个过程其实我觉得是很有意思的。”
“我反正一个人肯定是不可能把所有的这个这个这个例子找出来的，我需要我的这些同学们这个小部落的这个帮助。”
天赋、努力与认知错位：MIT的“最蠢者”体验
作者强调自己并非天赋型选手，而是“蛮力型”学习者：初中阶段并未投入远超常人的学习时间，却仍能进入重点数学组（约25人）；高中时甚至因一次几何题意外全对，拿下升学关键考试的满分。他将此归因于兴趣驱动的发散式探索——如沉迷马步棋、纸条传图，而非机械刷题。有趣的是，这种探索反而提升了他在竞赛数学与后续高等数学中的迁移能力，印证了AI领域发现的技能迁移现象（transfer learning）：数学强的人往往编码能力也强。进入MIT后，他陷入强烈的“冒名顶替感”：身边同学多为IMO金牌得主（如任秋雨、张胜彤），他自认是“数学系最愚蠢的那一个”，甚至期待自己“最傻”，反而缓解了焦虑。这种低预期心态使他坦然接受挑战：大一暑期本计划赴桥水基金实习，却因疫情转为线上，又意外被小野肯教授的REU（本科生数学研究项目）候补名单录取——最终放弃金融机会，开启数学研究之路。
“我每一天就是在就是顶礼膜拜这些大神……我每一天就是在就是顶礼膜拜这些大神。”
“我反正我就觉得我每天很幸运，我和能能能和这些人一起说话，一起上课，一起做作业，我觉得还挺好。”
失败作为默认状态：测度论考试与MIT的“舒适区”重构
MIT的“成绩保护”政策允许新生自由选课而不惧GPA影响，作者与同伴受“东校区”（以黑客文化著称）氛围鼓舞，选择挑战高阶课程——如博士级概率论，甚至从Lebesgue测度论与Borel σ-代数起步。面对完全陌生的抽象框架，他们与同学组成解题小组，群策群力应对难题。期中考试满分40分，全班平均分仅9分，作者等本科生得分均低于5分；他个人考了4分，却未因此感到自我失败，因他清醒意识到：失败是主动选择高难度路径的副产品，而非能力不足的证明。这种体验重塑了他对“失败”的理解——它并非客观结果，而是持续处于非舒适区的常态；而他的乐观与低自我期待，使每一次“失败”都成为探索的注脚，而非终点。
“我从来没有在一个考试上看到自己一个四十分的考试，我能拿四分，四分对。”
“他，我觉得他也不会触发你自己觉得自己很失败的这个机制。”
失败作为默认状态：从九分到重新出发
洪乐潼回忆起自己在麻省理工大一上学期的分析课期中考试：满分40分，全班平均分仅9分，而包括她在内的一群大一本科生，分数普遍在5分以下，成为拖累平均分的“主力军”。她坦言，自己曾在一次40分的考试中拿到4分——这在她看来并非失败的打击，而是主动选择更难路径的自然结果。她强调，自己从未触发“自我失败感”的机制，而是将失败视为默认项（default），并据此理性归因：学不好分析课，是因为实分析基础薄弱，于是她决定重学14—15岁时读过的Rudin《数学分析原理》，系统性补足根基。
“我什么失败都不会触发我自己觉得很失败的机制，就是我把我把失败当做是我的这个default默认项。”
“所以我就开始说，那我要学分析这个课，我学不好的原因就是因为我的分析的底子不好，于是我就开始很认真的去重新把我可能十四十五岁学过的Rudin的实分析，我又再学一遍。”
从团队 camaraderie 到对苦难本身的上瘾
早期，她的自我奖励机制高度依赖小团队的 camaraderie（同志情谊）：期中考后，全班同学集体决定——要么一起退课，要么一起坚持。这种“不抛弃、不放弃”的集体承诺，构成了强大的心理保护机制。她特别提到MIT倡导的“登山队精神”，强调共同攀登的归属感远胜于个人成就。
然而，疫情爆发后MIT封校、团队物理空间瓦解，她被迫转向从“事情本身”中获取正向反馈。她逐渐对困难本身产生近乎上瘾的接纳感，甚至将“痛苦与煎熬”（pain and suffering）视为一种值得沉浸的体验。她观察到许多创业者对苦难的“病态偏好”，并引用风投圈的说法——“chip on the shoulder”（肩上负重）能转化为“chips in the pocket”（口袋里的硬币/资本），即过往的挫折可转化为创业韧性与行动力。她虽承认这一逻辑略显激进，但认为其背后存在真实有效性。
“近几年可能真的是对这个东西完全没有呃负面的感受，所以就是这个难的事情本身，我有种对 pain and suffering 这个黄仁新老师讲的这个有更多的这种 suffering，反而对这件事情有点上瘾。”
MIT塑造的韧性、领导力与数学游戏观
洪乐潼认为MIT对其性格有根本性塑造：学校弥漫着一种“什么难做做什么，什么痛苦做什么，什么长期主义做什么”的集体气质。她举例，即使在波士顿暴雪红色警报天气中，MIT学生仍在坚持晨跑——这种极端毅力具有高度传染性，虽未必能抵达MIT期望的巅峰，却足以驱动人持续向那个方向努力。
她进一步反思：在高压下维系人际关系（无论是pair programming还是团队协作）是一门极其困难的技能。她引用巴菲特与查理·芒格的观点：真正值得招募的人，是那些内核稳定、技术扎实，又能具备服务型领导力的人。她特别指出，中文语境中的“领导”二字易生误解，而真正的领导力应是服务型、跟随型——“登山时，最好的角色不是前面喊话的，而是后面递水的”。
在数学探索上，她将高等数学比作乐高式搭建：每引入一个新定义，便能衍生出无数新定理与问题，形成个人知识宇宙。她引用AI for Math中的“Lego Prover”概念，强调这种创造过程不受零和竞争限制，而是站在巨人肩膀上自由探索——这让她看到数学作为“无限游戏”的深层魅力。
“最好的领导力可能是服务型。最好的领导力就是别人就是就整个团队在登山的时候，啊，你不是前面那个拿着喇叭的那个，你是就是后面递水的那个。”
从神经科学转向AI：一场实验伦理的顿悟
在牛津攻读神经科学硕士期间，作者原本希望深入理解人脑构造——这一动机部分源于家庭变故（祖父健康问题）带来的强烈求知欲。他此前曾参与果蝇实验，操作相对简单：撬开头盖骨、插入电极记录神经动力学。然而在牛津，若想开展脊椎动物实验，必须通过严格的动物实验许可考试，而考试要求亲手处死一只老鼠。这次伦理抉择成为关键转折点：他意识到自己无法接受以杀戮为前提的实验路径，因此果断转向计算神经科学方向。
值得注意的是，计算神经科学与AI在英国高度融合。例如UCL的Gatsby计算神经科学中心（由DeepMind创始人Demis Hassabis创立），其核心 faculty 多为AI研究者；Jeffrey Hinton作为AI奠基人之一亦是该中心创始人。作者在此结识了Andrew Saxe、Sean Gill、Tim Barran、Will Dorial、James Whittington等兼具数学、AI与神经科学背景的杰出学者。作为硕士生，他坦言初见这些学者时“非常激动”，认为他们能引领自己进入真正的研究领域。
“最后。我最后是就我的我的那个快乐来自于来自于AI，不来自于神经科学。”
“我当时是一个硕士的一个一个一个同学……我感觉这个人好像能带我做做研究，然后觉得这是个非常好的机会。”
硕士论文：用数学工具解构AI神经机制
尽管身处神经科学项目，作者的硕士论文实际由一群AI研究者共同指导完成，最终成果聚焦于两个方向：其一是连续学习（continual learning）中的神经动力学分析；其二是对单层线性Transformer的理论建模。后者因无法直接处理非线性神经网络，转而依赖大量线性代数与矩阵运算进行精确推导。这些工作体现了基础数学工具在AI-认知科学交叉研究中的核心作用——欧几里得几何、微积分、概率论等并非抽象符号，而是理解智能系统行为的实用语言。
“呃，就是有其实有找到说，比如有一篇其实就是continual learning的一篇……另外的一篇是，就是去看一个假设一个呃 one layer linear transformer……非常大量的线性代数，非常大量的矩阵运算。”
交叉学科的碰撞：法律诠释学、形式化证明与AI数学
作者在斯坦福法学院求学期间（2023年9月–2024年12月），系统研习了美国宪法解释的三种范式：原旨主义（originalism）、文本主义（textualism） 与活宪法主义（living constitutionalism）。他明确自认是“textualist”——主张严格依据文本字面含义进行诠释，这种风格与数学家追求定义精确、逻辑严密的思维方式高度契合。
正是在法学院课堂上，他萌生了一个关键洞见：若AI可被用于解析法律文本的语义结构（而非事实判断），为何不能将其应用于数学证明？ 这一想法迅速与现实联结：好友Kenny Luo（帝国理工/MIT交换生）正跟随Kevin Buzzard在Lean证明助手中构建形式化数学库（Mathlib），而Lean的本质正是将数学语言转化为可计算的代码。作者意识到，数学的结构性与形式化语言天然适配，而法律文本的模糊性恰是AI更难处理的领域。
“如果我们已经到了一个能拿AI去看这个宪法是什么意思的这样的一个时代了，我为什么不能拿AI做数学？”
“AI应该能够达到一个很熟练运用所有Devanport里面数论的工具与技巧的一个博士生的程度。”
咖啡馆里的偶遇与数学缘分
在法学院图书馆待久了，周末总想换个环境放松心情。Alto Downtown 附近有一家名为 Verve Coffee Roasters 的咖啡馆，它最特别的地方在于——只有周末才会有狗在庭院里活动。这些狗的主人平日忙于工作，周末才来遛狗，于是作者便把这里当作学习与放松的“第三空间”：点一杯抹茶，读法律案例、做笔记，同时观察狗儿们嬉戏，构成了他独特的快乐日常。
在这家咖啡馆里，他和一位常客逐渐熟络起来。两人最初因一个微小的互动结缘——他请对方帮忙拉上遮阳的窗帘，由此开启对话。他们坐在唯一的六人长桌旁，彼此都成了固定常客。起初只是泛泛而谈，后来发现对方本科与硕士均主修数学，甚至可能拥有两个数学硕士学位；而作者则因常看数学类书籍（如《数学天书中的证明》）被对方误认为是数学系学生。
“我就是，我就，我就like非常谢谢你帮就是拉这个窗帘。” “我经常看到你。” “我是也经常看到你。”
这段看似平淡的开场白，最终演变成持续一年半的深度交流。他们聊科学史、数学文化、AI发展，彼此成为对方在斯坦福校园外的重要思想伙伴。有趣的是，作者并不知道对方是AI领域的重要人物，甚至不知道他当时已在Meta工作；而对方虽听说过“摩根奖”（Morgan Prize），也了解一些获奖者转入AI行业的案例（如Alper在Anthropic、Greg Yang在XAI），却未曾意识到眼前这位数学PhD候选人，正是未来将共同创立AI for Math公司的联合创始人。
从学术探索到创业决断：一场理性的自我验证
2024年秋天，作者刚进入数学PhD项目，同时在量化公司XTX兼职。在那里，他第一次近距离接触高性能GPU集群，意识到AI工程能力的跃迁远超纯学术环境所能提供的可能性。这种体验让他开始认真思考：AI for Math 是否值得投入全部精力？
他回忆道，某次晨跑后，一种强烈的直觉涌现——“这个事情真的要发生了”。他立刻找到Shubh，两人在咖啡馆用一张餐巾纸估算融资规模与算力需求，最终达成共识：这不是一个可以在校内完成的研究课题，而是一个必须成立公司推进的工程系统工程。
然而，他并非天生的“创业者”。他坦言自己本质上更向往学术生涯，对硅谷的创业文化持保留态度——尤其反感“浮躁跟风”式的AI创业浪潮。他回忆在MIT时，曾因拒绝创业社团的免费寿司活动而被朋友调侃；他更倾向长期、基础性、高难度的问题，而非短期产品导向的项目。这种价值观使他在决定创业前经历了长达两个月的激烈自我劝退。
最终促使他坚定信念的，是一场系统性的自我验证过程：
- 广泛阅读科学史，从维基百科起步，逐步深入经典文献；
- 精读AI for Math领域的核心论文，建立了一个GitHub仓库，整理数百篇论文摘要，并逐篇研读关键文献；
- 反复进行费曼式推演：若要构建系统，技术路径是否可行？风险是否可控？
他得出结论：这不是一个“是否可能”的研究问题，而是一个“如何实现”的工程问题。技术风险远低于直觉预期，因此，创业是负责任的选择。
“我不可能说我自己觉得这个事情不会成功，然后去骗别人的钱，这个事情我觉得做不到。”
值得注意的是，他甚至曾试图加入竞争对手Verve（其CEO Tudor也是Verve咖啡馆常客），但对方明确表示“只招计算机PhD”，让他意识到：若想真正推动AI for Math，必须组建一个跨学科团队——既懂数学，又懂形式化验证与工程落地。
构建AI for Math的跨学科拼图
最终成立的团队，是一幅精心拼合的跨学科图谱：
- AI与系统层：汇聚大量强化学习、Agent系统、代码生成（PL方向）与编译器（Compiler）专家。其中，LMCompiler核心团队、CodeLlama 32B模型的部分成员均来自此背景；
- 数学层：包含纯数学家（如Kanono小野肯教授）、数学竞赛教练（如IMO金牌得主陈诗琪Evan Chen），以及Lean语言生态的核心贡献者；
- 形式化与元编程层：团队中既有Mathlib（Lean的数学库）维护者（如Kenny罗、居建章、张居建），也有能用Lean实现Autograd等复杂工具的元编程专家——相当于用Lean这门语言，写出Python生态中的PyTorch级基础设施。
这种结构打破了外界对“AI for Math=数学家+程序员”的粗浅想象，真正实现了数学思想、形式化语言、系统工程与机器学习的四重协同。作者强调，团队并非“全是数学人”，而是以问题驱动，按技术栈自然聚合的多元人才共同体。
他特别指出，创业初期最大的挑战并非技术，而是说服自己：这不是一次冲动的逃离学术，而是一次深思熟虑的理性奔赴。当感恩节假期临近，融资窗口迫近，他最终选择等待更成熟的时机——不是因为犹豫，而是因为确信。
元编程与工程化思维：Lean作为工具的再定义
在AI for Math的早期探索中，团队将Lean视为一种可编程的元语言——即“元编程”：不是仅用它来写数学证明，而是用它构建更上层的工具与抽象层。这种思路类似于用Python实现Autograd系统：不是调用已有框架，而是从底层重构计算图与梯度传播逻辑。一位同学曾用Lean实现了一个Autograd系统，这标志着Lean已超越形式验证工具，成为可承载通用计算任务的编程语言。团队成员背景多元，虽包含多位IMO奖牌得主（如五位），具备深厚的数学直觉与上下文理解能力，但核心要求始终是工程能力：能否将模糊的数学思想转化为可执行、可验证、可扩展的系统。正如团队所强调的，“这是一个工程问题”，数学背景是加分项，但不是决定性门槛。
我们要求非常强的……又去二四年九月，哎，你刚刚萌生了想法，但是在努力劝退自己。
他当时在Mela，就是他当时……他圣诞假闲着也是闲着，我们两个人就是找像像是一个reading group……
反直觉的招聘哲学：不招数学家的十五人原则
团队曾立下一条看似反常的规则：前十五人中不招任何数学家。这一决策源于对“AI驱动学科革命”本质的清醒认知——正如当年百度硅谷AI实验室坚持“绝不招一个语言学家”，坚信AI能绕过传统学科专家，直接重构方法论。他们观察到，许多数学家将数学视为一门“手艺”，如日本寿司师傅般精雕细琢，难以接受“Internet-scale dataset”或“scaling”这类工程化、工业化思维。有数学家在接过offer后又拒绝加入，理由正是“不想做大规模数据集”。团队最终希望招募的数学家，是能主动挑战系统弱点、构造更难基准的“对抗者”——而非被动接受者。Ken（小野）加入后主导基准建设，印证了这一理念：最好的合作者不是认同者，而是批判者。
他们当时办公室有一个就是一个一个理念，叫我们绝对不招一个语言学家。
我们以为是这样的。我们我们以为是这样的。我们当时定了一个事情，就我们不招到第十五个人的时候，不要招一个数学家。
阅读即创业：圣诞假期的reading group与学术脉络重构
舒博尚未正式加入时，两人在Zoom上进行了长达数小时的密集阅读讨论——尽管彼此都极度厌恶线上会议（他最多坚持45分钟，她超1小时就崩溃）。正是在这种“痛苦但高效”的协作中，他们确认了彼此思维的高度互补性与节奏同步性。他们精读了杨凯玉等人撰写的综述《Formal theorem proving: the next frontier of AI》，这篇survey将分散的文献串联为清晰图谱：从定理证明的四大能力象限，到每篇引用文献的逻辑脉络，团队甚至发现原始整理的GitHub库遗漏过半关键论文。这次阅读不仅是知识输入，更是创业前的战略校准：它确认了AI for Math的可行性，并锚定了技术路径。当舒博最终在2025年2月决定以联创身份加入时，团队已具备清晰的愿景与执行骨架。
我们发现我们能够是很好的联创团队的时刻，是我们发现我们两个都非常讨厌Zoom……我们Zoom了四五个个小时，每次都……这是我们发现一件事情，我们思考的方式特别的又相似又互补。
我原来知道的，像是一二三四五个很好的做法，现在这篇文章给我连成了一个面了……
融资启动：从JMM会议到第一个offer
洪乐潼的融资之旅始于2025年1月7日前后——彼时正值美国数学学会（AMS）年会（JMM）在西雅图举行，该届大会首次将 “AI for Math” 设为年度主题，对数学界而言是一次极具象征意义的突破。作为数学这一传统学科中罕见的前沿交叉议题，它吸引了大量数学家与计算机科学家参与。洪乐潼在此结识了DeepMind的Adam Wagner，并意外发现彼此曾就读于同一所英国学院（即Alfréd Rényi Institute），而Albert奖得主也曾在此学习，这种学术谱系的偶然重合令人印象深刻。
会后返程第三天，她便收到首个投资意向书（term sheet）。随后进入典型的“竞拍式融资节奏”：一家机构报价后，另一家迅速跟进并抬价，如此循环往复，最终初始offer在两个月内翻了三倍。她坦言，融资过程本身并不难在“结果”，而在于重复性沟通带来的精神消耗——“你是一个复读机，一次一次说一样的事情”，面对数十位投资人反复提问，她甚至考虑过将常见问题录制成标准应答文档。
“他比你更乐观，他比你更觉得你的商业模式有前景。他告诉你这些是你的商业模式。”
其中最具决定性的一次对话，发生在与B Capital的Howard Morgan之间。彼时她正赶一篇论文的rebuttal截止日，却在Zoom会议中被Howard的深度理解与高度认同所震撼——这位文艺复兴科技（Renaissance Technologies）联合创始人、First Round Capital联合创始人，不仅具备数学背景（曾与Jim Simons共事），还亲授纽约大学课程。洪乐潼回忆，自己早年在MIT曾参与Jim Simons生前的线上围炉对话，而Howard正是Simons的表亲，两人外貌极为相似，这种学术传承与现实机遇的奇妙交织，成为她最终选择B Capital的关键因素之一。
融资策略：坦诚风险反而赢得信任
洪乐潼在pitch中展现出罕见的坦诚与克制：她主动指出商业模式尚不清晰，甚至直言“AI for Math未必能成为量化交易的替代方案”，并承认当前效果尚不及成熟量化系统。她以自身量化交易员经验说明：一个数学能力较强的AI，大概率有用，但未必是第一个市场；种子轮的核心目标应是“把技术做出来”，而非急于商业化。
这种反常规的保守表达，反而形成独特优势——多数创业者倾向于过度乐观，导致投资人需对pitch内容进行“打折折算”（如你讲十分，他心里给八分）。而她的“七分陈述”因无折扣空间，反而被投资人视为可信度高、风险可控。她后来才意识到，许多投资人的沉默并非拒绝，而是等待“领头方出现”以避免单独背书风险，形成一种“群体思维下的观望策略”。最终，本轮融资严重超额认购（over subscribed），共有三家机构发出领投意向，价格从一倍逐步抬升至三倍。
值得注意的是，她在一月份已有初步意向，却因对方要求50%领投权而果断拒绝；二月接受另一家报价时，Shubal随即加入团队；三月在Howard Morgan的持续高频沟通（“每天一通电话”）影响下，最终被其愿景与支持力度打动，转而选择B Capital。整个过程凸显其对融资结构的审慎考量——她并非追求最快成交，而是希望构建一个能带来战略协同与长期支持的投资人组合。
创业启动：边上课边建公司，年轻是双刃剑
从三月到六月，洪乐潼处于高强度并行状态：一边完成法学院考试与数学课程（尽管出勤率下降），一边推进公司注册、法律尽调、办公室选址与团队搭建。她坦承，作为创始人，自己缺乏技术团队管理经验，这是年轻创业者普遍面临的“Track Record赤字”；而作为华人女性，她并未感受到明显身份加减分，但“年轻”确是核心变量——在消费级产品领域是优势（用户视角敏锐），但在Deep Tech领域则易被质疑决策成熟度。
她以扎克伯格19岁融资故事作对比：在餐馆中，萨姆·阿尔特曼（原文误作Peter Zill）手持term sheet要求当场签署，扎克伯格离席痛哭后返回签字——这一场景揭示了年轻创业者常处的高压决策困境：信息不全、时间紧迫、后果重大，而延迟决策本身又可能带来更高风险。她引用一次森林高空滑索（zip lining）经历作隐喻：作为第一个跳下者，她只能“闭眼咬牙，形成肌肉记忆式的信任跃迁”，这正是创业者每日需重复的心理训练。
“我有时候倒是觉得……年轻做product是加分，做Deep Tech是减分。”
她反思：若重来一次，愿多读三倍书籍，因当前知识储备仍显不足。高压、高频、高 stakes 的决策环境，要求创业者不仅要有第一性原理思维，更需在不确定性中快速行动——这恰是她此次融资与初创阶段最深刻的体悟。
在高压中跳入未知：决策的肌肉记忆
在创业过程中，许多关键决策往往没有足够时间权衡——你必须在那一刻选择跳下去。正如讲述者回忆：“一闭眼一咬牙我就下去”，而事后团队建议他将这种行为内化为一种肌肉记忆：一种每日重复、近乎麻木的“信仰一跃”（take the leap of faith）。这种高压环境源于创业本身的快速决定性质（nature of rapid decision-making），尤其当面临多份offer竞逐、资源有限、缺乏杠杆时，“bias toward action”（行动倾向）成为唯一可行路径。每一次在“执行”与“不执行”之间选择乐观选项，看似微小，却累积成通向终点的轨迹。
“每一次你在执行与不执行、做和不做中选择那个乐观的选项，你就能够有一天走到那个终点。”
“我有一些各种各样的感受到比较艰难的，可能我现在做的这个决定，我以后会后悔，但是我也得做这个决定的时刻。”
A轮融资：六个月的闪电执行与技术突破
A轮融资始于2025年圣诞节前，由Melo Ventures领投，最终于2026年1月5日完成pitch并当晚获得term sheet，一周后敲定第二份offer，从7月15日种子轮close到1月15日A轮close，仅用六个月。融资额达至少2亿美元，估值16亿美元，正式迈入独角兽行列。这一速度背后是团队在六个月中持续零失误的执行表现：从零搭建基础设施、训练模型、构建系统，到四个月时在普特南数学竞赛中取得满分，六个月时实现首个无人类干预的自动形式化证明系统，并在Verina benchmark上将准确率从DeepSeek Prover的11%提升至98.93%。
领投方Melo的合伙人Matt Craining自种子轮起便深度支持团队，其技术背景（电气工程PhD+物理本科）与founder spirit使其成为理想伙伴；而Melo作为Anthropic最大机构投资人，在AI基础设施层拥有深厚布局，其投资逻辑并非押注通用模型，而是看中团队在deep tech层面的系统性壁垒。
“我们不是一个模型公司，我们是一个deep tech公司，我们做的这件事情有点像SpaceX。”
为何顶尖人才愿意追随一位最年轻的CEO？
尽管讲述者是团队中最年轻、且无Tech Leader背景的CEO，却成功吸引了大量资深数学家与工程师加入。其核心原因在于：研究者与工程师能在无政治、无人事纠纷的纯粹技术环境中专注前沿探索——这正是 frontier lab 所需的理想土壤。更深层吸引力来自问题本身的宏大性与确定性：数学形式化证明虽极难，但其技术路径清晰（如Lean语言的验证机制、证明生成的工程挑战），通过工程手段可系统性突破。
Lean作为兼具编程语言、编译器与运行时的形式化系统，其设计极为“finicky”（脆弱且受限），早期社区验证工具comparator速度仅为自研系统的1/100，迫使团队从零构建一整套工具链（约12–13个核心组件）。面对AlphaProof采用的昂贵蒙特卡洛树搜索，团队果断转向更高效路径——这与字节豆包的DeepSeek Prover思路趋同，但实现更彻底的系统级优化。团队压缩了大量研发周期：Tutor公司耗时两年达IMO五题，而他们仅用四个月冲击普特南满分，并快速响应数学界真实问题（如Falcon猜想、van der Waerden变体），背后是小野肯老师（团队精神导师）所代表的高激励性、乐观导向的教练型领导风格。
“我只是一个递水的人。”
截胡OpenAI：小野肯的加入
小野肯（Ken Ono）的加入过程极具戏剧性。他在尚未正式接受OpenAI或DeepMind的邀约前，便主动向团队发出邮件，表示自己将前往湾区，并暗示可能加入上述两家机构——这实际上是一种出于朋友关系的提前告知，避免让团队在毫无准备的情况下得知潜在竞争关系。他选择坦诚沟通，而非突然“跳槽”。对此，创始人当场回应：“你可以来Action。”随后，双方在极短时间内（仅两三天）完成谈判，赶在OpenAI的offer“爆炸”前完成签约。整个过程没有冗长的招聘流程，也未安排实地参观，仅靠一次Zoom会议就敲定了这位重量级数学家的加盟。
“他去了OpenAI之后，可能觉得那边做数学的同学不是特别多；来我们这边的话，可能有更多数学的一个氛围。”
小野肯最终被Action打动的核心原因在于：Action的DNA是数学本身，而非泛AGI中的一环。与OpenAI相比，这里聚集了真正以数学为第一性原理的团队成员——包括Francis Charton、Evan、Kenny、居建等人，形成了一个被称为“Math Club”的高浓度数学共同体。小野肯本人是继承拉马努金精神的现代数学家，曾明确表示“不信AI会超越自己”，但后来态度发生转变。他的认知变化，与Action在AI for Math领域的持续深耕密不可分。
数学家的叛逆与开放：小野肯其人
小野肯不仅是杰出的数论学家（在模形式、划分函数等领域成就斐然），更是一位极具人格魅力的“高中篮球队教练式”人物：他以极致乐观感染团队，让成员在任务中保持兴致勃勃的状态。他不仅是导师，更是文化塑造者——他带出的学生多已成为优秀数学学者，其指导风格强调直觉与构造并重。尽管他自认在“直觉派 vs 理论派”光谱上居中，但其最独特的能力在于：他是罕见的‘理论建造者’——能打通不同数学分支，提出根本性问题，并为更擅长解题的合作者铺路。
他放弃终身教职加入一家初创公司，并非出于无奈，而是一种主动的“叛逆”选择。他同时身兼多重身份：美国数学学会前副主席、白宫政策顾问、奥运游泳数据分析专家、好莱坞电影导演（拍摄拉马努金与米尔扎扎尼传记片）、以及以拉马努金命名的慈善基金会创始人。这种跨界广度与思想开放性，使他并不担忧AI会“替代”数学家。相反，他与Andrew Granville等前沿学者一致认为：AI的崛起将推动人类数学家向更高抽象层级跃迁——从解题转向提出值得探索的问题，再由AI辅助探索与验证。
“我们真心希望AI能具备一定程度的猜想能力，让‘猜想’与‘证明’形成向上螺旋。”
数学作为AI的试验场：普特南竞赛的实战
Action将数学本身视为AI技术的天然试验场。2025年12月6日普特南大学生数学竞赛当天，团队在清晨收到考卷后，迅速进入“战争室”（庞加莱会议室）展开协同作战：有人同步解题，有人将题目形式化输入Action Prover系统。这一过程不仅检验了AI能力，更揭示了人类与AI解法的显著差异——AI常给出截然不同的思路，却同样严谨有效。
最终，系统在12道题中答对8道（满分120分，80分≈世界前五水平），并成功冲击全部12题满分。这一成绩验证了Action Prover在真实高难度数学场景中的潜力。更重要的是，该实践为AI的self-improvement机制提供了可验证的反馈闭环：每一道被证明的命题，既可作为技能库（如Lego Improver的skill library）被复用，又能转化为后续训练数据，推动系统持续进化。数学因其严格的验证信号，成为测试sub-agents、MCP（Model-Centric Programming）、continuous learning等前沿AI范式的理想“操场”。
“我们希望它一定是self-improving的……某种程度上，self-improvement甚至可以叫continuous learning。”
战时解题：从八十分到十二道满分
在 X Improver 项目中，团队最终采取了一种完全不同于传统思路的解题路径。在当天下午三点五十八分，他们确认已解决八道题，总分八十分（满分一百二十分）——这一分数在去年相当于世界前五，而往年通常处于前十至二十区间。团队随即面临关键抉择：是立即公布成果，还是继续冲刺更高分？最终，他们成功解出全部十二道题并取得满分。
解题过程中，小野肯教授提出了一个极具启发性的观点：“现在是战争状态，不要在数学纯粹之美的时刻去精确地搞这些东西；现在是求解时刻，要怎么快捷就怎么做。” 这一理念深刻影响了团队的工作方式——求解优先、快速喂数、再交由 Lean 完成形式化验证。Lean 本身仅支持证明，不负责求解，因此求解环节仍需人类完成。然而后续发现，系统中已集成的非形式化模型足以直接生成解法，从而省去了人工求解步骤。这一发现令人意外：原以为需人工求解的题目，实则可由 AI 自主完成。
“不要在现在不是说数学纯粹之美的时刻，不要去精确的去搞这些东西。现在是战争状态，就是在大家在求解的时候，他就说能怎么快捷的去去做。”
“因为Lean只能做证明嘛，它不能够帮你说是去求解，所以求解是人做的……最后其实我们发现，我们的每一道普通难的题，其实我们并不需要做人类求解那一步。”
数学家的新角色：直觉驱动的资源分配者
当 AI 数学家逐步承担起大量证明与求解任务，人类数学家的角色正发生根本性转变。未来，数学家的核心价值将集中于提供那百分之零点零一的直觉——即判断哪些问题更值得投入算力去攻克。他们将组织起来，制定“愿望清单”（wish list），评估问题的重要性、连接性与可推导性：解决某问题是否能连锁带动多个问题的突破？
这一转变本质上是资源分配问题。在有限算力前提下，数学家如同战略指挥官，决定将200个 H2 单位投入题A，8000个单位投入题B；算力分配即成为问题价值的量化映射。而在无限算力的愿景下，目标则更为激进：“fold everything”——将所有人类好奇的数学问题系统性求解。正如 AlphaFold 团队曾考虑的：若能折叠两亿个蛋白质，为何还要建平台？直接全量处理即可。
“如果你解决了这个，你应该能够把这一些都解决。”
“如果我们现在在一个无限的算力的情境下的话，我们就要做这件事情，我们要把所有能够人类想到的好奇的数学问题全部解决。”
数学、代码与现实：AGI 的三重验证层
Axiom 团队坚信，数学与编程是孪生兄弟——“math is coding, code is math”，其理论根基源于Curry–Howard 同构：每个数学证明可转化为计算机程序，反之亦然。Lean 等形式化系统正是这一思想的实践载体，使得 AI 数学家的输出（如数千行 Lean 代码）具备自我验证能力。
从数学到代码，再到现实世界实验（如抛鸡蛋验证重力），构成了 AGI 世界观的三层验证信号：数学提供逻辑严谨性，代码实现可执行性，现实实验给出物理反馈。这种闭环结构，使 AI 数学家不仅可推进纯理论（如用中国剩余定理研究神经元容量），亦能支撑跨学科应用（如用微分方程建模刑法效率与个体惩罚的平衡）。
此外，团队强调：纯数学是整个数学生态系统的根基。若纯数学萎缩，应用数学将随之枯竭——正如生物基础科学之于医学。因此，持续投入纯数学研究并非“无用”，而是保障未来技术突破的必要前提。
“数学是一个生态系统，你有纯数学，你就有应用数学。你这个纯数学如果死了，你应用数学也就没了。”
Formal Proof 的三步工作流：从草稿到 Lean
在将数学证明转化为 Lean 的过程中，存在一个清晰的三阶段流程：首先生成非形式化的提纲（draft outline），其次将其形式化为 Lean 草图（sketch），最后填充中间的证明细节（proof）。其中，Lean 中的 sorry 是一个关键中间工具——它表示“此处暂不证明，但假定为真”，用于快速构建结构骨架，后续再逐步替换为真实证明。填充 sorry 的方式多样：可借助 AI（如神经网络模型）、传统自动定理证明器（ATP），或基于规则的系统（rule-based ATP）。尤其值得注意的是，Lean 社区曾长期缺乏类似 Isabelle 和 Coq（现 Rocq）中已有的“Hammer”系统——即能一键解决大量子目标的强力工具。2023年6月，CMU团队发布了首个 LeanHammer，但其覆盖能力仍有限。后续推出的 Grind 系统则展现出更强的确定性求解能力：在某些数学问题上，无需任何 AI 成分即可直接输出完整证明。
Grind 这个其实某种程度上，它能够解决很多的数学的问题。我曾经见过一些其他的 AI for Math 数学公司，它有做一些 demo。其实那些题，呃，你如果 Grind 一下，甚至它都能直接给你做出来。
我们主张一种混合策略：优先使用确定性工具处理可解子问题，仅对复杂抽象层启用概率性大模型系统。这种“由简入繁”的系统架构，既提升效率，又保障可靠性。理想状态下，一个数学证明任务应被拆解为：先用轻量级工具快速清除 trivial 部分，再将剩余挑战交由大模型处理——这正是当前 AI for Math 系统设计的核心范式之一。
AI 与形式化验证的协同进化：从 Prover 到 Conjecturer
AI for Math 的前沿探索已超越单纯“证明”范畴，正迈向 Prover（证明者）与 Conjecturer（猜想者）协同自进化 的新阶段。其中，Self-Play Theorem Prover（董克凡、马腾宇等，Stanford）开创性地提出：可将证明系统作为猜想模型的“奖励信号源”——即一个猜想的价值，部分由其是否可被自动证明来判定。然而，猜想评估远比证明困难：证明结果是二元（成功/失败），而猜想需额外判断其数学意义与优雅性（elegance）。早期方法（如 STP）仅以“题干长度 vs 证明长度”衡量优雅性，但这在高等数学中显然粗糙且不可扩展。
一个数从四十个 node、四十个顶点的一个一个一个数一个一个一个一个证明就可以把它转化成一个数。这个数从四十个我们已经现在 scale 到四千个，就是它是一个更深更广的一个。
我们团队在实践中观察到两个关键突破点：其一，通过 sub agents 架构实现 inference scaling，借鉴 Anthropic 的子代理思想与 Sutton/Silver 关于“从经验中学习”的理论，将数学求解过程建模为可积累的“经历轨迹”（trail），并训练 agents 学会调用工具（learning to use tools）；其二，证明与代码生成的统一目标函数设计：当代码（如 Rust）与证明（Lean）共享强类型语义基础时，强化学习可更高效地同步优化二者，实现“一边验证一边生成”的闭环。这不仅提升形式化质量，也为软件工程带来直接价值。
此外，Auto Formalization（自动形式化）正成为比证明更难的核心挑战：将非形式化数学文献（如 arXiv 论文）转化为 Lean 中的完整定理-证明对，需完成定理切分、结构解析、知识迁移等多步任务。这一过程虽少受媒体关注，却是构建大规模形式化知识库的基石——毕竟，当前 Lean 中仅覆盖了极小部分已发表数学成果。
AI for Math 的生态定位与未来路径
从行业图谱看，当前 AI for Math 系统普遍遵循“预训练模型 + 领域后训练 + 工具集成”的范式：先选用开源基础模型（如 Qwen），再通过 SFT/RL 进行领域适配，最终嵌入包含多种专用模型与工具（如 Lean meta-programming 模块）的系统架构中。主流方案大致分两派：Seat Prover、Hyper Prover 等倾向端到端强化学习路径；而 Aristotle、早期 AlphaProve 则更依赖混合推理与符号引导。
团队在人才构成上强调“全栈工程能力 + 推理建模经验 + agent 系统设计”的复合背景，尤其重视对 Monte Carlo Tree Search 效率瓶颈的替代方案探索。我们坚信，AI for Math 的真正突破不在于解决特定数学问题，而在于形成具有泛化能力的智能闭环系统——其中，形式化知识库是核心基础设施：它需支持高效检索（已知/未知/反例）、自动更新与跨文献对齐。未来，当 conjecturer 与 prover 能够持续对话、相互反馈、自我进化时，AI for Math 才真正从“工具”升维为“数学研究伙伴”。
从数学文章到 Lean 的形式化鸿沟
将一篇数学论文（如来自 arXiv 的 PDF）完全转化为 Lean 代码，远非简单的“翻译”任务。其核心难点在于第一步的结构分解：必须将原文中的定理与证明拆解为足够细粒度的单元——即所谓 blueprint（蓝图）。某些结构清晰的文章可能较易处理，但许多论文的长篇证明中嵌套着多个子引理、引理与推论，若拆分不够细致，后续形式化将无法进行。陶哲轩、Kevin Buzzard 和 Alex Kontorovich 等数学家曾亲自为 PolyMath 等大型项目手写蓝图，再分发给全球本科生分头完成形式化，形成“星星之火，可以燎原”的协作模式。
“如果你需要让一个计算机，不管是 AI 还是一个 robust 的电脑系统，去进行从 PDF 到细粒度蓝图的拆分……这一步是非常难做的。”
这一过程对 AI 而言是巨大的挑战，因为它要求模型具备强分解能力与高阶推理能力，而当前模型对此仍严重不足。此外，Lean 的语料稀缺性加剧了难度：全球 Lean 代码总 tokens 量远少于自然语言语料，导致模型难以学习其语法与语义映射。相比之下，反向任务——从 Lean 到自然语言（即 auto-informalization）——反而更容易，因模型接触过大量自然语言数据；但其验证需依赖 cycle consistency（循环一致性）：将 Lean→英语→Lean 再比对，以检验是否一致无误。
“Lean 作为一个跟 Python 更类似的一种计算机代码语言，这个转化的过程……尤其由于 AI 没见过多少 Lean，现在全世界的 Lean 加起来没有多少的 tokens，所以这是非常困难的。”
形式化语言 vs 自然语言：语义错位与可验证性优势
形式化语言（如 Lean）与自然语言（如英语）存在本质差异：前者具备执行能力，运行后可直接输出“证明成功”（勾）或报错定位；后者则仅承载语义。更关键的是，数学语言并非英语的简单子集——同一词汇在不同语境下语义分布截然不同。例如代数几何中的 germ（germ）虽与英语“细菌”同形，但其数学含义完全脱离日常语义，若仅依赖英语训练 AI 做数学，必然出现严重偏差。
因此，将数学转化为代码，其价值不仅在于表达，更在于可验证性：程序可被严格验证是否满足 specification（规格说明），从而避免传统测试驱动开发中“靠样例覆盖”的局限。这引出了一个核心愿景：任何你能定义的，你都能证明；任何你能指定的，你都能执行。这与 Donald Knuth 早年的梦想一脉相承——让程序员像数学家一样，在自然语言中推理，系统自动完成编码与验证。
“任何你能写出的，或者是任何你能 specify（specify 就是英语里 program specification），任何你能表达的，你都能执行。”
specification 是瓶颈：定义与猜想才是真正的挑战
当前 AI for Math 的最大瓶颈并非证明环节，而是 specification（规格说明）的构建——即如何将人类问题精准转化为形式化语言中的命题。这要求模型不仅能理解问题，还需具备定义新概念的能力。例如在“First Proof”挑战中，AI 用自然语言解出部分题，却无法将题目输入 Lean，原因在于题干涉及大量未收录于 mathlib（Lean 核心库）的新定义；没有定义，就没有可形式化的命题，更无从证明。
这揭示出：定义与猜想是数学中更难的部分。AI 可能擅长推理与验证，但尚无法独立提出新概念框架。即便在芯片验证领域，传统 SMT 求解器（如 Cadence Jasper）仍面临局限；而 Lean 的引入虽带来更强表达力，却也要求用户具备专业数学背景——它不会让所有人“人人可做数学”，但能让更多工程师（如软件工程师）验证专业成果，降低验证门槛。
“所以这是我现在觉得的第一个第一个难点……由于我无法定义，导致我无法证明。”
芯片验证：高价值但高门槛的突破口
当前，形式化验证在芯片设计领域仍高度专业化，需要具备深厚数学与形式语言背景的专家投入大量时间——例如亚马逊曾组建业内顶尖的自动推理团队，耗时三至五年、编写二十六万行定理证明代码，只为验证一个用于CPU优化的hypervisor内存隔离组件。这一过程AI尚未显著改善工程师的生活质量，尤其在需要人工逐条核验数千个license的场景中。尽管如此，该领域具备极强的商业定价权潜力：一旦系统能可靠地验证芯片性质，其价值将远超通用编程辅助工具。相比之下，面向大众的编程场景中，verify generation（验证生成） 才是更关键的长期命题：用户期望在调用函数时，获得百分之百无需额外测试即可信任的代码。这不仅是技术目标，更构成未来商业模式的核心方向。
它要么就说这个事儿太难了，我做不到；要么他会给你一个正确的东西。
所以它是独立于语言之外的关数，数学跟语言应该是平行的关系。
语言与数学：猜想与验证的双轮驱动
在AI for Math的实践中，语言模型擅长生成猜想（conjecture），是突破认知边界的“拐杖”；而形式化数学（如Lean）则负责约束与验证，将直觉转化为可靠知识。二者并非主次关系，而是平行且互补：语言帮助提出“可能成立”的命题，数学确保其“必然成立”。这种“生成—验证”的循环，构成了科学发现的典型节奏。值得注意的是，突破边界并不唯一依赖语言模型——如Francesco Tart和Alberto Averino的工作所示，通过图扰动、嵌入分析、相似性挖掘等方式，也能独立生成直觉性猜想。而证明本身，则横跨两者：既需语言理解用户模糊意图，又需形式系统保障逻辑严谨性。
好的直觉其实就是一个配比，配比其实就是幻觉和这个规律推导的 pattern matching 和这个幻觉的一个配比，这个配比要合适。
定义先行：从 library learning 到 AGI 的挑战
当前系统已能解决多个成熟领域（如交换代数、代数几何、组合概率）的问题，下一步将瞄准Lean中尚无基础定义的前沿领域——如动力系统、随机曲面、概率理论等。真正的挑战在于：当领域缺乏定义时，连命题都难以写出，遑论证明。这引出了核心难题——library learning（图书馆学习）：即让AI自主构建数学理论体系，包括定义、定理与证明，并持续扩展。但定义的验证远比证明困难：如何确保新定义与人类已有体系“faithful”（忠实一致）？ 若AI为简化推理引入新定义，却导致逻辑悖论（如自相矛盾的“好图”定义），系统将失去可信度。因此，定义层的鲁棒性（robust to distribution shift）是通向更广数学AI的关键瓶颈。
我们相信能够去做一个尽量perfect的AI。
ASI而非AGI：专注数学的超智能路径
在探讨AI智能类型时，我们更倾向于使用 ASI（Specialized Superintelligent AI） 而非 AGI（Artificial General Intelligence）。后者追求覆盖人类所有超人类任务的“全圆盘式”能力（如证明黎曼猜想、写出莎士比亚级文学、治愈癌症等），而我们的策略是：从数学这一高度结构化、边界清晰的领域切入，以垂直突破带动横向辐射。具体而言，我们以“证明黎曼猜想”为圆心，向代码验证、物理建模等方向发散出一个扇形能力域，而非试图覆盖所有人类智能领域（如文学创作）。这一路径不仅更可行，也具备明确的B2B商业价值。
“我们不是，我们是，我们从这儿然后往这个证明黎曼猜想这儿打，我们就往数学这个代表数学的这一个超人类任务打。”
“打完了之后，我们觉得他会发散出一个扇形，……我绝对不会覆盖到这个拿诺贝尔文学奖这里。但是我会有一个比较大的扇形，而我这个大的扇形，在我这个B to B的这个市场上是有意义的。”
形式化验证：智能与确定性的双重保障
AI for Math 的核心哲学在于：它同时提供‘超人类表现’与‘百分之百正确性’。前者体现在模型能生成数十页复杂数学证明；后者则依赖于形式化证明这一基石——即所有推理必须在 Lean 这类证明助手中被机器可验证。相比之下，非形式化路径（如纯大模型推理）虽可能更快落地，却难以保证无误，也难以支撑长期的 recursive self improvement（递归自进化） 能力。
我们相信，验证是AI科学能力的‘第一性原理’：它不仅是产品功能，更是构建可信AI科学家生态的前提。未来，这一能力可延伸至 AI for Science（如理论发现）与 AI for Optimization（如工业级边缘case覆盖），尤其在那些“沉默性高投入、高回报”的场景中——例如芯片验证依赖的枚举与分类讨论，或搜索引擎对极端情况的完备覆盖——数学与形式化方法提供了不可替代的底层支撑。
“所以在这两个象限上再往上推，然后我觉得AI for Math是我们公司的这个DNA，或者Math我们是我们的公司的DNA。”
多元智能协同：数学家+编译器专家+AI工程师的三角驱动
我们的DNA是“多元产生智能”，具体体现为三类人才的深度协同：数学家（提供问题建模与直觉）、编译器/代码生成专家（实现自动形式化与Lean数据生成）、以及AI工程师（驱动模型训练与推理优化）。这种组合使我们能高效应对数学AI特有的挑战——例如在Lean数据极度稀疏的背景下，模型频繁遭遇“拦路虎”，反而比在通用文本领域更早暴露系统瓶颈，从而加速技术迭代。
我们坚信，数学是现实世界的‘沙盒’：它兼具可验证性、结构性与规律性，远比依赖实验验证的生物/化学等科学领域更适合作为AI推理能力的训练场。尽管我们尊重如 Periodic Labs、Edison 等 AI for Science 公司的探索，但我们的定位是“理论侧的拐杖”：为实验科学提供可验证的数学支撑，而非替代湿实验本身。
“我很好奇啊，嗯，你们公司就是有数学家的公司，和你那个竞争对手，他不要数学家的公司，他DNA区别会是什么？”
“我们觉得就是……降维打击，另一个是多元智能……我们做一个更难的事情，希望能够垂直下来给其他的一些领域，就是某种程度上能够去去去去。去降维打击。”
Auto Formalization 是猜想探索的前提
在探索 AI for Math 的过程中，团队经历了大量失败与试错，但关键在于：失败本身无法清晰归因，尤其当 formalization 工具（如 Proof Assistant）尚不成熟时，难以判断是模型能力、数据质量，还是自然语言到 Lean 的转化环节出了问题。因此，团队坚持认为，必须先将 auto formalization（自动形式化）做到位——即高效、准确地将自然语言数学陈述转化为 Lean 代码——才能为后续的猜想生成提供可靠基础。这不仅是获取高质量训练数据的手段，更是提升证明自动化水平的核心技术支点。
我们希望能做好这个的话，能够有更大的，既是一个能拿更多数据的手段，又本身能够对证明做一个很好的一个一个帮助，然后我们才会去做这个猜想。
猜想其实是数学最有魅力的地方，是吗？
直觉型数学家 vs. AI 的能力边界
Ken Ono 的加入为团队带来了对“猜想生成”的深刻理解。他与拉马努金的关联不仅体现在家族传承——其父曾参与拉马努金雕像筹款，并保存了拉马努金遗孀致其父的亲笔信——更在于精神内核：两人均被视为直觉型数学家。但二者风格迥异：拉马努金的直觉是“尖锐的、公式驱动的”，常凭宗教冥想或梦境获得公式；而 Ken 更擅长发散式连接不同数学领域，提出系统性猜想。
这引出一个根本问题：AI 能否训练出拉马努金式的天才？ 目前团队聚焦“后训练”（post-training），而拉马努金的直觉可能源于其独特“预训练”——长期沉浸于宗教仪式、非线性思维与早期数论直觉的混合环境。AI 若仅靠后训练，难以复现这种浑然天成的洞察力。但一旦拉马努金学会形式化证明，其直觉便获得“指数级放大”——证明能力将直觉转化为可传播、可迭代的知识。因此，AI 辅助证明，仍是对直觉型数学的重要赋能路径。
他到了这个剑桥之后，他接触了就是证明，他知道如何写证明了，然后他就使得他的这个数学的这个影响有有更指数级的爆炸……
他有说过这个，这个不知道。我肯定不是预训练的产物，而且你看他的预训练好像不只是数学。
创业定位：专注形式化数学的‘登月’公司
作为一家成立仅七个月的创业公司，团队清醒认识到自身处于“高密度人才密集型赛道”，与 OpenAI、DeepMind 等巨头的策略存在本质差异：大厂多将 AI for Math 视为 AGI 的子任务，或用于增强通用推理（如先 informal→formal→验证→反馈），而非核心产品。而本团队选择“专注、垂直、形式化”路径，虽面临执行与学习时间的尖锐矛盾（“执行越多，学习越少”），却坚持长期主义——公司 DNA 是‘登月’，而非逐利。
尽管有人将 Lean 数据用于预训练，团队明确拒绝自建预训练大模型，原因有二：成本过高，且 Lean 生态的深度价值更依赖后训练与领域适配。他们更愿与大厂形成“互补性合作”，如 SpaceX 式的“鱼与熊掌兼得”哲学：既追求登月成功，也接受多次坠毁的迭代过程。团队坚信，该项目的结果是 binary 的——要么登月成功，要么彻底失败，没有中间态。
如果我是这些就是玩家之一的话，并不一定会去做我们现在做的这件事情的原因是，我一样的人才的这种这种高高密度人才的队伍，我可以把他们再继续在代码生成或者说在一些更红海的一些目前竞争咬的比较紧的呃的领域去去去去去做的更深……
人机交互与创业生态：好奇心作为底层驱动力
当前的人机交互体验仍远未成熟，尤其在专业领域如数学中，工具的可用性与效率仍有巨大提升空间。在谈及硅谷模型公司与New Lab之间的竞争时，访谈者指出：短期输赢导向的环境（如量化交易）会扼杀长期主义——正如Peter Thiel所言，“垄断催生创新，竞争导向平庸”。正因如此，许多怀抱burning passion的研究者选择离开大厂，投身New Lab：这不是出于功利目的，而是源于人类与生俱来的好奇心，一种无法被压制的基本需求。
一个关键思想实验是：若AI已能解决所有千禧年难题（如P vs NP、Hodge猜想），数学家是否还有存在的必要？答案是肯定的——人类不会满足于“答案”，而会追问“为何如此”。一旦看到一个百万行Lean代码构成的证明，人们仍会主动拆解、理解、重构，进而催生新的猜想与理论。这构成了“AI发现 → 人类理解 → 新发明”的正向反馈循环。正因如此，即便面对一亿美元级项目资助，也无法真正“收编”青年研究者的好奇心；他们反而会以更自由的方式，创造出如Stefano Arman的快速diffusion推理模型、Periodic在材料科学中的探索、Recursive在AI-硬件协同优化等极具原创性的方向。
“你给我一个一百万行Lean代码的一个，我一定要去看里面是怎么做出来的。你不让我去看，我都会去看。这就是人类的这个好奇心的体验体现。”
“由于这个证明最后被产生的方式，这些去看懂了他的数学家们又会有新的猜想、新的想法。这就是整个这个发明发现的这一个这一个循环……AI做了，可能AI做了这个发现，让数学家更好的发明。”
登月精神与失败文化：在不确定性中前行
当前AI for Math领域常被问及：“这是泡沫还是登月？”——访谈者认为，真正的登月项目不以成败论英雄：有些公司虽未成功，但其团队日复一日的真诚投入（如“九九六一块朝梦想努力”）本身即具价值；而真正的问题在于，当养老金等社会资金通过多层投资进入高风险前沿探索时，我们是否承担了过高的系统性责任？
然而，若研究者是被使命驱动而非 ego 驱动，则其协作更具整合性——例如，面对同一问题，八支分散团队各自为战是低效的；而当不同背景（数学、CS、物理）的研究者围绕同一愿景协同攻关时，这种探索才真正具备legitimacy与可持续性。New Lab的多样性（不同信仰、事实认知）非但不是弱点，反而是创新的必要条件。
在与OpenAI、DeepMind等Frontier Lab的竞争中，小团队的结构性优势在于：单位资源下的创新效率更高，且能实现大公司难以复制的组织文化。正如OpenAI当年也曾是Google旗下的“黑马”——曾濒临发不出工资，却最终颠覆格局。历史并非线性进步，而是螺旋上升+局部扰动的动态过程。访谈者强调：“There is always a way”——这并非理性推导，而是一种信念，也是吸引如Humans & AI联合创始人（Google七号员工）等资深人才仍愿倾注全部热情的核心原因。
“你有你有可能说这是非常不负责任的，就是为什么这个呃一些可能说 pension fund 一些大家的退休资金，最终通过好几层的投资到了这个私有市场，去给这一些有想法的研究者去满足他们的好奇心呢？”
终局想象与代际特质：当AI成为数学家的‘新器官’
访谈者描绘的终极愿景，是实现莱布尼茨式的universal representation theory——即“所有你能表示的东西，你都能表示”。更具体地说，他期待一个未来：顶尖推理能力成为默认状态，且具备自我验证能力。这不仅是技术目标，更是一种认知范式的跃迁。
他进一步引入Jevons Paradox（杰文斯悖论）来思考AI对数学产出的放大效应：当工具变得高效，人类使用量反而激增，从而催生远超个体总和的理论产出。历史上，从算盘到微积分、从Babbage引擎到现代密码学（如Victor Miller基于纯数学的椭圆曲线密码学），“无用”的纯数学总在数十年后成为关键技术基石。高斯曾言数论“如金子般美而无用”，却在百年后支撑起整个互联网安全体系。
关于代际特质，访谈者作为零零后女性CEO，坦承自己最快乐的状态是作为research scientist而非CEO——她将自己定位为“inter”（中间态）：既非纯粹学者，也非典型管理者。这种身份的模糊性，恰恰构成其领导力的独特性：不因事情本身而创业，而是因事情需要而行动。她曾因想做一道数学题，召集团队分工解题，却被资深工程师提醒：“你是个CEO，他们会觉得这是正经事”——这个笑话揭示了组织中角色标签如何扭曲任务优先级，也反衬出她对“本真性”的坚持。
“我现在是从事情中……让你最burning的是对终点是什么？……让推理能力成为最顶尖的推理能力，成为一个默认状态的一个这样的一个情况。且是能够自我验证的推理能力。”
CEO视角：从亲力亲为到放手的文化建设
在Action初创阶段，我曾设想亲自组织团队分工推进AI for Math项目——比如让数学背景的同事各领二三十道题，形成系统性攻坚。但一位资深工程师的一席话让我意识到问题：当CEO将某个项目表述为“正经事”，它就立刻被团队提至最高优先级，哪怕它本质上只是个side project。这让我反思自己角色的权重——技术领导者的一言一行，会深刻塑造组织对“重要性”的判断。此后我选择更“hands off”，转而聚焦于构建一种bottoms up的创新文化：公司由技术人员主导，他们是真正的主干与锚点；而我作为CEO，并不强加个人对低层级问题的信念，反而为多元想法留出空间。
“你是一个CEO，所以你跟他们讲的时候，他们就会觉得这是一个正儿八经的一件事。我真的要去把这个当做我的前几件事情去做。”
这种文化也体现在物理空间中：我们的会议室以数学家命名——高斯、庞加莱、希尔伯特、Loveless、图灵。命名过程曾引发激烈争论：有人坚持图灵必须入选（“Shugo甚至说‘如果你不给图灵，我就走了’”），也有人强调应补上Noether等女性数学家。最终取舍标准清晰浮现：我们倾向选择跨领域的Polymath（通才型数学家），而非像拉马努金这样专精数论的天才——因为AI for Math的目标，是培养“无领域偏置”的智能体，而非复刻单一方向的突破。
数学家群像：直觉、遗产与AI的边界
若能与历史数学家共进晚餐，我首选Erdős——他讲述组合数学时生动易懂，性格古怪又真诚；Grothendieck虽令人神往，但因我代数几何基础薄弱，恐难充分汲取其思想深度。这些人物之所以鲜活，正因他们不仅是解题机器，更是有温度、有风格、有社群联结的“人”。我曾作为硕士生参加Heisbrow的生日峰会，听Ben Green、James Maynard轮流讲述其学术遗产——这种传统，是数学文化中不可替代的部分。
“AI会把数学的很多证明可能能够帮数学家们快速解决，但是这个猜想、直觉以及构造……数学家们仍然会有非常多的乐趣，他们仍然是智力的灯塔。”
因此，即便AI能高效完成验证与部分证明，直觉、猜想生成与创造性构造仍是人类数学家的核心疆域。我甚至认为，当前许多解析数论工作只是对圆法、筛法等成熟工具的熟练套用；而真正的“直觉”，或许指向一种尚未被形式化的、更高阶的推理机制——这可能是未来五到十年的关键挑战。数学的永恒魅力，正在于它永远有“难倒AI”的问题：数学家的遗产不会被磨灭，反而会持续成为人类智力的灯塔与挑战。
学徒心态：在探索中寻找意义与快乐
我曾因无法成为职业数学家而失落，甚至哭泣；但如今我更愿称自己为“学徒”——在数学、物理、神经科学、AI、法律等领域持续学习。法律中的反垄断与合同法，因其严密逻辑，让我感到与数学的亲近；而宪法、庭审等则展现另一种“讲故事”的艺术。学习本身，而非身份标签，才是我最珍视的体验。
人生最快乐的几个月，是初识GitHub、逐篇精读AI for Math论文的时光；如今与舒博及早期论文作者并肩作战，更添这份喜悦。当人与事达成统一——既有战友的联结，又有共同目标的驱动——创业便有了意义支点。作为CEO，我深知“乐观主义需被谨慎收起”，对人负责；但我也相信，当人与事冲突时，往往反映的是自身认知的局限。
“热爱数学就是看到了上帝的面容。”
这句话源于十六岁的信念：数学是探索基本真理的路径。创立Action时，我在斯坦福教堂下奔跑，阳光穿透壁画上的天使与十字架——那一刻的灵性震颤，让我思考：若智力遗产可乘以一亿，你是否愿为之登月？这当然掺杂着ego，但更是一种对“unlock”的深切渴望。即便最终由他人完成，只要AI for Math成真，便是值得。
至于墓志铭？我不执着于它。“学徒”二字或许最贴切：愿在尽可能多的智力领域，继续学下去。
冲突中的作者性与责任
在 CEO 角色中，当人（如员工、实习生）与事（如业务目标、技术路径）发生冲突时，洪乐潼强调：任何乐观主义都应被谨慎取代，决策必须经过深思熟虑，因为你最终要为结果负责。但更深层的反思是——冲突本身往往并非源于外部情境的不可调和，而是自身能力或判断的局限所致。即便面对一位陌生员工，其困境也常是管理层一系列决策层层传导（trickle down）的结果。因此，他提出“authorship”（作者性）这一核心信念：你是自己人生篇章的书写者，不能将选择归咎于情境；相反，你有能力重构情境，避免非此即彼的僵局。
“你不能够觉得说，就是一个情境它就能够决定你的一个决定，是你决定让这个情境决定你的决定的，所以你也可以决定用其他一些方法去使这个情境不要这么走。”
“他到走到冲突的那一刻，一定是因为你自己本身曾经有做过一些错误的决定。”
AI 与数学：新公理、新世界与新合作
当被问及若 AI 在证明中引入全新但合理的公理（如超出 ZFC 的体系），是否应被接受时，洪乐潼持开放态度：只要该公理被数学共同体视为自然，就会被接纳。他指出，类似情形已在现实中发生——例如 DeepSeek Prover 曾因“作弊”（隐式使用未声明公理）高估性能，说明 AI 正在探索数学中尚未充分开发的领域。他类比代数几何与组合数学的融合，推测未来可能出现如“probabilistic analytic combinatorics”等交叉领域，而数学作为人类文明的构造，其边界本就可协商、可拓展。相较之下，物理定律的新增更难被接受，因其触及客观世界约束；而数学公理的增补，本质是语言与工具的演进。
“如果这个公理大家觉得是自然的，大家就会接受它。”
“这个其实是数学某种程度上是一个是一个人类文明的一些构造，所以我觉得大家是可以的。”
中国 AI 生态、未来预期与生活直觉
谈及中国 AI 发展现状，他高度肯定如豆包（Seed）、Kimi、MiniMax 等团队的执行力与技术实力，尤其赞赏其在 RL-based formal proving 等方向的快速突破。但他也提醒：学术的纯粹性在于信任与天真，而商业考量常遮蔽创新路径；理想状态应是工业界实践与学术开放性协同演进。对于 2026 年，他预测：首个持续学习（continual learning）小模型与强多模态推理模型将由小型实验室（如牛 lab）率先落地；而 formal verification tooling 作为 RL reward 的应用仍被严重低估。他个人押注于 system-level 创新（如 orchestrator、sub-agents）与递归自改进（recursive self-improvement）的实现，并强调：“I bet system, not model.”
“每一次我去就是在跟就是新希望能加入 Action 的同学聊的时候，就会觉得呃，未来无限好，未来无限希望……感觉像是两只鲸鱼又在找到了彼此的这个聊天频率。”