Carina Hong 访谈：AI 在数学与 Axiom 中的应用

时长: 263 分钟 · ▶ 观看视频

嘉宾: Carina Hong 洪乐潼 · Axiom 创始人兼 CEO

Switch → English

章节 (41)

  • 00:00 · 简介
    • 介绍 Carina Hong 及其背景和她的初创公司 Axiom。
  • 02:16 · 数学之美与定义
    • Carina 探讨了数学中“被闪电击中”的顿悟时刻，并将数学定义为一种结构化语言。
  • 06:01 · 数学是被发现的还是被发明的？
    • 以 Ramanujan 和 Hardy 为例，探讨数学究竟是被发现的还是被发明的。
  • 08:28 · 数学中的直觉与暴力破解
    • Carina 解释了她在数学竞赛中的“暴力破解”方法，并讨论了 DeepMind 的 AlphaGeometry。
  • 11:01 · AI 在数学中的角色
    • 探讨 AI 如何作为暴力破解的协作者，以及自动定理证明与交互式定理证明之间的区别。
  • 14:41 · 在广州的成长经历与注意力管理
    • Carina 分享了她在广州的童年经历，并介绍了受限注意力与自由注意力的概念。
  • 18:13 · 创始人原型
    • 将创始人分为远见者、执行者和销售员，并以 Mark Zuckerberg 和 Elon Musk 为例。
  • 23:33 · 在 MIT 的求学经历与应对失败
    • Carina 回顾了她在 MIT 的时光，意识到自己并非“天才”，并学会了如何有所取舍。
  • 40:01 · 创始人的痛苦成瘾
    • 探讨创始人为何能忍受创业的痛苦，以及成功所需的心理特质。
  • 50:00 · 领导力与数学竞赛
    • 嘉宾探讨了她对服务型领导力的看法，以及早年在数学竞赛中构建“乐高宇宙”的经历。
  • 51:37 · 选择 MIT 与本科学习
    • 她解释了自己对进入 MIT 的强烈渴望（甚至把它写在草稿纸上），以及决定学习数学和物理的过程。
  • 54:09 · 学术荣誉与研究
    • 嘉宾谈到了获得摩根奖（Morgan Prize）的经历，以及在本科期间与 Ono 教授一起进行的数论研究。
  • 57:45 · 在 Oxford 攻读硕士与转向 AI
    • 她描述了在 Oxford 攻读硕士期间，从湿实验室神经科学（果蝇实验）向计算神经科学和 AI 的转变。
  • 01:01:05 · 对法学院的兴趣与跨学科思维
    • 嘉宾讨论了她对法律的兴趣、在 Oxford Union 的辩论经历，以及法律文本主义如何与她的技术背景产生交集。
  • 01:06:30 · 创立 Axiom 与结识联合创始人
    • 她讲述了在 Verve Coffee 结识联合创始人 Shubho 的经历，以及决定从 Stanford 博士退学以创立一家数学 AI 公司的过程。
  • 01:15:00 · 数学 AI 的发展格局
    • 嘉宾分析了 AI 应用于形式化数学的历史和现状，并提到了关键人物和里程碑事件。
  • 1:40:00 · 艰难的融资过程
    • 创始人描述了早期融资重复且令人筋疲力尽的过程，以及最初面临的拒绝。
  • 1:45:00 · 获得首批投资意向书
    • 融资的转折点出现在 Howard Morgan 等知名投资者表现出兴趣时，这带来了多份投资意向。
  • 1:50:00 · 高风险决策的压力
    • 讨论年轻创始人面临的巨大压力，并提及 Peter Thiel 与 Mark Zuckerberg 的强势谈判。
  • 1:55:00 · 种子轮融资与团队执行力
    • 以 $300 million 估值完成 $64 million 种子轮融资的细节，以及团队在构建基础设施方面的快速执行力。
  • 2:00:00 · Axiom 与 DeepSeek 及 OpenAI 的对比
    • 解释为什么 Axiom 是一家类似于 SpaceX 的硬科技公司，而不仅仅是另一家像 DeepSeek 那样的模型公司。
  • 2:05:00 · 解决 IMO 难题与数学俱乐部
    • 公司在解决复杂数学问题上的成功，以及吸引顶尖数学家加入其“数学俱乐部”的经历。
  • 2:10:00 · 拒绝 OpenAI 的收购尝试
    • 创始人讲述了 OpenAI 如何试图通过人才收购（acqui-hire）买下她的团队，以及她为什么选择保持独立。
  • 2:15:00 · 人类数学家的未来
    • 预测 AI 将负责计算，而人类数学家将专注于提供直觉和方向。
  • 2:20:00 · 攻克 Putnam 竞赛
    • 团队在“战时”状态下为解决 Putnam 竞赛付出的巨大努力，并取得了近乎完美的成绩。
  • 2:25:00 · 将数学扩展到其他领域
    • 讨论如何将数学形式化应用于法律和经济学等领域。
  • 2:30:00 · 数学与代码如同双生子
    • 探讨Curry-Howard同构，以及数学与代码之间根本的联系。
  • 2:31:33 · AI数学领域的ChatGPT时刻
    • 预测AI在数学领域将迎来类似ChatGPT或AlphaGo的突破性时刻。
  • 2:33:39 · AI数学领域的技术范式
    • 探索“Draft, Sketch, and Prove”范式以及Lean等形式化语言的使用。
  • 2:42:29 · 泛化：证明、猜想与形式化
    • 将AI数学领域的版图拆解为定理证明、提出猜想与自动形式化。
  • 2:52:21 · 编程与数学及软件验证的对比
    • 对比AI在编程与数学方面的能力，并强调软件验证是一项关键应用。
  • 3:02:58 · 商业化与市场潜力
    • 探讨形式化验证在软件和硬件领域的商业可行性。
  • 3:11:50 · AGI与ASI的对比
    • 探讨通往通用人工智能（AGI）与超级人工智能（ASI）的路径。
  • 200:00 · Lean 数据短缺与合成数据
    • 嘉宾讨论了用于形式化验证的 Lean 数据稀缺问题，以及如何利用 AI 生成合成数据。
  • 204:00 · AI for Science 与 AI for Math 的对比
    • 对比了 AI for Science（湿实验室）缓慢的迭代周期与 AI for Math 纯数字化、快节奏的特性。
  • 208:00 · Ramanujan 与数学直觉
    • 嘉宾分享了关于 Ramanujan 的故事，以说明直觉性数学发现与形式化证明之间的区别。
  • 211:00 · AI 中的预训练与后训练
    • 讨论了数学直觉是否是预训练的产物，以及当前 AI 模型为何严重依赖后训练。
  • 215:00 · 与科技巨头竞争
    • 嘉宾解释了涉及 OpenAI、DeepMind 和 Anthropic 的竞争格局，以及初创公司如何加快发展速度。
  • 220:00 · 创业哲学与二元结果
    • 反思了 Peter Thiel 对垄断的看法、Elon Musk 的 SpaceX，以及雄心勃勃的初创公司成功或失败的二元性质。
  • 230:00 · 渴望成为学徒
    • 嘉宾分享了她的个人目标，即希望成为一名“实习生”，以便在数学、物理和法律等各个领域不断学习。
  • 235:00 · 公司文化与数学英雄
    • 探讨了公司文化，包括以 Gauss、Turing 和 Lovelace 等数学家的名字命名会议室。

