洪乐潼：数学直觉、形式化证明与 AI 数学家的可能性

张小珺在硅谷的 Facebook House 采访洪乐潼。洪乐潼是 Axiom 的创始人兼 CEO，探索 AI 与数学；本期既谈数学研究，也谈她的成长和创业经历。

洪乐潼说，融资常常意味着反复介绍同一个想法、回答相似问题；但在大量重复中，偶尔也会出现令人兴奋的对话，帮助创始人找到合适的投资伙伴。

张小珺问她有没有被数学“击中”的时刻。洪乐潼说，阅读别人的成果时，她常因不同数学领域之间出人意料的联系而感受到美。

她回忆在 Ross 数学项目中学习初等数论：每天完成题集才能继续，逐步走到二次互反律。简洁的结论背后可能有深刻而富有创造力的证明，这让她印象很深。

张小珺问数学究竟是什么。洪乐潼把它描述为人们约定公理、再从这些基础上构建理论的活动；她认为数学同时具有艺术与科学的特征。

在她看来，数学不只是解一道给定的题。研究者还会从例子、序列或集合中发现规律，形成猜想，再试图证明；选择什么问题本身也是创造过程的一部分。

关于数学是被发现还是被创造，两人提到这是长期争论。洪乐潼没有给出简单的二选一，而是讨论数学家如何凭共同背景形成直觉，并通过证明交流和检验新想法。

她以拉马努金与 Hardy、Littlewood 为例：背景不同的人可能发现不同的规律，而严密证明能让一个结果被其他数学家检查和接受。

她还谈到张益唐与 James Maynard 的数论工作。不同研究者可能使用不同技巧证明相关结果，后续数学家可以比较、整理并简化这些方法。

洪乐潼说，自己曾希望拥有天才式直觉，但常觉得自己更依赖耐心和蛮力。面对不擅长的几何题，她会用自己更熟悉的代数表示寻找解法。

她举 AlphaGeometry 为例：把几何关系转换为符号形式，再借助计算寻找证明。她认为机器的具体方法与自己的做法不同，但都有把问题转换到另一种表示的思想。

在 MIT 时，她曾长期思考教授给出的球堆积相关问题，连续数月没有结果，仍每周汇报尝试。她认为，愿意处理艰苦、漫长的工作也能与其他人的长处互补。

张小珺问 AI 是否也是蛮力型选手。洪乐潼说，一个系统可以组合不同模型：有的负责提出大致方向，有的负责大量搜索、细节检查和证明。

她回忆一道存在简洁人类解法的题，机器却给出了很长的形式化解法。比较人和机器采用不同路径得到证明，可能帮助研究者理解各自擅长什么。

她区分自动定理证明（ATP）和交互式定理证明（ITP）：在深度学习兴起之前，计算机科学家和数学家就已研究如何让程序帮助检查和构造证明。

在洪乐潼的描述中，AI 可以承担交互式证明中原本由人完成的一部分工作，而规则系统仍负责验证形式化步骤。她把这一方向视为既有证明工具与 AI 的结合。

谈到广州的童年，她记得家乡美食、离家很近的学校，以及走路时会因为想数学题而不知不觉走远。她说，这种自由游荡和思考的状态让她快乐。

她引入创业导师提到的两个概念：受任务和期限约束的注意力，以及能够自由探索的注意力。日常邮件和待办需要执行，但它们也可能占满思考的空间。

洪乐潼认为，自由注意力可能帮助创业者和数学家发现新的方向；如果每天只计算完成了多少任务，就可能失去这些机会。她并不认为两种注意力必须固定按某个比例分配。

灵感也不是投入时间后立刻按比例出现。她说，自由思考留下的线索可能过一段时间才与正在处理的任务发生联系。

她借用三种创业者类型说明团队差异：提出方向的人、擅长执行的人和善于沟通影响的人。她认为这些是帮助思考的分类，团队既需要互补，也需要共同语言。

谈到自己，她觉得自己更接近提出方向的一类，也承认对目标常常非常乐观。张小珺追问知名企业家的风格，她的回答是个人观察而非严格分类。

洪乐潼说，Axiom 早期成员中有不少来自 Facebook，他们熟悉的协作方式影响了新公司的文化。她重视团队成员之间既有共识、也能互相补足。

