AI 用几千行 Lean 代码硬解普特南题，这不是智能的胜利
普特南竞赛 98 年只有五个满分，AI 拿到第六个，但它没走人类那张图，而是用几千行 Lean 代码枚举硬算——自动定理证明这个领域在 AI 之前就存在了。
原视频在 YouTube 上放不出来，用音频听：
核心论点 · 点时间戳可跳到原声
AI 拿满分，但没走人类那张图
Axiom 的 Action Prover 在普特南大学生数学竞赛拿了满分。这项竞赛 1927 年开始，过去 98 年人类历史上只有五个满分，这是第六个，由 AI 拿到。有意思的是解法对比：队伍里的 Evan Chen（美国 IMO 队教练）画一张图就把某道题做出来了，AI 没找到这个解法，而是用几千行 Lean 代码，靠类似枚举、分类讨论一步步硬核出来。洪乐潼由此说这是「大力出奇迹的 AI」——即使一道明显可以走创造力解法的题，机器也会用它擅长的路径给出完全不一样的解法。
— 洪乐潼自动定理证明不是 AI 的胜利
洪乐潼纠正了一个常见误解：自动定理证明（ATP）这个领域在没有深度神经网络、没有 AI 的时候就存在了，是一群计算机科学家希望用基于规则的系统帮人类解决数学问题。ITP 是交互式定理证明，过去由人类数学家和电脑系统合作完成。现在做的只是把 ITP 中的人类换成了 AI。所以这个古老学科本质上是 ATP 与 AI 的交集，不能算 AI 的胜利。
— 洪乐潼bounded attention 与 free attention 的配比
洪乐潼的导师提出一对概念：bounded attention 是被框架住的注意力，比如每天起来处理必须执行的邮件和 deadline；free attention 是自由注意力，很多成功企业家是极有纪律的执行家，日复一日复利执行。但区分一个平均创业者和有策略性决策的创业者，恰恰在自由注意力这里。她强调这不是线性的——投入自由注意力时间也可能什么都没想到，但后面被逼做任务时会有 callback，回到自由注意力给大脑打下的基础。配比因人而异，她自己也不知道。
— 洪乐潼从宪法解释跳到 AI 做数学
在法学院学宪法解释时，洪乐潼接触到 originalism、textualism、living constitutionalism 三种诠释方式，她自认是 textualist。有人建议用语言模型喂建国文献等数据去理解词义，她由此想到：如果 AI 已经能看宪法是什么意思，为什么不能拿 AI 做数学？因为数学需要的不是英语，而是更结构性的呈现，形式化语言把数学变成了代码。她最好的朋友之一 Kenny Law 从 2020 年起就在做 Lean 形式化证明，是 Mathlib 最早五到七个建设者之一，是 Kevin Buzzard 的学生。
— 洪乐潼数学家背景对 Scaling 团队可能是负分
Axiom 早期定了一条规矩：招到第 15 个人之前不招数学家，因为种子轮融资相对要做的事是 under raise，人头受限。更关键的是，一些数学家背景的同学对 Scaling 有犹豫甚至不喜欢这种哲学，觉得数学是手艺、像日本师傅捏寿司，有人接了 offer 之后又不来了，说不要做 Internet Scale Dataset。所以现在招数学家要求思想非常开放，希望他们做 adversarial 的、与系统相对抗的基准创造，去感觉系统哪里弱。Ken Ono 加入后成为基准级集结的第一号人物。
— 洪乐潼融资是群体博弈，没人愿意先拒绝
洪乐潼描述融资时投资人的真实行为：他们不直接拒绝，而是拖着你——因为怕拒绝后你以后不理他，所以等你拿到别人的 offer 再跟。她把这种机制叫 groupthink。所以创始人真正要解决的不是「说服所有人」，而是找到一个愿意先 say yes 的领投方，剩下的会 oversubscribe。她种子轮同时拿到三个领投 offer，价格从一倍涨到两倍再到三倍，一个月一个台阶。
— 洪乐潼Lean 数据太少，验证工具得自己造
Lean 是形式化语言，公开领域的 token 总量非常小，远不能和 Python 比。它同时是编程语言、编译器和 runtime，非常 finicky，object 必须符合种种限制。她还指出作弊风险：如果假设公理 n 加 n 等于 n，就能「证明」2 加 2 等于 2。社区原来用的 comparator 比她们自研的 verify proof 慢一百倍，所以她们造了十二三个辅助工具。AlphaProof 用 Monte Carlo tree search，她们觉得太贵，钱不够，只能另找办法。
— 洪乐潼把数学翻译成 Lean 比证明更难
她认为 auto formalization 被严重低估：把 arXiv 论文里成对的定理与证明转成 Lean 代码，需要先拆出 blueprint 蓝图，20 页文章可能拆成 200 到 500 页。陶哲轩、Kevin Buzzard、Alex Kontorovich 曾手工写蓝图，再分给全世界本科生每人领一小块。她指出这不是翻译——英语和法语抽象层级类似，而 Lean 更像 Python，且 AI 见过的 Lean 数据极少。反方向 auto-informalization 较易，但要用 cycle consistency 反复转回验证正确性。
— 洪乐潼原话 · 已逐字校验
2024一炮而同的这个Alpha proof 拿了28分差一分金牌的银牌 这个对我来说是一个 是IMO被解决的那一个时刻
2024 年一炮而红的 Alpha Proof 拿了 28 分，差一分金牌的银牌。这个对我来说是一个 IMO 被解决的那一个时刻。
洪乐潼1:37:43
它就是累 你是一个复读机 你一次一次的 说一样的事情 你一次一次的 接到一样的问题
它就是累。你是一个复读机，你一次一次地说一样的事情，你一次一次地接到一样的问题。
洪乐潼1:40:43
年轻做product是加分 年轻做deep tech是减分
年轻做产品是加分，年轻做 deep tech 是减分。
洪乐潼1:50:45
大家没有意识到一件事情 我们不是一个模型公司 我们是一个deep tech公司 我们是一个深科技公司 我们做的这件事情 有点像spacex
大家没有意识到一件事情：我们不是一个模型公司，我们是一个 deep tech 公司，我们做的这件事情有点像 SpaceX。
洪乐潼2:02:48
现在不是说数学纯粹之美的时刻 不要去精确的去搞这些东西 现在是战争状态
现在不是说数学纯粹之美的时刻，不要去精确地搞这些东西，现在是战争状态。
洪乐潼2:22:05
但是如果你只是把 这个人类已经就是发现了的 写好了的数学 转化为了这个形式化的 你会得到更少的赞美 但是这个科技 它其实比这个证明要更难 至少是一样的难度 我其实觉得是更难
但如果你只是把人类已经发现、写好的数学转化成形式化的，你会得到更少的赞美。而这个技术其实比证明更难，至少是一样的难度——我其实觉得是更难。
洪乐潼2:46:31
数字与实体
| 普特南数学竞赛 AI 满分 | 人类历史第 6 个满分（1927 年开赛以来共 5 个） | 12:04 |
| Alpha Geometry 解决 IMO 几何题比例 | 81% | 10:03 |
| Axiom 种子轮后团队规模 | 30 人 | 1:28:37 |
| Axiom 融资估值 | 16 亿美元 A 轮 | 0:00 |
| 种子轮估值 | 3亿美金 | 1:48:44 |
| A轮估值 | 16亿美金 | 1:59:47 |
| A轮融资额 | 至少2亿美金 | 1:59:47 |
术语
- ATP自动定理证明
- 用基于规则的系统自动证明数学定理，早于深度学习存在。
- ITP交互式定理证明
- 人类数学家与电脑系统合作完成证明，现在人类被 AI 替换。
- LeanLean
- 形式化数学语言，同时是编程语言、编译器和 runtime。
- auto formalization自动形式化
- 把自然语言数学论文转成 Lean 代码，比证明本身更难。
- groupthink群体博弈
- 投资人互相观望、不愿先拒绝，等别人先出手再跟。
收听指南
适合做 deep tech 或 AI for Science 的创业者、关注早期融资博弈的投资人，以及想了解形式化数学与 AI 结合前沿的工程师。
对法学院宪法解释和创业者分类不感兴趣的，可跳过 1:04:26 和 18:05 两段。