数据 (26)

时间 事实 数值 背景
00:38 Axiom 在 A 轮融资后的估值 $160 million 在介绍 Carina Hong 的初创公司时提及。
00:46 员工与创始人之间的年龄差距 57 岁的教授为 24 岁的创始人工作 强调 Axiom 独特的团队动态。
08:10 James Maynard 荣获菲尔兹奖 2022 在讨论数学中不同的证明技巧时提及。
10:05 AlphaGeometry 的成功率 81% DeepMind 的 AlphaGeometry 解决的历史 IMO 几何题的百分比。
12:23 首届普特南数学竞赛 1927 提及普特南竞赛的历史。
12:18 普特南历史上的满分 人类获得过 5 次满分，AI 获得了第 6 次 讨论 AI 在解决复杂数学竞赛中的突破。
01:05:06 Kenny Luo 开始研究 Lean 2020 提到她的朋友何时开始进行形式化验证研究。
01:06:24 在 Verve Coffee 会面 1000 cups 开玩笑说在与联合创始人讨论创业想法时买的咖啡数量。
01:14:50 阅读小组持续时间 1.5 years 在正式创立公司之前讨论想法所花费的时间。
01:26:50 HOList 项目启动 2016 Christian Szegedy 和 Yuhuai Wu 在 Google 早期进行的数学 AI 尝试。
01:27:15 GPT-f 项目 2019-2020 OpenAI 早期在 Ilya Sutskever 支持下进行的形式化数学研究。
01:27:44 AlphaGeometry 取得成功 2024 DeepMind 的系统解决了 IMO 几何问题。
1:40:05 估值增长 3x 从最初的报价到最终的报价，公司的估值增长了三倍。
1:48:30 种子轮估值 $300 million 种子轮融资以 $300 million 的估值完成。
1:49:08 种子轮融资金额 $64 million 公司在种子轮中筹集了 $64 million，超过了 $50 million 的目标。
1:59:57 DeepSeek Prover 表现 11% DeepSeek Prover 在特定基准测试中取得了 11% 的成绩。
2:00:00 Axiom 在基准测试中的表现 98.93% Axiom 的系统在同一基准测试中取得了 98.93% 的成绩。
2:00:31 A 轮估值 $1.6 billion 公司在 A 轮融资中达到了 $1.6 billion 的估值。
2:00:36 A 轮融资金额 $200 million+ 公司在 A 轮融资中至少筹集了 $200 million+。
2:21:12 Putnam 竞赛得分 80/120 AI 在 Putnam 竞赛中获得了 80/120 的分数，排名前 5。
2:32:32 DeepMind AlphaGeometry得分 28 points 于2024年取得，标志着AI在数学领域迎来了类似AlphaGo的时刻。
2:41:15 Draft, Sketch and Prove论文发表 2022 为AI定理证明引入的一个关键范式。
2:58:06 Donald Knuth的愿景 1980s Donald Knuth提出文学编程与代码形式化的时代。
3:01:30 Amazon自动推理代码 260,000 lines 在3到5年间为验证hypervisor组件而编写的证明代码量。
202:28 公司员工人数增长 15 to 30 公司从 12 月的 15 名员工增长到目前的 30 名员工。
202:37 竞争对手员工人数 50 to 75 嘉宾估计他们的主要竞争对手有 50 到 75 名员工。