回到广州成长经历，她说自己小时候喜欢历史、文学和数学竞赛。家庭与北京文化的联系，也让她接触到许多作家和艺术家的故事。

她说自己并不是教练眼中最刻苦的学生，但碰到特别感兴趣的题目时，会长时间与它较劲。她区分了机械地投入时间和被问题本身吸引。

初中时，她开始主动读微积分等更高等的数学。相比竞赛排名，她觉得探索数学知识不必是零和游戏，可以和同学共同深入自己感兴趣的问题。

但竞赛规则仍会影响选择：她喜欢数论，拿到试卷可能先钻研最后一道难题，即使按照得分策略，先完成自己不擅长的几何题更合理。

她喜欢的数论题可能占去整场比赛的大量时间。这个例子让她看到，追求有趣的问题与优化考试分数有时会产生冲突。

张小珺问她是否好胜。洪乐潼回忆，小时候竞赛培训中不断按成绩重新分班，让她感受到强烈竞争压力；到了初中，她开始有意识地不把排名当作唯一目标。

她没有完全离开考试，而是降低对排名的关注，同时寻找也愿意读课外数学的朋友。这样的同伴让她可以把好奇心发展成共同探索。

她回忆与三到五位朋友研究棋盘上的马步问题：能否不重复地走遍格子，并为更一般的棋盘构造证明。他们分头尝试小规模情形，互相传递发现。

这个经历让她想到合作式数学研究：大问题可以拆成子任务，由多人分别处理，再把结果组织起来。它与只强调某位天才独自完成证明的叙事并不一样。

她和朋友当时在课堂上传纸条，分享找到的棋盘构造。共同解决问题的快乐，对她来说比一个人的排名更有吸引力。

她认为阅读更广的数学可能间接帮助了竞赛，但也承认后来在 MIT 学习时，自己需要练习更专注。她不认为“怎样学好数学”有一条适用于所有人的公式。

在 MIT，她常把同学视为比自己聪明的人，也因此觉得能与他们一起学习很幸运。这是她对自己当时处境的主观感受，并不需要当作能力的客观排名。

她原本考虑进入量化金融，也拿到了实习机会。疫情期间，她同时申请小野肯教授面向本科生的数学研究项目，先进入候补名单，后来获得参加机会。

她决定把那个暑假用于数学研究，金融实习则留到之后。回头看，她说当时最大的感受是珍惜这次可能改变方向的机会。

谈到家庭，她说母亲曾担心自己数学不好，因此鼓励女儿早点接触数学。洪乐潼认为，早期引导与后来自己对问题的兴趣共同影响了她。

面对外界列出的竞赛荣誉，她说自己也经历过大量不如预期的尝试。一次集中准备后没有被选上，让她对“荣誉”和个人感受之间的差距有复杂体验。

她说，乐观有时意味着为自己设定很高目标，因此主观上也会经常感觉失败。外界看到的结果与她自己的期待并不总是一致。

她以 MIT 新生的成绩保护制度为例：学生可以尝试更难的课程，不必一开始就把每一次成绩当成永久记录。她住的东校区也聚集了许多热爱动手和解决问题的同学。

学长学姐建议她选最难的课，即使预备知识还不充分。她和几位大一同学报名博士概率论，第一天就遇到陌生的测度论，大家面面相觑。

这次困难与独自参加竞赛不同：几个同学可以一起承认自己不懂，再组成小组研究题集。洪乐潼说，这种合作让她觉得有意思。

期中考试满分四十分，她只拿了四分。她意识到自己的分析基础需要加强，于是重新学习之前接触过的实分析材料。

张小珺问她从哪里获得继续学习的动力。洪乐潼说，年轻时重要的奖励来自同伴感：大家决定共同面对难题，而不是分别放弃。

小组期中成绩不理想后，他们讨论一起退课还是继续，最后决定继续。洪乐潼说，那种“我们一起没放弃”的感觉本身就是奖励。

她把后来对困难工作的投入称为一种可能不太健康的习惯，并质疑把创业者的痛苦简单等同于商业成功的说法。

疫情让 MIT 的同学离开校园，她失去了原先每天一起学习的小团队。她说，自己因此不得不尝试从困难的事情本身寻找乐趣。

她欣赏 MIT 同学展现出的毅力，但也承认自己未必能达到想象中的标准。周围人的坚持对她有感染力，影响了她面对长期任务的方式。

