最近在追一篇 Google DeepMind 的論文，看完之後一直在想一個問題：當 AI 不再只是「輔助工具」，而是真的能自主產出新知識，整個知識生產的社會結構會怎麼變？

這篇論文描述的系統叫 AlphaProof Nexus。它讓 LLM 去生成 Lean 語言的形式化證明，再由 Lean 編譯器自動驗證每一個邏輯步驟。結果是什麼？這個 agent 自主解決了 353 個 Erdős 開放問題中的 9 個，還證明了 OEIS 資料庫中 492 個猜想裡的 44 個。更驚人的是，其中兩個問題已經懸而未決 56 年。

每個問題的成本：幾百美元。

---

知識生產的「平民化」，是禮物還是陷阱？

從社會學的角度，我習慣先問：這項技術的受益者是誰？

表面上，這個發展聽起來非常民主化。如果幾百美元就能突破一個困擾數學家幾十年的問題，似乎任何人都能參與高端研究，不再需要長達十年的博士訓練或昂貴的學術機構支持。這是知識民主化的夢想。

但我有保留。

首先，「幾百美元」對誰來說是低門檻？對 Google DeepMind 的研究員，或是有充分算力資源的人來說，當然低。但對全球大多數研究機構，尤其是南半球的大學、資源不足的學術環境，這仍然是一個不小的門檻。更關鍵的問題是：如果這套工具真的有效，誰控制它的使用權？

Lean 形式化語言的基礎設施、LLM 本身的訓練數據、AlphaProof 系統，這些全部集中在少數幾個科技巨頭手裡。知識的「生產工具」高度集中，這不是民主化，這是一種新型的知識生產壟斷。

---

形式化證明解決了幻覺問題嗎？還是只是轉移了問題？

論文特別強調，用 Lean 這類形式化語言可以解決 LLM 的「幻覺」問題，因為每一步都有編譯器驗證，不存在邏輯跳躍。這個說法技術上沒錯，但我認為它迴避了一個更根本的問題。

形式化驗證能確保「邏輯上無誤」，但它無法確保「問題問得對」。

在數學裡，這個區別可能不那麼明顯。但當這套方法論被延伸到其他領域，比如社會科學、政策分析、醫療決策，問題就大了。一個 AI 系統可以完美無瑕地回答「在這個模型假設下，解是什麼」，但如果模型本身的假設帶有偏見，或者把複雜的社會現象過度簡化，那邏輯再嚴謹也沒用。

現在 AlphaProof Nexus 已經被部署在組合數學、最佳化、圖論、代數幾何，甚至量子光學領域。未來進入社會科學或政策研究只是時間問題。到時候「形式化驗證」的光環，有沒有可能讓人忽視更根本的框架偏誤？

---

誰的問題值得被解決？

論文裡有個細節讓我很注意：他們選擇的開放問題是 Erdős 問題集和 OEIS 猜想，這些都是西方主流數學圈長期積累的問題庫。

這不是批評，而是一個觀察：AI 系統解決的問題，取決於它被訓練用什麼數據、被部署在什麼脈絡。如果知識生產的工具繼續集中在特定地理、語言、學術傳統的主導下，那 AI 加速的只是既有知識結構的再生產，而不是打破它。

更激進的問法是：非西方的數學問題、被邊緣化的知識傳統，會進入這類 AI 系統的訓練數據嗎？還是這波 AI 知識革命，本質上只是把現有的學術不平等高速複製？

---

我真正擔心的不是 AI 取代研究員，而是什麼算「研究員」這件事本身

這篇論文展示了一個 AI 系統自主工作、自主發現、自主驗證的完整循環。在這個循環裡，人類研究員的角色是什麼？

作者說，系統「正在輔助進行中的研究」。但我覺得這個描述低估了它的影響。當一個 AI 能在幾百美元內解決 56 年的懸案，人類研究員在這個過程中貢獻的是什麼？是問題的選擇？是對結果的詮釋？還是只是按下「執行」的那個動作？

這背後是一個深層的學術制度問題。學術界的訓練、評鑑、晉升，整個結構都建立在「人」花時間攻克問題這件事上。如果 AI 開始大量「解題」，博士訓練的意義是什麼？學術評鑑的指標要怎麼調整？學術成就感這個東西，還有沒有市場？

---

我沒有答案。但我覺得，現在討論這些問題，比等到這個系統真的普及了再來後悔，要重要得多。

AlphaProof Nexus 是一項令人驚嘆的技術成就。但技術成就從來不在真空中運作，它在一個有歷史、有權力結構、有不平等的世界裡落地。我們需要的不只是更好的數學工具，而是一個關於「AI 知識生產

」的認真倫理討論。