研究观点 & 预测 (13)

  • [11:01] 数学领域的 AI 可以分为直觉型/智能型 AI 和暴力破解型 AI。
    • 证据: 基于当前 AI 模型的发展，这些模型要么模仿人类直觉，要么依赖海量计算能力。
  • [13:31] 交互式定理证明 (ITP) 是未来数学领域人机协作的方向。
    • 证据: AI 正在从单纯的自动解题 (ATP) 向与人类并肩进行交互式定理证明转变。
  • [01:04:30] AI 可用于解释法律文本和宪法。
    • 证据: 将 LLM 应用于历史文献以理解最初的公众含义，将其视为一个结构化数据问题。
  • [01:06:00] 形式化验证（Lean）可以将数学转化为代码。
    • 证据: 将数学问题视为编程问题，使 AI 能够更有效地解决它们，实现从自然语言到形式逻辑的转变。
  • [01:20:00] 仅仅扩大规模可能不足以解决数学领域的 AI 问题。
    • 证据: 与语音或视觉领域不同，数学可能需要新的架构或数据生成策略，而不仅仅是扩大计算规模。
  • [2:24:50] AI 将使社会从“数学贫乏”向“数学丰富”转变。
    • 证据: 随着 AI 以指数级更快的速度解决复杂的数学问题，数学证明和发现的供应量将呈爆炸式增长。
  • [2:25:55] 人类数学家的角色将转向提供直觉。
    • 证据: 人类不再进行手动计算和编写证明，而是指导 AI 哪些问题是重要的，并提供高层次的直觉。
  • [2:31:33] AI数学领域将迎来ChatGPT时刻。
    • 证据: 由形式化验证与大语言模型的结合所驱动。
  • [2:46:02] 自动形式化是一个主要瓶颈。
    • 证据: 将自然语言数学转化为形式化代码（如Lean）目前比证明定理本身更难。
  • [2:52:21] 软件验证是AI数学领域的第一个主要商业市场。
    • 证据: 在实现通用数学AI之前，形式化验证代码的能力将彻底改变软件工程。
  • [3:11:50] ASI（超级人工智能）将先于AGI出现。
    • 证据: 在具备跨越所有人类任务的通用智能之前，AI将在特定领域（如数学或验证）达到超越人类的表现。
  • [201:30] AI 可以有效地为 Lean 生成合成数据。
    • 证据: 通过使用 AI 合成数据，公司可以克服人类编写的形式化证明稀缺的瓶颈。
  • [211:40] 数学直觉可能是预训练的结果。
    • 证据: 嘉宾假设 Ramanujan 的“直觉”本质上是一种高度优化的预训练状态，而当前 AI 在数学方面的努力主要集中在后训练上。