压力也会考验人际关系和团队。她认为，既能保持专业上的坚持，又能帮助同伴继续前进，是一种很难得的能力。

谈到领导力，她更喜欢服务型的比喻：团队登山时，领导者不一定是拿喇叭走在最前面的人，也可以是留在后面递水的人。

对于她来说，高等数学像搭积木：引入定义后，可以与已有概念组合，发现新的定理和问题。探索的空间不必受一份考试大纲限制。

她从高中起就特别想去 MIT，甚至会在数学草稿纸上写学校的名字。电影、数学家、物理学家和宇航员的故事，都构成了她对那所学校的想象。

本科选择数学与物理双专业：数学是早已确定的方向，物理则部分来自对量子问题的兴趣，以及她在概率研究中反复听到的物理联系。

谈到大学获得的奖项，她说不少来自教授提名和鼓励，而非一次单独的竞赛。她尤其记得教授愿意为学生寻找适合其兴趣的研究机会。

对于摩根奖，她强调提名、推荐与评审过程，也认为许多同龄研究者同样优秀；最终谁获得表彰，包含一定偶然性。

她提醒，获得奖项并不意味着其他候选者不够优秀。研究共同体的支持、评审选择和机会，都可能影响谁最后被看见。

她继续研究数论，涉及模形式和椭圆曲线，并与小野肯教授及暑期项目中的合作者共同写论文。她说自己一直在寻找最感兴趣的数论方向。

硕士阶段她去了牛津学习神经科学，部分原因是家庭经历让她想了解大脑。接触实验要求后，她意识到自己更愿意走计算研究方向。

计算神经科学与 AI 的交叉吸引了她：既能使用数学工具，也能与不同背景的研究者合作。她发现自己在 AI 相关问题中获得更多乐趣。

她描述硕士研究中使用线性代数、矩阵运算和微分方程等工具。为了满足神经科学学位的要求，她与导师一起把 AI 研究问题放进相应的研究背景。

之后她回到斯坦福继续数学博士，同时探索法学。她说，延后入学的数学机会和罗德奖学金让这些经历得以衔接；从小对辩论的兴趣也影响了她选择法律。

洪乐潼说，自己在不同学科有突出的兴趣，也有明显短板。她不把跨学科学习理解成“什么都擅长”，而是不断寻找不同工具之间的联系。

法学院对宪法解释方式的讨论，启发她思考 AI 是否能帮助处理结构明确的文本与规则。她尤其关注如何精确定义问题，而不是把模型输出直接当成权威判断。

在讨论法律文本时，她对解释方式之间的差异很感兴趣。这个经验让她更注意：即使文字看似明确，输入材料和解释规则的选择也会影响结果。

一位长期从事 Lean 形式化证明的朋友让她看到，数学表达可以写成计算机能够检查的形式。她开始想：如果 AI 能帮助处理规则化的语言，是否也能辅助数学研究？

在帕洛阿尔托的 Verve 咖啡馆，她与后来合作的书博反复聊科学和技术。她回忆，最初只是去读法律材料、喝抹茶、看院子里的狗，关系是慢慢建立起来的。

她希望 AI 帮数学家处理大量标准但繁琐的工作，例如检查许多可能性或把已知工具用于新问题，从而把人的时间留给更重要的思考。

她把这个想法放在自己当时的研究经验里：数学中有些工具可以迁移到一系列问题，熟练运用它们却需要大量时间和专业训练。

读法学院时，她喜欢通过大量阅读拓展视野，同时又想念数学和科学。于是她常坐校车到咖啡馆，与书博继续没有预设结果的讨论。

两人的相识始于一个很小的日常请求：咖啡馆里阳光刺眼，需要拉窗帘。随后他们发现彼此对数学和科学都有兴趣，逐渐成为朋友。

他们的聊天持续了一年多，主题包括数学、科学史和技术。洪乐潼认为，没有急着把关系变成商业合作，反而让双方有时间了解彼此的思考方式。

洪乐潼说，两人认识很长时间后，才逐渐了解彼此的具体工作背景。她珍惜这种先从共同兴趣建立的关系，而不是一开始就为了职业目标而结识。

