【科技快報】《Gauss：自動形式化代理｜AI 破解困擾人類數月的數學證明》(2025)

哥德巴赫猜想（Goldbach's conjecture）是數論中存在最久的未解問題之一。這個猜想最早出現在1742年普魯士數學家克里斯蒂安·哥德巴赫與瑞士數學家萊昂哈德·歐拉的通信中。用現代的數學語言，哥德巴赫猜想可以陳述為： “ 任一大於2的偶數，都可表示成兩個質數之和。 ”將一個偶數用兩個質數之和表示的方法，等於同一橫線上，藍線和紅線的交點數。

使用 Gauss，產出了 約 25,000 行 Lean 代碼，包含超過 1,000 個定理與定義。這類規模的形式化證明在歷史上常是重大里程碑，通常需多年努力才能完成。歷來最大型的單一形式化專案通常需要十年以上、堪稱研究生涯巔峰的成果，也僅比這大一個數量級（約 500,000 行代碼）。而 Lean 的數學標準函式庫 Mathlib 則大兩個數量級，擁有 約 2,000,000 行代碼、35 萬個 Lean 定理與定義，並由 600 多名貢獻者歷經 8 年建構完成。

內容摘要：

1. Gauss 完成了由知名數學家 陶哲軒（Terence Tao） 與 Alex Kontorovich 在 2024 年提出的強質數定理形式化挑戰。
2. 人類專家僅在該挑戰上取得「中期進展」，數學界在 18 個月後（2025 年 7 月）才完成較簡化的 中等版本（Medium version）。
3. Gauss 可自主連續工作數小時，並生成 25,000 行經過驗證的數學程式碼，其中包含 1,000 多個相互關聯的證明與定義。
4. Math Inc. 計劃在未來 12 個月內 將數學代碼量擴展 100 到 1,000 倍，以此作為訓練數據，推動「機器數學多面手（machine polymaths）」與「驗證型超級智慧（verified superintelligence）」的發展。

重要性：

複雜數學是 推理的基礎，而 AI 正快速掌握這一領域，這是 系統能創造新思想並加深我們對世界理解 的最強信號之一。隨著 Gauss 的突破，以及 Google、OpenAI 等 在國際數學奧林匹亞中獲得金牌，AI 在數學上的加速正在飛速發生。

Gauss 展現了形式化在未來如何擴展。目前，它仍依賴數學家提供的自然語言框架，並需要高階專家的指導與開發。預期未來版本的 Gauss 將更具能力與自主性。Math Inc. 團隊將開始部署這項技術，讓數學家與證明工程師能實際使用。目前Math Inc. 團隊正與部分數學家接洽，進行封測（beta testing）。你可以在此註冊 Gauss 早期使用權。若你有關於自動形式化的雄心計劃，歡迎與Math Inc. 團隊聯繫。（👉聯絡網址：https://www.math.inc/）

• 如果你對內容有共鳴、想分享想法，
• 歡迎在下方留言互動 💬 你的支持就是我持續寫作的動力！
• 📮 也歡迎來信交流：childbenefits@gmail.com