关键概念 (17)

  • [04:36] 数学作为一种结构化语言
    • 数学是一个建立在人类公认的公理之上的文明系统，并在此基础上构建了复杂的结构。
  • [14:05] 自动定理证明 (ATP)
    • 使用计算机根据预定义规则自动证明数学定理。
  • [14:08] 交互式定理证明 (ITP)
    • 人类与计算机合作证明定理的协作过程，其中 AI 充当助手。
  • [15:55] 受限注意力与自由注意力
    • 受限注意力是严格专注于所需任务（如回复电子邮件），而自由注意力则允许思维漫游并产生富有创意的战略性想法。
  • [01:02:50] Originalism / Textualism
    • 关注宪法最初公众含义或严格文本的法律哲学，她将其与结构化数据分析联系起来。
  • [01:05:08] Formal Verification (Lean)
    • 使用编程语言编写并以绝对的确定性验证数学证明，将数学转化为代码。
  • [01:06:09] Math as Code
    • 将数学形式化使其成为一个软件工程问题的理念，从而使其易于使用 AI 工具处理。
  • [2:02:12] Formalization (形式化)
    • 将数学问题和证明转化为严格的、机器可读的语言（如 Lean）的过程，以便计算机能够验证其正确性。
  • [2:03:17] Program Synthesis
    • 自动生成计算机程序以解决特定问题，Axiom 使用它来弥合自然语言数学与形式化代码之间的差距。
  • [2:23:52] Axiom (公理)
    • 数学中不证自明的真理，被选为公司名称以反映其基础性目标。
  • [2:30:30] Curry-Howard Correspondence
    • 计算机程序与数学证明之间的直接联系。
  • [2:41:15] Draft, Sketch, and Prove
    • 一种范式，即先起草非正式证明，将其形式化为草图，然后使用AI证明器进行严格证明。
  • [2:46:02] Auto-formalization
    • 将自然语言数学自动转化为如Lean等机器可验证的形式化语言的过程。
  • [2:52:21] Formal Verification
    • 根据特定的形式化规范或属性，证明或证伪系统底层预期算法正确性的行为。
  • [200:26] Lean
    • 一种形式化证明验证语言，用于在数学上证明代码或定理的正确性。
  • [201:34] 合成数据生成
    • 在人类数据稀缺时，使用 AI 模型创建人工数据（在此处为形式化数学证明）来训练其他模型。
  • [211:45] 预训练与后训练
    • 预训练是在大量原始数据上训练 AI 以建立直觉的初始阶段，而后训练则是针对形式化验证等特定任务对其进行微调。