2024 年秋天，她开始认真考虑把 AI 数学项目做成公司。她和书博在咖啡馆用餐巾纸估算所需的计算资源，觉得单靠学术环境可能难以承担。

洪乐潼说，自己先开始筹资，后来拿到工作签证才离开学校。书博最初仍在 Meta 工作，两人并不是从第一天起就确定一起创业。

她说自己很向往学术生活，曾花两个月劝自己不要创业。她反复追问的不是这个方向是否热门，而是自己是否真正理解问题、是否有办法把它做出来。

为验证想法，她读科学史和 AI 数学方向的大量论文，也试着在纸上推演系统设计。她认为，向投资人争取资源之前，自己有责任先了解技术风险。

她甚至询问过另一家相关公司的招聘机会，因为如果能加入别人做同一件事，也不一定需要自己从零创业。对方当时的招聘要求与她的背景并不吻合。

读论文的过程让她认识了自动证明、寻找数学规律等不同研究方向。她说，后来有些当时论文的作者也加入了团队，这让她很珍惜共同工作的机会。

张小珺说，这像是她重新形成了一个小团队。洪乐潼介绍团队既有机器学习与代码生成研究者，也有数学家、Lean 语言和数学库的贡献者。

Lean 是形式化语言，Mathlib 则是建立在其上的数学知识库。她强调，除了数学知识，构建工具、训练模型和工程实现也需要不同专长。

节日期间，她和书博组成远程阅读小组。尽管两人平时都不喜欢长时间视频会议，讨论论文时却经常聊上几个小时，发现彼此的思路既相似又互补。

她说，团队早期曾讨论减少数学家的比例，后来更重视找到思想开放、愿意同时考虑规模和方法效率的数学家。她希望数学专家帮助发现系统的弱点。

她提到团队曾遇到对规模化方法持保留态度的数学研究者。她并不把数学背景视为障碍，而希望找到愿意探索不同方法、也能质疑系统结果的人。

数学家可以设计更有挑战性的基准，检验系统在哪里失败，而不是仅凭团队已有的测试判断进步。洪乐潼把这种对抗性评估视为团队互补的一部分。

假期里一篇形式化定理证明综述帮助她把分散的方法连成整体。她逐篇核对参考文献，发现仍有不少自己还没读过的工作。

她说，硅谷研究者在学界、工业界、顾问和创业者之间流动，容易让不同经验的人围绕问题交流。她认为有价值的是共同做的事情，而不只是头衔。

两人讨论如何把提出猜想、自动证明和更早的专家系统研究联系起来。洪乐潼希望在资源允许时，把这些方向组织成一个可持续试验的系统。

她把 AI 数学研究放在更长的历史中：规则系统、早期定理证明、AlphaGeometry 和 AlphaProof 等工作都为后来的系统提供了背景。

她认为 2024 年 AlphaProof 在国际数学奥林匹克竞赛上的表现是重要节点，也说 Axiom 后来对普特南题目的工作建立在这一研究序列之上。

筹资开始后，她发现不同投资方陆续提出报价。她说自己最初并不熟悉融资，也不愿接受会让创始团队承担过高稀释的条件。

她形容融资最累的部分是反复讲同一件事、回答相似的问题。但偶尔也会遇到真正理解方向的人，那些讨论会让她感到兴奋。

她回忆与 B Capital 的 Howard Morgan 对话，认为对方能理解数学和技术潜力。她把投资伙伴是否提供长期理解和帮助，看得和价格一样重要。

推介时，她坦言商业模式还不确定，团队首先想把技术做出来。她后来意识到，投资人对创始人的乐观叙述有自己的折扣方式，沟通风险也需要考虑表达背景。

她说，一些投资人没有直接拒绝，而是等待其他人是否领投。她从中感受到融资中的群体心理，以及找到愿意作出决定的领投方的重要性。

多个报价之间，她继续评估稀释、估值和投资者的长期支持。她强调自己是边做边学，并非一开始就懂得如何安排融资。

融资和建立公司期间，她仍在上课并招聘团队。后来工作签证获批，她在夏天离开学校；签署投资条款之后还要经历法律尽调、办公室和招聘等实际工作。

她回忆种子轮筹资约 6,400 万美元，并说明这笔资金要服务模型、系统与团队建设。融资数字反映的是她在访谈中描述的当时情况。

