OpenAI 數學大爆發

官方公告翻譯 × HN 185 則討論整理

sourceopenai.com / HN

Lead: OpenAI 把大批 AI 數學成果一次丟上 GitHub，含 Lean 形式化與推理摘要，並承諾釋出模型。HN 共識是成果驚人，但驗證、開放性、算力說法三處爭議未解。

A

官方說了什麼

諮詢 IAS 的數學與 AI 獨立小組，按其公開建議發布
成果放 GitHub，附論文修訂與引用規範，研議社群託管替代方案
多數證明附 Lean 形式化，陸續補齊
公開 10 份推理摘要、Pro 用量換算算力、嘗試題數統計；平均每題約 3 小時 Pro thinking
資助工作坊與特別計畫，協助理解 AI 產出的重大結果
正努力負責任地釋出產出成果的模型

B

這次炸了哪些題

題目	份量	HN 反應
Unique Games 猜想	複雜度理論基石，牽動大量近似難度結果	事先無共識會往哪邊解，最大亮點
整數乘法 O(n (log n)^(1-κ))，κ=2^-182	打破 n log n 信仰	極小改進，疑為 galactic algorithm，實用性存疑
複數 FFT 低於 n log n	同上	意外，與乘法同源
矩陣乘法 ω ≤ 2.25、Subset Sum 0.49	演算法突破	待驗證，shock 級
Barnette 猜想、三機排程 O((L+2)^150020)、平面 5 色不可能、Navier-Stokes 強制流圖靈完備	橫跨圖論、排程、組合	排程指數被笑 crazy exponent
proofatlas top 500 宣稱解 90 題	含 Hilbert 10th over Q、Landau-Siegel、Baum-Connes	有人估 50-100 年人類進度

C

Lean：驗證器還是遮羞布

正方：無 Lean 會被十億行定理淹沒，Buzzard 之問開始有答案
反方：Lean 只保證明對，不保陳述寫對；Hales 球堆積經驗，難在 statement
賭盤：跨多領域不可能全 spot check，必有一篇出錯；出錯是否算公關 backfire 雙方僵持
寫作：UGC 論文符號混亂，模型數學強、英文闡述弱，更顯形式化必要

D

為何數學家不爽

此前Navier-Stokes 事件引用與搶發爭議，Bubeck 等人被點名
09-29AGMAI 公開信要求停用封閉模型解開放難題， proprietary 測試不背書
此次GitHub 大放送成果公開、模型說以後釋出，被酸 fuck all your demands
Tao 補刀Mastodon 發文要的是 AI 向數學家解釋結果，不是一堆 preprint

E

算力、職涯、末日

算力：3 小時 Pro thinking 被疑沒算失敗運行，單位不明，要 Blackwell GPU 小時數
方法：推理過程紀錄僅給節錄，harness 看似不強，主因是內部模型強 4 倍
博士生：被搶發自古有之，現在機率大增；建議拿 AI 成果當新起點或轉應用
末日：一方稱 RSI era 已至，AI 做演算法研究即遞迴自改；一方稱 token 化萬物皆可解；濫用與強化學習對齊失效風險並存
署名：要求掛人類審稿名；反方稱 OpenAI 在訓練你信任機器

Repo: github.com/openai/math，含 preprints、reasoning_traces、overview.pdf
鏡像: hub.valency.io/collections/openai-math
討論: news.ycombinator.com/item?id=49984923，240 points / 185 comments
提醒: 證明正確性待社群覆核，引用前先查 repo 最新修訂

---
template: sheet
title: OpenAI 數學大爆發
subtitle: 官方公告翻譯 × HN 185 則討論整理
cols: 3
source: openai.com / HN #49984923 / github.com/openai/math
---
Lead: OpenAI 把大批 AI 數學成果一次丟上 GitHub，含 Lean 形式化與推理摘要，並承諾釋出模型。HN 共識是成果驚人，但驗證、開放性、算力說法三處爭議未解。

## A 官方說了什麼
- 諮詢 IAS 的數學與 AI 獨立小組，按其公開建議發布
- 成果放 GitHub，附論文修訂與引用規範，研議社群託管替代方案
- 多數證明附 Lean 形式化，陸續補齊
- 公開 10 份推理摘要、Pro 用量換算算力、嘗試題數統計；平均每題約 3 小時 Pro thinking
- 資助工作坊與特別計畫，協助理解 AI 產出的重大結果
- 正努力負責任地釋出產出成果的模型

## B 這次炸了哪些題 {span=2}
| 題目 | 份量 | HN 反應 |
|---|---|---|
| Unique Games 猜想 | 複雜度理論基石，牽動大量近似難度結果 | 事先無共識會往哪邊解，最大亮點 |
| 整數乘法 O(n (log n)^(1-κ))，κ=2^-182 | 打破 n log n 信仰 | 極小改進，疑為 galactic algorithm，實用性存疑 |
| 複數 FFT 低於 n log n | 同上 | 意外，與乘法同源 |
| 矩陣乘法 ω ≤ 2.25、Subset Sum 0.49 | 演算法突破 | 待驗證，shock 級 |
| Barnette 猜想、三機排程 O((L+2)^150020)、平面 5 色不可能、Navier-Stokes 強制流圖靈完備 | 橫跨圖論、排程、組合 | 排程指數被笑 crazy exponent |
| proofatlas top 500 宣稱解 90 題 | 含 Hilbert 10th over Q、Landau-Siegel、Baum-Connes | 有人估 50-100 年人類進度 |

## C Lean：驗證器還是遮羞布
- 正方：無 Lean 會被十億行定理淹沒，Buzzard 之問開始有答案
- 反方：Lean 只保證明對，不保陳述寫對；Hales 球堆積經驗，難在 statement
- 賭盤：跨多領域不可能全 spot check，必有一篇出錯；出錯是否算公關 backfire 雙方僵持
- 寫作：UGC 論文符號混亂，模型數學強、英文闡述弱，更顯形式化必要

## D 為何數學家不爽
```timeline
此前 | Navier-Stokes 事件 | 引用與搶發爭議，Bubeck 等人被點名
09-29 | AGMAI 公開信 | 要求停用封閉模型解開放難題， proprietary 測試不背書
此次 | GitHub 大放送 | 成果公開、模型說以後釋出，被酸 fuck all your demands
Tao 補刀 | Mastodon 發文 | 要的是 AI 向數學家解釋結果，不是一堆 preprint
```

## E 算力、職涯、末日
- 算力：3 小時 Pro thinking 被疑沒算失敗運行，單位不明，要 Blackwell GPU 小時數
- 方法：推理過程紀錄僅給節錄，harness 看似不強，主因是內部模型強 4 倍
- 博士生：被搶發自古有之，現在機率大增；建議拿 AI 成果當新起點或轉應用
- 末日：一方稱 RSI era 已至，AI 做演算法研究即遞迴自改；一方稱 token 化萬物皆可解；濫用與強化學習對齊失效風險並存
- 署名：要求掛人類審稿名；反方稱 OpenAI 在訓練你信任機器
## F 來源 {bare}
```kv
Repo: github.com/openai/math，含 preprints、reasoning_traces、overview.pdf
鏡像: hub.valency.io/collections/openai-math
討論: news.ycombinator.com/item?id=49984923，240 points / 185 comments
提醒: 證明正確性待社群覆核，引用前先查 repo 最新修訂
```