提及人物 (35)

  • Carl Friedrich Gauss — 在谈到数学顿悟的“被闪电击中”时刻时被提及。
  • Srinivasa Ramanujan — 被用作具有无法解释的、外星人般直觉的数学家例子。
  • G. H. Hardy & J. E. Littlewood — 致力于正式证明 Ramanujan 直觉发现的数学家。
  • Yitang Zhang — 因其关于素数有界间隔的著名证明而被提及。
  • James Maynard — 因其 2022 年获得菲尔兹奖及证明技巧而被提及。
  • Henry Cohn — 给 Carina 布置球体堆积问题的 MIT 教授。
  • Evan Chen — IMO 教练，其复杂的几何图被 AI 破解。
  • Mark Zuckerberg — 被用作“执行者”型创始人的典型例子。
  • Elon Musk — 被用作“远见者”型创始人的例子。
  • Sam Altman — 被用作“销售员”型创始人的例子。
  • Mike Schroepfer (Schrep) — 被提及为 Facebook 具有远见的 CTO，与 Zuckerberg 形成互补。
  • Sheryl Sandberg — 被提及为帮助 Facebook 扩大规模的强力执行者。
  • Prof. Ono — 嘉宾本科期间的数论研究导师。
  • Kenny Luo — 一位来自 MIT 的朋友，向她介绍了 Lean 和形式化验证。
  • Shubho — 嘉宾在 Axiom 的联合创始人。
  • Tudor — 一家竞争性数学 AI 公司的 CEO。
  • Christian Szegedy — 数学 AI 领域的先驱，曾参与 HOList 项目。
  • Yuhuai (Tony) Wu — 曾在 Google 从事数学 AI 研究，后来创立了 xAI 的研究员。
  • Ilya Sutskever — 在 OpenAI 支持了早期的数学 AI 研究。
  • Howard Morgan — 早期对公司表现出信任的投资者，提升了创始人的信心。
  • Jim Simons — 传奇数学家、Renaissance Technologies 创始人，作为人脉关系被提及。
  • Peter Thiel — 以强势谈判策略闻名的投资者，在 Mark Zuckerberg 的故事中被提及。
  • Matt Murphy — Menlo Ventures 合伙人，主导了对 Axiom 的投资。
  • Ken Ribet — 著名数学教授，曾与 Axiom 团队就数学证明进行交流。
  • Francois Chollet — 加入 Axiom 团队的 AI 研究员，以其在 ARC 方面的工作而闻名。
  • David Silver — 一篇关于从经验中学习的论文的合著者。
  • Richard Sutton — 一篇关于从经验中学习的论文的合著者。
  • Terence Tao — 参与数学形式化的著名数学家。
  • Kevin Buzzard — 提倡使用Lean进行数学形式化的数学家。
  • Donald Knuth — 在1980年代构想代码形式化的计算机科学家。

公司提及 (20)

Facebook (Meta) · Axiom · Google DeepMind · MIT · Oxford University · Stanford University · Meta · Baidu · Anthropic · OpenAI · B Capital · First Round Capital · Facebook · Menlo Ventures · DeepSeek · SpaceX · DeepMind · Amazon · Cadence · Essential AI

引用 (13)

数学有点像人类决定创造一个文明系统，在这个系统内，我们建立在我们一致认为是真实的公理之上。 — Carina Hong @ 04:43

我是一个暴力破解型选手。如果你给我一道几何题，我就会直接用复数强行计算出来。 — Carina Hong @ 08:45