被问到身份和年龄，她说自己没有明显感受到华人女性身份的加减分，但年轻和缺少大型技术团队管理经历，可能让投资者对深科技项目有所顾虑。

她认为创业者常要在时间有限、信息不完整的情况下反复作重要决定。等待更多信息有时有价值，也可能错失机会；她形容自己仍在学习承担这种不确定性。

她回忆自己在重要决定前常感到准备不足。更多经验可能有帮助，但现实中的决定往往不能等到所有信息都齐全才作出。

她用第一次玩高空滑索作比喻：明知已经系好保护，迈出第一步仍然困难。她说有些创业决定也有类似感受，但不是每个风险都可以忽略。

招聘是一例：优秀候选人可能同时收到多个报价，小公司需要在资源有限时作出取舍。洪乐潼说，这类决定常常没有完全确定的答案。

她介绍后来 A 轮融资的过程：原有投资者提出提前投资的意向，团队随后比较了不同方案。她说最终选择了能够提供长期支持的领投方，同时也让其他支持者参与。

她将投资人对团队的信心，归因于团队在短时间内搭建基础设施、训练模型和构建验证工具的执行力。这是她对投资决定的解释。

洪乐潼介绍公司报告的进展，包括普特南题目和若干研究问题的形式化证明。她的说法涉及特定评测和系统设置，不能据此推断 AI 已解决一般数学研究。

被问到资深团队为何愿意由她担任 CEO，她说自己更希望为研究者创造环境，让团队集中解决共同的问题，并把自己的角色比作给登山队递水。

她说，公司面临的不只是训练模型：Lean 数据有限，形式化语言和验证工具本身也有工程挑战。团队需要同时改进数据、搜索、工具和计算效率。

她举验证为例：证明检查不仅要看代码能否运行，还要确认陈述与假设是否对应原题。一个形式上通过的证明，如果修改了前提，也未必回答了原问题。

资源限制也影响搜索方式。洪乐潼说，团队比较不同系统设计，既要控制计算成本，也要在快速推进后补足基础设施的欠账。

张小珺问小野肯如何加入团队。洪乐潼形容这位导师像一位乐观的篮球教练，既给人鼓励，也能帮助团队找到值得研究的数学问题。

她说，自己过去不敢主动邀请资深研究者，更希望对方了解项目后自主决定。书博表示愿意一起做时，她感到高兴，因为独自推进这件事有些孤单。

小野肯后来发邮件谈到自己的职业选择，洪乐潼提出也可以考虑 Axiom。她回忆，两人很快就团队和研究方向展开讨论。

她猜测团队对数学的专注、以及已有数学研究者的共同语言，对他的决定有吸引力；她也明确这是自己对他动机的理解。

她认为小野肯擅长构建理论、连接不同领域，并提出值得其他人继续解决的问题。除了自己的研究，他长期指导年轻学生，也是她所重视的导师。

被问到 AI 是否会取代数学家，她转而设想人和工具在不同抽象层面合作：数学家提出方向和判断问题价值，系统帮助探索与验证。她强调这是一种未来愿景。

她举编程抽象层变化作类比：工具变化后，人可以在更高层讨论问题，但仍需要理解和检查底层结果。她认为数学家也可能逐渐调整分工。

她希望猜想系统与证明系统能够形成反馈：新问题交给证明器检验，得到的证明和失败经验再帮助后续探索。能否有效形成这种循环仍需实验。

团队尝试让已解决的证明和搜索经验成为后续工具或训练材料。洪乐潼希望系统能逐渐积累能力，但这仍是研究目标，需要持续检验效果。

她回忆团队在 2025 年普特南竞赛题目公开后，将题目转为形式化陈述，再交给系统证明。题目转写和某些需要求具体答案的环节当时有人参与。

团队一度决定是否公布已经得到的部分结果，最终报告十二题均得到形式化证明。她说，竞赛式题目与研究数学的难度和评估方式并不相同。

当时团队先以为部分题目必须由人求出答案，再交给系统验证；后来他们发现系统中的非形式化模型也能提供这些答案。她把这一点作为当次流程的事后观察。

Axiom 取名来自“公理”。洪乐潼喜欢从有限的基础规则推导出新结果的意象，也将其与形式化证明中的定义和逻辑联系起来。

