--- id: "bTxL01xq1W4" title: "Carina Hong（Axiom）——数学 AI 的前沿【完整演讲】" channel: "Stanford eCorner" host: ["Ravi Belani"] guests: ["Carina Hong"] date: "2026-11-03" updated: "2026-11-04" duration: "46:45" duration_seconds: 2805 source_type: "youtube" youtube: "https://www.youtube.com/watch?v=bTxL01xq1W4" canonical: "https://pod-exp.pages.dev/bTxL01xq1W4/" transcript_jsonl: "https://pod-exp.pages.dev/bTxL01xq1W4/transcript.jsonl" language: "zh-CN" translation: true translated_from: "en" timestamp_precision: "block" topics: ["人工智能","数学与科学","创业与经营"] series: ["AI 研究前沿"] --- # Carina Hong（Axiom）——数学 AI 的前沿【完整演讲】 > 中文译文，由英文原音字幕翻译整理，不是官方逐字稿；引用原话请核对英文原视频。说话人标签由整理者依上下文标注，带「未确认 / 未标注 / 不确定」等字样的标签不可靠。时间戳一般为块级（所在时间块的起点），不是逐句时间；正文自带 [hh:mm:ss] 的段落除外。 **内容提要：** Carina Hong 回顾了自己从数学、神经科学到创办 Axiom 的经历，并解释公司为何以形式化数学推理切入 AI：把数学证明转成机器可检查的代码，进而为 AI 生成内容提供验证层。她谈到有限单群分类证明的形式化、AI 在编程和科学研究中的潜力，以及两轮融资背后的技术进展。创业管理方面，她强调设定长期高目标、保持技术栈灵活、重视人才密度与情绪沟通。她也分享了数学训练如何培养分析力和专注，以及未来数学家、脑机接口和可训练智能体可能带来的变化。 ## [0:15] Carina Hong 的经历与创业转折 · YouTube **Ravi Belani：** 我特别高兴地宣布，本周的演讲嘉宾是 Carina Hong。她是 Axiom 的创始人兼 CEO。Axiom 是一家 AI 公司，正在打造能够自我改进的超智能推理系统，第一步从 AI 数学家做起。Carina 在中国广东长大。现场有人出生或长大在中国吗？（观众欢呼）看来大家对中国很热情。她也是家里第一代大学生，而且一鸣惊人：她不只上了大学，还去了 MIT；不只去了 MIT，还同时读了数学和物理两个专业，这可都不轻松。她在 MIT 本科期间获得了摩根奖，这是全球本科生研究领域能拿到的最高奖项。之后她作为中国代表，凭罗德奖学金去了牛津，取得神经科学硕士学位；她还在伦敦大学学院的盖茨比计算神经科学中心（Gatsby Computational Neuroscience Unit）学习机器学习。后来她来到斯坦福读研究生，原本要攻读数学博士和法学院的 JD，但不到一年、差不多一年后就退学创业，创办了 Axiom。Axiom 已从 Menlo Ventures 等基金筹集超过 2.6 亿美元风险投资。今天 Carina 来和我们分享她的故事。她今天身体不太舒服，但还是特地来课堂和大家见面。请大家热烈欢迎 Carina Hong。 **Ravi Belani：** Carina，欢迎回到斯坦福，很高兴你来了。 **Carina Hong：** 很高兴见到你。 **Ravi Belani：** 你在斯坦福读书时上过 ETL（Entrepreneurial Thought Leaders）吗？或者知道这门课吗？ **Carina Hong：** 知道，那是门非常有名的课。 **Ravi Belani：** 好。在聊 Axiom 的细节之前，我想先聊聊你决定离开斯坦福的那个时刻。之前我们谈过，你其实挺喜欢研究生阶段的学习，尤其是法学院的课程。能不能带我们回顾一下整个过程：你什么时候决定离开？是什么时候意识到自己真的要走？这个决定容易吗，还是很难？ **Carina Hong：** 我记得大概是十一月，那时我刚开始读数学博士。我已经看 AI for Math 的论文两个月左右了，大概从九月、十月到十一月，我对这个领域特别感兴趣。我觉得 AI for Math 会改变世界。GitHub 上有个收集了几百篇论文的仓库，我就先读摘要；摘要够有意思，我再去读全文。后来我意识到，自己上课时也只顾着在笔记本电脑上看这些论文，这就有点说不过去了。 **Carina Hong：** 后来我参加了一场 Knight-Hennessy 午餐会。演讲者 Julia Zhu——我记得她好像是 Facebook 最早的产品经理——讲到她写书的经历：她只是开始写，结果就停不下来。我当时问她，我也有类似的困扰，她就说：“跟着你的热情走，看看它会把你带到哪里。”于是我很快就开始筹款了。 **Carina Hong：** 抱歉，我今天有点不舒服。 **Ravi Belani：** 慢慢来。 **Carina Hong：** 谢谢。我开始筹款后，大概过了一个学期，就决定该退学了。 **Ravi Belani：** 好，别着急。喝点水、补充水分。也提醒今天可能身体不舒服的各位：补水、休息，生活还会继续。谢谢你分享这些想法。我觉得这确实是个很有用的判断方法：当你想开始做一件事，它抓住了你，让你着迷，甚至晚上睡不着、注意力总往那边跑，这就是个信号。并不是你单纯想当创始人，而是你爱上了 AI 正在数学领域引发的这些变化。所以你能不能…… ## [4:16] 形式化数学与可验证推理 · YouTube **Ravi Belani：** 对还不了解 Axiom 的人来说，一家数学公司第一次融资就拿到超过 2.5 亿美元，确实让人好奇：一家数学公司怎么能一下融到这么多钱？Axiom 是做什么的，为什么吸引了这么多资金？ **Carina Hong：** Axiom 做的是形式化数学推理：把数学转成机器可以检查的代码。这很有价值，因为 AI 正在生成大量内容，却缺少一层验证。昨天我们宣布，已经把有限单群分类定理形式化了。这个定理是人类写过的最大数学证明；没有别的证明比它更长。它太庞大，以至于没有任何一个人读完过。它汇集了几代人的 20 世纪数学成果。简单群的概念最早可以追溯到伽罗瓦；到了 19 世纪，有人提出家族里可能还包括五个左右的散在群；大约在 20 世纪 50 年代，布劳尔在著名的国际数学家大会上发起了分类所有有限单群的工作。整个证明超过 1.5 万页，散落在许多论文和书籍里。 **Carina Hong：** 我们的使命，是把大量数学成果，也包括其他领域的内容，转成机器可检查的代码。运行程序时，你就能确认它是正确的，达到百分之百验证。严格说，哥德尔会告诉你，任何东西都不可能让人真正确信；但这里是把庞大的证明归约到一个很小、可信的内核。因此它的正确性可以说“排除了合理怀疑”，除非发生非常重大的理论问题。最终，这个证明被写成了 Lean 程序语言里的五千多万行代码。 **Carina Hong：** 从商业角度看，这也很有意思：它是最大的开源软件项目，比 Linux 还大，也超过你能想到的其他开源项目。它用 Lean 这门编程语言表达的，其实就是一个定理、一个特别庞大的证明。昨天不少数学家说，他们觉得压在自己毕生工作和学术遗产上方的一团阴云终于散去了。 **Ravi Belani：** 从学术研究的角度看，这个证明的意义很深远。能不能谈谈，风险投资人为什么这么兴奋？ **Carina Hong：** 我想，首先是因为这件事以前从没人做成过。新兴技术总让人兴奋。关键是有了验证层之后，事情就不再只是“我有一段代码，请告诉我它对不对”，而是我可以生成新代码，立刻得到验证反馈。我觉得这会成为 AI 辅助编程的未来。 **Ravi Belani：** 所以变化在于：现在大家用 ChatGPT、Codex 或 Claude Code 来生成代码，思路还是由人来创造；而你们设想的是让智能体自己写代码，是这个意思吗？ **Carina Hong：** 我想是这样。现在大家其实不太信任测试。你看看新闻里的国家关键基础设施：铁路停摆，或者波音 737 因为严重软件漏洞不得不返航。这些系统都经过测试了。现在代码审查的力度，已经降到了历史最低点…… ## [8:17] Axiom 的价值层次与融资经历 · YouTube **Carina Hong：** ……实际上很多 AI 原生公司根本不做代码审查。我知道自己公司有些部分也没有代码审查，代码就这样上线了。我觉得这会带来问题；问题严重到一定程度，就会让 AI 部署整个停下来。所以这里大致有三层价值。第一层是技术直接创造的价值，主要是生成经过验证的代码，也有一部分是验证现有代码；虽然这部分听起来较小，其实也不小。第二层，是让更多机构愿意在市场规模很大、又很关键的领域部署 AI。让 AI 得以部署，本身就有价值。 **Carina Hong：** 第三层，如果你关心自动化研究，那就是 AI for Science：让智能体自主开展长周期的发现工作。这和经过验证的代码生成有相似之处，但更有意思的是，你可以让系统去处理数据。我觉得这会把 AI 从现有的信息提取和交换领域，带到物理世界，也带到材料科学、新分子等领域。第三层就是走出软件，进入物理世界——不只是硬件，而是更广泛的科学。 **Ravi Belani：** 这项技术基础性很强，能影响多个领域，我理解它的分量。不过我还是想知道，你是怎么做到在六个月内完成两轮融资、总共融到 2.6 亿美元的？当时你 24 岁，是独立创始人，没有联合创始人，对吗？女性独立创始人融资尤其不容易，更何况当时你只有学术背景，没有职业工作经验，是从学界出来的，对吗？ **Carina Hong：** 我第一轮融资时 CTO 加入了，所以确实分担了很多压力。 **Carina Hong：** 我觉得第一轮种子融资，核心是“AI 将改变数学”这个想法。当时也有其他公司在做形式化推理，但我们在技术路线和愿景上投入了很多思考。我们当时就很确定，不会采用单体式的训练搜索方法，而会把搜索放在推理阶段；后来事实证明这是正确的选择，其他很厉害的团队也采取了类似方向。 **Carina Hong：** 第二轮融资更多是因为我们看到了迁移学习的能力。我们做出的形式化数学证明器，在其他软件验证基准上也拿到了很高、很出色的成绩，这让我们自己都很意外。Putnam 数学竞赛的成绩也达到了满分。我觉得这说明它不只是会被“苦涩的教训”压过去；但要始终走在前沿，仍然是一场持续的较量。 **Ravi Belani：** 所以你们有了这些实质性的里程碑和成果，确实很重要。 **Ravi Belani：** 但有些人也拿出了实质成果，还是融不到资。你的融资方式有没有发生转变？融资过程容易吗？有没有哪个转折点让你改变做法，从而成功完成融资？ **Carina Hong：** 第一轮非常难，毕竟那时只有一个想法，我的融资幻灯片可能做得很糟。第二轮时有些东西变了：我把注意力集中在把公司建起来。 **Carina Hong：** 当你专心建设公司，就不会把太多精力耗在融资流程上，结果反而挺顺利。若一门心思只想着融资，可能会想太多，把流程拖长。后来我就专注于把公司做好…… ## [12:18] 融资策略与快速变化中的目标 · YouTube **Carina Hong：** ……我觉得等我专心把公司建起来之后，融资就容易多了。 **Ravi Belani：** 能不能把这件事讲具体一点，让大家明白？听起来有些反直觉：你越少关注融资，效果反而越好。能不能说说实际过程是怎样的？ **Carina Hong：** 第二轮时，我基本上想的是：我们种子轮融来的钱还没怎么花，没必要再融资。与此同时，很多风投对我们很感兴趣，有些主动找上门，有些直接发了条款清单，所以我们拿到了“抢先投资”（preemptive offer）。如果没有人抢先出价，通常就得一家家去敲门；有了抢先报价，就像是已经有个很诱人的条件摆在面前，而且我确实有兴趣接受。那我们就可以约定一个期限，免得流程拖个没完，导致其他报价也可能失效。所以如果这是一堂创业融资课，我觉得一个好建议就是：尽量拿到抢先报价。 **Ravi Belani：** 这个抢先报价是你刻意安排出来的，还是自然发生的？ **Carina Hong：** 是自然发生的。我大概看到了苗头，也试着促成它，因为在我们达到那个里程碑之前，就有人表现出想提前投资的兴趣。我当时觉得，在里程碑即将到来时就接受报价不一定是好事。首先，融资非常分心；其次，等一等，你可能会获得更多投资人的兴趣。 **Ravi Belani：** 如果你能给过去的 Carina 一条建议——关于如何完成那轮非常难的初始融资，你现在知道什么，是当时希望告诉她的？ **Carina Hong：** 被拒绝并不是世界末日。我觉得这是特别重要的一课。很多事情当下看起来很糟。创业是给敢于冒险的人做的。我也一直很敬佩那些公司最后没做成的创始人，因为一家公司为什么成功、另一家为什么失败，未必有很多清晰的理由；执行本身就有很大的随机性。每天都会遇到事情特别不顺的低谷期，融资时被拒绝很多，这种感受会被放大。 **Carina Hong：** 第一轮融资时，我的做法确实有变化：我意识到自己没必要在这一座山上拼到死——这件事不是我唯一想要的结果。我退一步看，市场上还有很多很好的风投机构。想通之后，压力小了很多，人也更放松、更自在；而且我觉得，这也传递出一种信号：公司很有价值。这种信心是由内而来的。所以这是一点。相反，绝望对融资过程没什么帮助。 **Ravi Belani：** 好，我想转到 AI。这个行业变化速度快得惊人，是我这辈子见过最快的行业。我想知道，在变化这么快的行业里，你怎么规划该聚焦什么？ **Carina Hong：** 这是个很好的问题。AI 变化太快了，所以设定目标时，不能只设一个下季度要实现的雄心勃勃的目标，而要设定未来一年的目标。否则就会落后于趋势，因为前沿进展更新得非常快。我记得三月时，我们还在问：能不能形式化“素数间有界间隔”这个结果？这是个很漂亮的结果，它说的是…… ## [16:19] 设定远期目标，保持全栈与灵活 · YouTube **Carina Hong：** ……有无穷多对素数，它们之间的差不会超过某个有限值，而这个有限值一直在被压低。要是降到 2，就证明了孪生素数猜想，那就恭喜了。2013 年，张益唐第一次证明这个差值有一个有限上界，当时是 7000 万。2014 年的纪录到了 246，后来一位数学家又把它推进到 240。那是很近的事，我们甚至和她经历了一场时间紧迫的竞赛。可是当我们想把 2014 年这个 246 的结果形式化时，公司里大多数人都认为做不到：工作量实在太大，他们不想定下这个目标。我们只能说，最终总得做点什么、真正留下些成果。我从中得到的一个重要启发是，目标要定得有野心。后来大家已经觉得，形式化素数间有界间隔是理所当然能做到的事。 **Carina Hong：** 第二点听起来有些矛盾：你既要什么都想自己做，又要能放手采用别人的东西。我们采取全栈路线：自己收集和管理大型数据集，不依赖数据供应商；自己制定数据策略；有模型训练团队，负责密集的中训练和后训练；我们自己构建 harness、运行基础设施和版本控制。几乎整个技术栈都不外包，唯一没做的是预训练。这就是我们全栈野心的规模。 **Carina Hong：** 但这样做的好处是，我们也得准备好接受现实：技术栈有些环节会被别人超过，所以需要时用别人的方案也没关系。你得广泛撒网。今天你可能不在前沿，但九个月后也许就能赶上。像 Harvey 这样的公司也在讲，他们先把收入做到相当规模，再开始训练前沿模型。所以这不是短跑，而是马拉松。 **Carina Hong：** 我特别关注那些不能随着技术进步及时调整的公司。举例来说，有个新模型发布时，我们第一天就试了它的分类模型；当天晚上，数据仓库里的许多分类任务已经在用它了。我们很愿意试用别人的东西，不会因为觉得自己也能做同样的东西就产生防备心——当然我说的不是刚才那个具体例子，而是我们在其他情形里也见过这种心态。 **Ravi Belani：** 所以你们愿意押很多注，也接受其中一些判断可能错了；但你们同时押了足够多的方向，因此相信自己仍然会有价值、仍然不可或缺？ **Carina Hong：** 对，而且也要聚焦。有些东西是我们的重点，比如数据。我们认为，自我改进能力来自合成生成数据。因此这类东西我们会牢牢掌握在自己手里。 **Ravi Belani：** 你觉得 AI 公司要保持竞争力，必须拥有专有数据吗？ **Carina Hong：** 我觉得是。数据和基准测试大概就是模型的定义。 **Ravi Belani：** 数据和基准测试。那你觉得现在大多数人搭建的 AI 技术栈方向都错了吗？ **Carina Hong：** 这个问题我们刚才也提到了。过去的模式是硬编码一个 harness，再调用一堆专用模型。 **Carina Hong：** 我们认为，至少现在看到的新模式，是一个尽可能精简的 harness，加上通过智能体强化学习训练出来的协调模型。 **Carina Hong：** 它可以递归地调用自己，也可以调用其他硬编码工具；这些工具甚至可能更像…… ## [20:20] 新型 AI 实验室的管理与人才 · YouTube **Carina Hong：** ……这样的工具更像是智能体。所以我们看到的方向正在变化，很多人还在为旧技术栈建设基础设施；我们觉得自己最好始终领先两步。即使能力层面落后了，你仍然有机会在基础设施层面参与竞争；但如果没领先两三步，就会陷入一种僵尸状态。 **Ravi Belani：** 你们现在站在很高的位置。我想让大家感受一下这种稀有公司群体的状态：你们融了很多钱，正在快速成长，目标也很高。你们是所谓的“新实验室”（new lab）？ **Carina Hong：** 我想 DDA 有一份列出 50 家公司的“新实验室”名单，我们确实在其中。 **Ravi Belani：** 对这类公司来说，你们要面对哪些其他初创公司可能没有的问题？比如快速扩张、增加团队成员时，跟一般初创公司有什么不同？ **Carina Hong：** 作为 CEO，很多时候不可避免地要做人员管理。对新实验室尤其如此，因为人才密度决定了企业是什么样子。如果人才模式不成立，我觉得就会进入危险区：那时你可能就不再是新实验室，而得开始拼收入了。我的日常工作有很大一部分，是理清技术管理。这和创业初期相比已经变了。 **Ravi Belani：** 我想确保大家真正理解这一点：你 24 岁，在斯坦福读书，却已经留住并吸引了世界一流的人才；别人可能花几代人的时间才培养出这样的团队。能不能讲讲你最早请来的 CTO 的背景，以及你如何吸引这么出色的人才加入？有什么诀窍吗？ **Carina Hong：** Shubho 曾在 Facebook AI Research 工作，是那里的 IC 总监。他是个有远见的人，我特别喜欢听他谈任何事情。当时 Facebook 的情况也有些动荡，时机上确实有点机缘巧合。要让每个人融入我们在 Axiom 建起来的团队，有时我得先弄清楚他们受什么驱动。理想情况下，驱动力就是我们正在解决的技术问题。Shubho 曾研究 AI 生成单元测试的评估，他相信规模化、无限数据和大规模训练。他还是 2014 年 DeepSpeech 和 DeepVoice 论文的作者之一，所以理念很契合，这为团队打下了很好的基础。 **Carina Hong：** 当然，初创公司的常态就是起起落落，压力大的时候尤其如此。我们会主动沟通，而且尽量坦诚。谈到留住人才，这是我学到的一点。说实话，作为创始人最难的是，有些日子你会觉得一切都在往下掉。你想照顾好自己，也要顾着团队，确保大家都还好。学会共情、在两者间找到平衡，这并不是我在学术训练中重点学到的东西。过去总是追求更高、更快、更强——怎么让分数再提高一点，像奥林匹克竞赛一样；不一定教你如何和人真心交流。但这对创业很重要。 **Carina Hong：** 这是新实验室面临的独特挑战之一。另一方面，新实验室不只是要做人员管理，还得做技术管理；各种优先事项可能相互冲突，而且情况一直在变化…… ## [24:22] 目标、风险与团队沟通 · YouTube **Carina Hong：** ……你可以有雄心勃勃的目标，但不能因此忽略风险。事实证明，负责定远大目标的人，和最擅长发现执行风险的人，几乎从来不是同一类人。如果按这两种角色来划分，基本是互不重叠的。当然，公司里定目标的人技术都很扎实，但这往往是附带的；专门标出风险的人，注意力则都放在“这可能行不通”上。 **Carina Hong：** 他们听起来像唱反调，但实际上不是，只是在提醒你必须听到的真实问题。有时我会想，我可以让他把话说得客气点；但他说得对。所以，关键是平衡真正的技术优先级，决定该多做还是少做，有时候少即是多。前面我讲了全栈方案，但聚焦也很重要。比如做分类或有限单群分类时，我们就只专注这件事，让所有人都朝同一个方向努力。 **Ravi Belani：** 在管理团队或吸引人才方面，有没有什么反直觉但你很看重的诀窍或做法？我听一些投资你的风投说，你有吸引顶尖人才的超能力。你刚才说的当然都是其中的一部分，但有没有什么具体方法值得未来的创始人学习？ **Carina Hong：** 我觉得有三件特别重要的事，是我以前没意识到的。每条建议背后都有很多天的煎熬和反复思考，我才把它们提炼出来。第一，从自己开始，再影响别人。当我状态不好、觉得精疲力尽时，团队也会感受到那种能量，大家都会很难受。所以有时要休息，让自己的状态平静、沉着。我以前总盯着解决这个问题、那个问题，或者某个人的问题，却没意识到，很多影响最大的时刻，来自调整自己的状态，以及脑子里突然想通、变清晰。 **Carina Hong：** 第二，我以前很不擅长描述感受。创业之前，我当然也有情绪，只是不说出来。 **Carina Hong：** 现在我更会给感受命名，也会留意别人的感受。要走过很长的自我探索过程，我才学会把情绪说出来，因为人很容易筑起一道墙，总是只用理性思考。我说这是个重要诀窍，是因为如果你不谈感受，感谢之情就不会像我希望的那样经常表达出来。我也不擅长让别人放松，因为我不会说出感受。 **Ravi Belani：** 能举个例子，让大家真正理解这个经验吗？ **Carina Hong：** 我对团队每位成员都心怀感激。 **Ravi Belani：** 好。 **Carina Hong：** 但我不是每天都说出来。有些重要时刻大家会埋头苦干，比如有限单群分类结果发布前一晚，整个办公室都在忙，至少有一半人通宵工作。 **Carina Hong：** 有意思的是，我们内部的基础设施和工具非常好，所以所有事情跑得很快。后来我们意识到，到了发布的时候，理想情况下应该让外部的人能够独立验证我们的成果，对吧？但他们的基础设施…… ## [28:22] 表达感谢、适应团队差异与数学训练 · YouTube **Carina Hong：** ……外部验证的选择并不理想。到了最后关头，比如晚上八点、早上七点就要发布时，我们还在通知大家：运行和交叉核验这个证明可能要花很久，甚至可能会失败，让人以为它是错的。正因为这个问题，大家才通宵工作。我后来意识到，我表达感谢的方式是给大家买一大船寿司，而不是直接说出来。有时候我就是说不出口，真的挺难的。 **Ravi Belani：** 你的“爱的语言”不是说出来，而是替别人做事。 **Carina Hong：** 没错。 **Ravi Belani：** 但假设你不在团队身边，只能通过 Slack 交流，那就更要让每个人觉得自己被看见了、你记得他们。我后来才学到这一点，因为日常压力会不断累积紧张感。 **Carina Hong：** 第三件事也挺有意思：我后来才学会，人和人有时就是很不一样。我起初做事很专注于单一目标，所以也希望大家都盯住一件事。但有些人像章鱼一样，同时把触手伸向八件事，反而状态最好。我真的学会了让这种做法发生，也看到了它的好处。现在我们的模式更像自下而上、又带点“仁慈的独裁”；以前公司规模变大时，我更强调自上而下和指挥链。 **Ravi Belani：** 很好。为了让大家有个概念，你们今年年初、一月份有多少员工？ **Carina Hong：** 不到 15 人。 **Ravi Belani：** 到现在十月份有多少人？ **Carina Hong：** 大概 80 人。 **Ravi Belani：** 从 15 人涨到 80 人，不到一年就增长四倍多，差不多五倍。很好。接下来我会问 ETL 的招牌问题，再开放给学生提问。大家可以先想想要问什么。Carina，先问个问题——在此之前我想知道，你学数学的经历有没有什么帮助你成为创业者？ **Carina Hong：** 什么都帮到了，真的。 **Ravi Belani：** 说说看吧，我觉得大家可能会惊讶，数学竟然和创业有关。 **Carina Hong：** 这是我在法学院学到的。我很喜欢自己在法学院读的那一年。 **Ravi Belani：** 你不是不喜欢法学院吗？ **Carina Hong：** 我喜欢，非常喜欢第一年。在数学里做证明，会训练第一性原理思维，也会训练一种非常具体的能力：高度分析。于是任何事情都会变成一道待解的题。我没法过分强调这一点在日常工作中有多重要，尤其是风险很高、压力很大的时候。我在高压的数学竞赛里仍能解题，这种能力留了下来，是非常关键的训练。 **Carina Hong：** 数学带给我的另一项帮助，是深入钻研、对一个问题着迷的能力。我把它叫作“心理韧性”。它不是说能扛过什么苦难，而是：我想不出来，就继续想、继续想、继续想。休息一下，到了第二天还是放不下。我觉得这对建立公司非常重要；没有这种韧性，你就会躲开最关键的问题。 **Ravi Belani：** 说得很好，谢谢你分享。这些是课程的招牌问题，我们会挑几个来聊，但也想留时间让学生提问…… ## [32:22] 如果重来会研究什么，以及失败的教训 · YouTube **Ravi Belani：** 我们可能稍后会发个投票。问题会穿插着问。Carina，如果你今天 20 岁、重新开始，你会把接下来五年用来学习或打造什么？ **Carina Hong：** 脑机接口。 **Ravi Belani：** 脑机接口。 **Carina Hong：** 对。我是个大书呆子，当年就是出于这种 nerdy 的兴趣读了神经科学硕士。我想选它，首先因为它还很早期，没人真正知道应该怎么做。大家还在争论该不该采用侵入式方案，技术问题也很多；我们连神经科学都还没真正弄明白，又怎么理解脑机接口？ **Carina Hong：** 但我也不想选一个只是特别难、完全不知道怎么解决的问题。我希望它关系到每个人：人人都需要沟通，而沟通的延迟实在太高。我第一次用 WhisperFlow 时特别受启发，它让我打字快了很多；打字是我沟通的一种方式，而沟通在我的生活里占了很大的时间成本。 **Carina Hong：** 第三，它连接了过去、现在和未来。过去是 AI。（Ravi：对。）现在，我觉得脑机接口正处在一个足够早期的阶段。未来则是：如果人类之间的沟通问题解决不了，那么在 AI 时代，我们可能会遇到被彻底排除在外的风险。这就是我会选择它的原因。 **Ravi Belani：** 太棒了，谢谢。关于今天创业，你有什么认识，是希望自己还坐在这些学生的位置时就已经懂得的？ **Carina Hong：** 创业真的很难。我觉得有一点值得说：困难并不能提前给你多少提示，它会在你最没想到的时候出现。如果你是个喜欢把事情安排好、连旅行都要计划好的人，有时候很难跨过那道心理关。它会挑最奇怪的日子袭来。很多最艰难的时刻，反而会出现在取得很好的成绩、拼搏告一段落之后。我没想到不确定的痛苦和煎熬会是这样。我原以为事情可能会很难，或者会很突然，却没想到两者会同时发生。 **Ravi Belani：** 又突然、又困难，而且还很煎熬。 **Carina Hong：** 对。你如果是个计划型的人，这就更糟了。 **Ravi Belani：** 是啊，因为它会突然冒出来，你只能把韧性再练强一点。好。能问问你职业生涯里最大的失败是什么，以及从中学到了什么吗？ **Carina Hong：** 有一次高中数学竞赛，我记得自己特别受打击，因为离想达到的名次就差一点。后来我回头想了想原因，也意识到那正是我最大的优势造成的——至少在那个情境里，它成了我的弱点。 **Ravi Belani：** 嗯。 **Carina Hong：** 那场中文数学竞赛有四道题。我一头扎进最后一题——数论，通常是最难、也是我最喜欢的题。我差点没能从那题里抽身。我很执着，这就是我说的那种心理韧性，结果整场比赛时间都花在那一道题上了。我从中学到，很多特质要看情境，有时是优点，有时是缺点。我不觉得没有这种特质就会成为今天的我，但在当时那个具体的场景里，它让我…… ## [36:23] 数学推理如何通向 AI 与创业建议 · YouTube **Carina Hong：** ……当时真的让我很受打击。我想，其中一个教训是，事情可能没有那么多绝对的对错。当然，时间管理是好事，缺乏优先级也确实不好，但很多时候要看具体情境。 **Ravi Belani：** 就像古希腊英雄的故事：你的长处也可能变成悲剧性的弱点。谢谢。接下来我们听学生提问。请靠近麦克风一点，让后排也能听见。 **现场提问：** 这样可以吗？ **Ravi Belani：** 很好。 **现场提问：** 如果我理解得没错，Axiom Math 正在打造 AI 数学家，最终愿景是构建能够递归改进的 AI 系统。你为什么认为数学推理特别适合用来实现递归自我改进的 AI 系统？ **Carina Hong：** 我可能会特别强调形式化数学，也就是把数学转成机器可检查的代码。转成代码之后，就能解更多数学问题：既有“用代码做数学”，也有“用数学处理代码”。所以更准确地说，我们是一家和编程关系很紧密的公司。我们会用同一套形式化数学推理引擎和技术栈来证明软件，也证明硬件。起初我有个想法：解好数学，就能解决一切。但很多关键点都藏在细节里。更准确的说法是，你搭建的技术栈中每个部分，如今都能复用来做编程，而我觉得这会改变世界。 **现场提问：** 谢谢回答。有人说，创业之前最好先去大型实验室或大公司工作，积累训练和经验。你觉得这仍然重要吗？还是建议直接跳进深水区、放手去做？ **Carina Hong：** 去大型实验室工作很有价值，前提是你觉得那里能让你学习、看到前沿。我有点特殊：在形式化数学 AI 这个新领域里，学术界当时其实处在前沿。我读的都是学术论文，因为大实验室那时兴趣不大。这个方向在大实验室里大概短暂出现过一阵，也就几个季度，然后就被放下了。 **Carina Hong：** 所以如果你所在的是一个成熟领域，前沿实验室大概就掌握着前沿，先去那里工作会是不错的选择。这是我的建议。 **现场提问：** 可是现在 AI 发展这么快，还有时间先去前沿实验室学习，再创业吗？还是应该趁现在就开始？ **Carina Hong：** 我觉得有一点是，你能在很短时间里学到很多东西。这可能出乎意料：一切都在加速，学习过程也被压缩了，学习本身还会进一步提速。我觉得这样挺好。另一点是，选择一个足够难的问题；问题足够难，就能给自己留出更多缓冲时间，让自己经历完整的学习过程——从“前严格”到严格，再到“后严格”。 **现场提问：** 谢谢你今天来。我叫 Will，是数学专业的学生。我想知道你觉得未来数学家的工作会是什么样子？我现在学的技能以后还能用得上吗？ **Carina Hong：** 你现在学的技能将来肯定用得上。关于数学以及人类数学家未来会走向哪里，我想了很多，也和许多处于不同观点光谱上的数学家谈过。…… ## [40:24] 数学的工作的价值，以及物理学的可能性 · YouTube **Carina Hong：** ……数学到底更像癌症生物学，还是更像下棋？每个人都得有自己的世界观，再据此做判断。如果你觉得它更像癌症生物学，那么数学就有内在价值：解决一个问题、做出一项发现、提出一个猜想，本身就有价值。AI 会缩短这些发现走向实际应用的时间，数学就会对科学、应用科学、技术和工程领域特别有用。这是我的看法：数学更像癌症生物学，而不是下棋。 **Carina Hong：** 当然，也有人做数学纯粹是为了乐趣。对他们来说，数学就是下棋，我后面这些论证就不适用。如果你认同数学更接近癌症生物学，也认同 AI 能缩短它走向应用的时间，那么即便数学现在已经很有用，未来也会显得更有用。就像哈代在《一个数学家的辩白》（A Mathematician’s Apology）里谈到的那样，还存在一个问题：如果事情能办成，为什么还需要人的理解？ **Carina Hong：** 我目前听到的最有说服力的理由是：人类的理解能带来 AI 目前想不出的范式转变。人类天才可能会发现一些方法，比如用 Maynard 筛法证明素数间隔有界，从而推动整个领域前进。但这个观点最有力的反驳是：如果 AI 持续进步——我觉得这更多是资本市场的问题，而不是技术问题——它也能提出猜想、建立数学理论，甚至想出分布外的范式转变。 **Carina Hong：** 接下来反过来问：人类数学家会在哪里？如果你认为数学有内在价值，那数学家会有更多类似开发者的工作流，因为编程就是一个有内在市场价值的例子。如果你不这么认为，那数学就会走下棋那条路，我觉得前面这些论点就不适用了。 **Ravi Belani：** 但如果资本市场满足需求，而且 AI 继续进步呢？ **Carina Hong：** 最坏的情况其实是…… **Ravi Belani：** 至少数学专业的学生还是会有用的。 **Carina Hong：** 我觉得最坏情况是资本市场崩盘，AI 进展受阻。到时没多少人投入时间去理解数学，范式转变的想法也会变少，然后我们就会陷入停滞。这会是最坏的情况。 **Ravi Belani：** 那最好的情况是市场继续发展…… **Carina Hong：** 最好的情况是市场继续发展，更多人成为数学家——这里的数学家，是指在工作流程中把数学作为重要部分、甚至主要部分的人。他们的需求不会被 AI 机器取代。假如 AI 真的持续进步，反而会需要更多数学理论来解释收集到的数据，也需要从数据中推导出该证明什么的规格说明，同时代码库也会不断发展。当然，时间上可能有个衔接期：一开始也许很好，之后市场又可能崩盘，这可能会是个问题。 **现场提问：** 谢谢。 **Ravi Belani：** 好，谢谢。下一位……嗨。请再靠近一点。 **现场提问：** 好。先介绍一下背景：我和一个叫 Assumptions of Physics 的团体合作，他们召集世界各地的研究者，试图找出能够导出物理学的最小物理假设集合。这也意味着，要让物理学在数学上保持一致。既然 Axiom 关注数学，你们会不会也考虑物理学？物理学的解释很重要，还需要用预测来支持这些解释。Axiom 会往这个方向做吗？ **Carina Hong：** 这很有意思。我们和几个应用领域的团队有合作项目…… ## [44:24] 数学以外的合作与智能体新范式 · YouTube **Carina Hong：** ……我们和几个应用领域的团队有合作项目。我们实际上维护一个叫 Math Econ Lib 的计量经济学库，是我们发起并维护的。我相信我们还和一个量子计算学术团队有合作。我觉得也有深度学习理论、物理学方面的合作。物理学似乎有一个由开源社区维护的库。我们还没有专门深入探索物理学领域，但我很感兴趣的是，你刚才用一阶逻辑的方式来描述如何寻找最小假设集，以及如何像依赖树一样在其上构建理论。我们之后一定要聊聊。 **现场提问：** 太好了，谢谢。 **Ravi Belani：** 最后一个问题。 **现场提问：** 你好，很高兴认识你。我有个比较细节的问题：你提到智能体的未来会不同于我们现在看到的硬编码 harness。能不能再具体讲讲？你说我们需要可训练的 harness，对吗？ **Carina Hong：** 现在我觉得已经有几家实验室能对模型做智能体强化学习。这样模型就能使用所有工具和技能，甚至调用自身或自身较小的检查点。我觉得这会成为 2026 年的新词，2027 年也许又会有一个新词，我还不知道会是什么。我觉得“群体”（swarm）已经很接近了。没有 swarm，我们就做不到现在这些事。接下来一个前沿问题是优化 swarm 的成本；要做到这一点，需要非常好的小模型。因此，小实验室训练智能体强化学习模型的故事不会结束，因为你可能既需要更大的模型，也需要更小的模型。 **现场提问：** 训练起来应该更容易——希望更容易。谢谢。 **Ravi Belani：** 好，请大家一起感谢 Carina 分享了这么多内容，甚至…… **Carina Hong：** 抱歉。 **Ravi Belani：** 尤其感谢你今天坚持来参加，经历了这么多意外的考验，展现出韧性。谢谢你，Carina。也谢谢大家。下周我们再见，到时嘉宾是 Loyal 的 Selene。