自由注意力是区分普通创始人与具有高度战略眼光和决断力的创始人的关键。 — Carina Hong @ 16:42

我们认为不可能的一切都是可能的。 — Axiom Founder @ 01:07:16

我认为这项技术的风险并没有我最初想象的那么高。 — Axiom Founder @ 01:14:26

我们这顿饭不吃完，你不签，我这个东西我现在撕掉。 — Peter Thiel (quoted by guest) @ 1:50:38

不要再去精确的搞这些东西了，现在是战争状态，能怎么快捷的去做就怎么快捷的去做。 — Axiom Founder @ 2:20:51

数学就是代码，代码就是数学。 — Guest @ 2:30:26

任何你能定义的东西，你都能证明。 — Guest @ 2:52:26

我不太喜欢AGI这个词。我认为我们正在构建的是ASI（超级人工智能）。 — Guest @ 3:14:15

Ramanujan 那种自然的、直觉性的状态，实际上可能是预训练的产物。 — Guest @ 211:41

垄断导致停滞，竞争导致平庸。 — Guest @ 220:05

我目前是‘Don’t Die’运动的信徒。 — Guest @ 249:48

经历 & 个人故事 (11)

  • [14:52] Carina 在广州长大，喜欢当地的美食，并在上学的路上思考数学问题。
  • [23:33] 在她的数学竞赛时期，她意识到自己并非天生的几何“天才”，因此她开发了一种使用复数来解决问题的暴力破解方法。
  • [34:00] 在 MIT，她周围都是才华横溢的同龄人，她意识到自己无法仅凭纯粹的天赋竞争，这促使她寻找自己独特的道路，并退出了那些她觉得无法胜出的课程。
  • [51:37] 她非常渴望进入 MIT，在考试时把这几个字母写在草稿纸上以激励自己。
  • [57:45] 在 Oxford 攻读硕士期间，她意识到自己更喜欢计算 AI，而不是用果蝇进行湿实验室神经科学实验。
  • [01:06:30] 在决定从 Stanford 博士退学并创立 Axiom 之前，她花了大约一年半的时间在 Verve Coffee 与未来的联合创始人讨论想法。
  • [1:40:00] 创始人分享了早期融资的艰辛经历，面临无数次拒绝，不得不在兼顾学业和考试的同时重复相同的推销。
  • [1:51:51] 她讲述了与其他女性创始人一起参加高空滑索活动的经历，在那里她必须克服恐惧并放手一搏，她将其比作在信息不完整的情况下做出高风险决策的创业之旅。
  • [2:09:14] OpenAI 主动联系希望收购她的团队。尽管对方享有盛誉，她还是拒绝了这份邀约，因为她想实现自己的愿景，并认为加入大公司会妥协她的目标。
  • [2:49:38] 嘉宾分享了一段个人轶事：在疫情期间学习代数几何时，学到了“germ”这个词（在日常英语中意为细菌，但在数学中有特定含义，即“芽”），以此说明自然语言与数学术语之间的鸿沟。
  • [230:00] 嘉宾分享说，她的终极梦想不一定是永远做 CEO，而是成为一名“实习生”或学徒。她喜欢涉足新领域（如计算神经科学、物理学或法律）并从零开始学习的想法。