她设想 AI 可能扩大可用于数学研究的能力，让数学家更集中地选择重要问题、提出直觉和分配研究资源。这是她对未来的乐观看法，不是已实现的结果。

如果计算资源有限，她认为判断问题的重要性仍很关键；如果未来资源和方法大幅改善，研究者或许能探索更多今天没有精力处理的问题。

洪乐潼认为纯数学和应用数学相互依赖：基础研究中的工具，可能在许久之后用于科学、工程或其他领域。她反对只根据眼前应用衡量基础数学的价值。

她把数学证明、程序和现实实验视为不同形式的反馈来源。形式化验证能检查明确的逻辑性质，现实应用仍要考虑模型、规格和环境是否对应真实需求。

张小珺问 AI 数学是否会迎来类似 ChatGPT 的时刻。洪乐潼认为，仅有技术演示不够，要让能力真正服务用户，还需要产品和可用的工作流程。

她区分竞赛数学和研究数学的里程碑，也提到自然语言证明与形式化证明是不同输出。评价一项结果时，需要看问题、验证方式以及人参与的程度。

她介绍一种“草稿—形式化提纲—证明”的流程：先提出思路，再写成形式化结构，最后填补尚未证明的部分。中间的占位符本身不等于已经完成的证明。

填补证明时，系统可以使用传统规则工具，也可以调用神经网络。洪乐潼说，便宜而可靠的确定性方法能解决的部分，应当先用这些方法处理。

她讨论 Lean 中的自动化工具，认为社区已有的规则方法常能解决一些看起来复杂的步骤。AI 的作用应放在整个工具链中评估，而不是把每一步都归功于模型。

另一个方向是让多个子任务并行探索，并从搜索路径中积累经验。她把子智能体和工具使用描述为正在尝试的系统设计，而不是已经证明优于所有替代方案。

她说团队观察到数学证明能力向代码验证任务迁移的迹象。由于比较依赖基准和实现细节，她把它作为一个值得继续研究的发现。

在她描绘的 AI 数学系统中，预训练模型、后训练、工具和验证器共同工作。不同团队在搜索、数据和系统结构上可能采用不同方法。

她认为除了证明器，还需要能够提出猜想的系统。证明器提供的反馈可以帮助筛选，但一个猜想即使可证，也未必重要或有数学价值。

如何衡量猜想的新颖性、优雅和意义，仍是困难的研究问题。她提到一些粗略的过滤方法，并指出它们未必能扩展到更高级的研究数学。

知识库也是关键：大量人类数学尚未写成 Lean 中可直接使用的定义和定理。系统需要知道已经证明了什么，也要能够查找可能推翻猜想的反例。

自动形式化不仅是翻译词句。把一篇论文拆成足够细的定义、引理和依赖关系，再写成机器可检查的形式，本身就是困难工作。

她提到数学家为大型形式化项目手写证明蓝图，再由许多参与者完成各个部分。如果要让系统自动构建这样细致的蓝图，就需要可靠的分解与推理能力。

把形式化内容转回自然语言也需要检查是否改变含义。她提到往返转换可以作为一致性检查之一，但这种检查本身不能保证翻译完全正确。

张小珺问数学与编程在执行任务时有什么区别。洪乐潼说，程序产生输出，证明可以检查明确的性质；两者互补，关键在于把需求准确写成规格。

她设想生成程序时同时验证其符合规格，而不仅检查有限的输入输出案例。但规格写错、遗漏需求或没有形式化定义时，证明并不能弥补这些问题。

她以研究数学题为例说明限制：如果题目所需概念尚不在形式化库中，系统可能连题目都难以准确表示，更不用说证明。

她认为数学能力向其他任务的泛化可能比垂直领域的进展更慢、也不那么戏剧化。数学、代码和硬件验证之间的联系值得研究，但不能假设所有能力都会一起提高。

她用排序程序说明规格的重要性：有限测试可以帮助理解需求，但即使所有测试通过，也不能单独证明程序在所有允许输入下正确。

她提到芯片和软件验证作为潜在应用：这些领域需要检查系统是否满足明确性质。她认为形式化工具可能帮助专业人员，但并不消除定义性质和理解系统的工作。

对于商业化，团队想一边增强核心系统，一边探索哪些验证问题能解决、哪些不能。洪乐潼认为，理解有意义的失败比收集表面成功更有价值。

