AI 開始「做研究」了

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