工具与模型 (15)

  • AlphaGeometry: Google DeepMind 开发的一款 AI 模型，通过将复杂的 IMO 几何问题转化为符号表达式来解决它们。
  • Lean: 数学家用于交互式定理证明的一种形式化证明编程语言。
  • Lean: 一个用于将数学数字化的形式化证明验证系统和编程语言。
  • HOList: Google 开发的一个用于高阶逻辑证明机器学习的早期环境。
  • GPT-f: OpenAI 开发的一个基于生成式预训练 Transformer 的自动定理证明器。
  • AlphaGeometry: DeepMind 开发的一个能达到奥林匹克竞赛水平并解决复杂几何问题的 AI 系统。
  • Lean: 一种形式化证明验证语言，用于翻译和验证数学证明。
  • DeepSeek Prover: DeepSeek 开发的用于数学推理和证明的 AI 模型。
  • Monte Carlo Tree Search (MCTS): AI 中用于探索可能解决方案的搜索算法，被提及在他们早期的一些方法中计算成本过高。
  • Lean: 一种函数式编程语言和定理证明器，被大量用于数学形式化。
  • Isabelle: 一种较早且成熟的交互式定理证明器。
  • Coq: 另一种成熟的交互式定理证明器。
  • AlphaGeometry: DeepMind开发的一种AI系统，能够以奥林匹克竞赛水平解决复杂的几何问题。
  • Lean: 一种用于数学形式化验证的定理证明器和编程语言。
  • Transformer: 在《Attention Is All You Need》论文背景下提到的底层神经网络架构。

主题

数学 AI · 自动定理证明与交互式定理证明 · 创始人原型 · 数学竞赛与教育 · 注意力管理 · 数学 AI · 形式化验证 · 创业历程 · 跨学科研究（数学、法律、AI） · 学术生涯与创业 · 数学 AI · 初创公司融资 · 形式化验证 · 硬科技创业 · 风险投资谈判 · AI在数学中的应用 · 形式化验证 · 定理证明 · 自动形式化 · Lean编程语言 · AGI与ASI的对比 · 用于数学的 AI · 形式化验证 · 合成数据 · 创业策略 · 预训练与后训练

要点

  • 通过交互式定理证明，AI 正在将数学从纯粹的人类探索转变为人机协作的过程。
  • 创始人通常分为三类：远见者、执行者和销售员。成功的公司需要这些特质的互补组合。
  • 自由注意力对于创造性解决问题和战略领导力至关重要，它是区分伟大创始人与普通创始人的关键。
  • 并非所有成功的数学家或研究人员都纯粹依靠“天赋”；暴力计算和坚持不懈的努力也是非常有效的策略。
  • 像 Lean 这样的形式化验证语言正在弥合抽象数学与 AI 之间的差距。
  • 跨学科思维（例如将 AI 应用于法律文本主义）可以激发新颖的创业想法。
  • 数学 AI 领域发展迅速，从 2016 年的早期实验发展到了 2024 年的奥赛级系统。
  • 创立一家深科技初创公司通常需要长期的构思和建立信念，然后才能迈出这一步。
  • 为硬科技 AI 初创公司融资需要极大的韧性以及应对反复被拒的能力。
  • 拥有强大的、逆向的愿景（例如专注于形式化而不仅仅是 LLM 扩展）可以吸引顶级的投资者和人才。
  • AI 将从根本上改变数学领域，将人类的角色从计算和手动编写证明转变为提供高层次的直觉。
  • 年轻的创始人必须学会在信息不完整的情况下，快速做出高风险的决策。
  • AI与数学的交叉领域正朝着形式化验证发展，证明过程被写成代码（如Lean）并由机器进行验证。
  • 自动形式化（将人类数学转化为代码）目前是比实际定理证明更大的瓶颈。
  • “AI数学”的首个大规模商业应用很可能是在软件和硬件验证领域，以确保代码没有漏洞。
  • AI的发展很可能会在实现广泛的通用人工智能（AGI）之前，先在特定领域实现超级人工智能（ASI）。
  • AI for Math 的迭代周期比 AI for Science 快得多，因为它不依赖于物理湿实验室。
  • 形式化验证 AI 的最大瓶颈是缺乏人类编写的 Lean 数据，这使得合成数据生成变得至关重要。
  • 初创公司可以通过更快的行动速度和承担二元的高风险赌注来与科技巨头竞争。
  • 数学直觉（如 Ramanujan 的直觉）可以被认为是高度优化的预训练，而形式化证明生成则是一项后训练任务。