她认为自然语言与形式化证明可以互补：自然语言适合沟通需求或提出提纲，形式化语言则有助于严格检查某些证明步骤。

系统中的不同模型经过不同的后训练，部分专门生成 Lean 代码。她希望把理解用户意图和机器可检查的输出连接起来。

她希望验证减少数学任务中的幻觉。但形式化检查只能确认形式陈述在给定假设下得到证明，仍须检查翻译、假设和题目是否忠实对应。

在她看来，提出猜想与验证猜想是一个来回过程：生成可以探索可能性，验证则排除不成立的路径。不同的生成方法也可以来自数学结构，而不只来自自然语言。

团队下一阶段希望尝试更多研究领域，尤其是形式化基础还不充分的领域。洪乐潼说，研究级基准难找，也需要数学家帮助提出值得试验的问题。

如果一个领域的基本定义不在数学库中，系统可能无法写出命题。她认为，自动建立和扩展知识库是比解一道已有题目更基础、也更困难的问题。

自动生成定义还需要判断它是否忠实表达了人类原意，以及新增定义与既有体系是否协调。她把这些问题列为需要继续研究的限制。

谈到 AGI，她不愿把擅长数学的系统直接称为通用智能。她用扇形作比喻：某种能力可能扩展到相邻的代码验证或物理问题，却不必覆盖所有人类任务。

她提出自己对“专长型超智能”的说法，同时承认通用系统未来也可能覆盖相同领域。这个分类表达的是她的战略判断，并非已经确定的行业标准。

她希望研究中的证明工具最终成为更广泛系统的一部分，而不是宣称一个数学模型已经拥有所有领域的智能。其具体泛化范围仍有待验证。

她说，Axiom 希望同时吸引数学、AI 和编译器背景的人。不同专长组合后，可以从数据生成、证明搜索和软件工具等多个角度处理同一障碍。

Lean 数据稀缺，使完全依赖人工编写的数据扩张困难。她讨论用模型生成、修复和分类样本，并强调这需要工程与数学判断共同参与。

她把数学称为现实世界的一个沙盒：形式化问题有较清晰的反馈，而生物或物理实验往往还要处理材料、设备和真实环境。两类研究可以相互帮助，但验证方式不同。

她希望 AI 数学工具有一天能协助科学家处理理论问题，再由实验研究者在真实世界检验相关假设。这是对未来协作的设想。

张小珺追问，AI 能否不仅验证，还提出具有创造性的数学问题。洪乐潼认为猜想尤其困难，团队仍有不少失败，短期还需要加强自然语言到形式化表达的转换。

她认为提出好问题需要判断难度、意义和已有知识之间的关系，而不是随意生成命题。小野肯善于连接不同视角并提出问题，是她欣赏的能力。

两人谈到拉马努金的数学直觉，以及后来与其他数学家交流、证明和整理结果的过程。洪乐潼认为，直觉与证明可以相互促进，但它们如何产生仍有很多未知。

两人借预训练与后训练作类比，讨论数学直觉能否由经验积累、专项训练或二者结合形成。洪乐潼承认，这个问题目前没有简单答案。

她说，团队当时没有计划从零进行大规模预训练，主要使用已有模型并开展后训练，也可能探索中训练。成本和数据条件影响这一选择。

大型实验室与专门的数学公司可能采取不同路径。洪乐潼认为，双方既可能竞争，也可能在工具和专长上合作；她对其他公司内部计划的描述仅是个人观察。

她认为最大的挑战之一是执行速度与学习时间的平衡。创业事务越多，留给阅读和研究的时间越少，而过度追求速度又可能带来战略错误。

公司既要对员工和早期团队负责，也要坚持困难的研究目标。她把商业可持续性与科学雄心看作需要持续平衡的两件事。

她用登月作比喻，认为项目可能成功，也可能失败。这个比喻表达的是高风险研究的不确定性，并不意味着创业结果必然只有两种。

如果项目未能成功，她说自己仍对神经科学和人机交互感兴趣。不同领域的长期问题，对她的吸引力并不完全取决于一个公司的结果。

谈到硅谷竞争，她认为强竞争能推动快速进步，也可能让需要更长时间才能验证的研究被忽视。她希望小团队能为这些方向创造空间。

