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 兩段。