她设想，即使未来 AI 能解决极难的数学问题，人仍会想理解证明、比较方法并提出新问题。对她而言，好奇心和数学社区不会因为工具进步自动消失。

她也承认，高风险研究失败会影响投资者和更广泛的资金来源，因此如何负责任地投入并不是一个可以回避的问题。

面对大型实验室，她认为小团队的机会来自专注、执行效率和人才组合，但也承认资源差距真实存在。这是她对竞争位置的判断。

小公司与大公司的资源、人才密度和组织结构不同。她认为创业团队应寻找自己能做得更好的问题，而不是假设规模差距不存在。

张小珺问她如今从事情还是从团队获得动力。洪乐潼说，问题本身带来向前的冲动，团队则提供支持和安全感，使她保持脚踏实地。

她的长期理想是让更强的推理能力更容易获得，并能在适当条件下被验证。她把它描述为一个研究方向，而不是当前系统已经具备的能力。

她想象，如果数学工具变得更容易使用，更多科学家可能提出和探索原先没有资源处理的问题。但这种潜力仍取决于工具的可靠性和实际应用。

洪乐潼说，自己最自在的角色其实更像研究实习生：可以学习、提出不成熟的问题。她创业主要是为了推进想做的事，而不是为了成为 CEO。

她讲过一次管理教训：自己以为只是提议一个兴趣项目，年轻同事却因为她是 CEO 而把它当成高优先级任务。此后她更注意自己的话对团队的影响。

公司会议室以数学家和计算机先驱命名，选择过程甚至引发热烈讨论。团队偏爱在多个领域工作的研究者，也希望纪念不同背景的贡献者。

她尤其喜欢高斯在数论和解题方面的贡献。若能与历史上的数学家共进晚餐，她觉得与 Erdős 聊组合数学和他独特的生活方式会很有趣。

她珍惜数学家的社区、友谊与共同工作，也曾担心强大工具会让这些体验消失。后来她更相信，人仍会通过猜想、直觉和互相挑战获得乐趣。

她回忆数学家为同事举办学术庆典，学生和合作者讲述共同完成的工作。对她而言，这种关系和传统也是数学的重要部分。

她区分熟练运用已有证明工具与发明全新方法，并猜测后者对 AI 仍更困难。她提出的时间尺度只是个人预测，并不能视为进展保证。

她回忆跑步经过斯坦福纪念教堂时，想到数学家留下的知识以及扩大这种发现能力的可能性。她也承认，这个愿景中既有公共意义，也有个人雄心。

被问到希望如何被记住，她说标签没有经历本身重要。比起固定地称自己为数学家或创业者，她更愿意做一个不断学习的“学徒”。

她很喜欢学习一个新领域时从资料中逐渐建立全景的感觉。后来能与一些曾阅读过的论文作者并肩工作，是她认为很珍贵的经历。

当团队与任务发生冲突时，她认为负责人应谨慎处理，并反省是否有更早的管理选择造成了问题。她强调，涉及他人的决定需要承担责任。

推荐阅读时，她提到初等数论、Davenport 的解析数论，以及《红楼梦》等文学作品。她喜欢数学与文学带来的不同类型的理解。

张小珺设想 AI 使用新公理证明重大猜想。洪乐潼说，数学界需要明确区分原有假设与新增公理，并讨论新体系的意义；形式化通过不等于原命题无条件成立。

她赞赏中国研究团队在 AI 数学上的工作，也希望科学想法能够交流。对中美未来角色，她表示难以预测，研究者会基于各自情况选择工作地点。

对于 2026 年的技术发展，她提出关于持续学习、多模态推理、智能体和验证工具的个人预测。她将这些作为值得关注的方向，而不是已经证实的结果。

她说，与潜在同事讨论数学和 AI 时，常会重新感受到创业的初心。找到既有共同语言又能提出新视角的人，是招聘中令她快乐的部分。

她推荐关注自动证明和数学 AI 的一系列研究，也强调系统设计、工具和后训练的组合。她认为旧方法与新模型之间的联系常带来启发。

她强调自己的押注更偏向完整系统，包括模型之间的协作和验证工具，而不是只比较单个模型。递归自我改进等想法仍是她的预测。

谈到“语言及世界”，她想到数学家长期用自然语言表达严格推理，而形式化语言提供了另一种可检查的表达方式。两人以语言、逻辑和持续探索的话题结束访谈。