GPT-6 Astra 攻克類哥德巴赫猜想：Lean 形式化驗證已全部通過

數學家們大概是全世界對 AI 幻覺最沒有耐心的群體，畢竟推導裡只要錯了一個符號，整座大廈就會跟著坍塌。但如果把推導過程直接扔進嚴格的機器證明系統裡跑一遍，事情就不一樣了。

研究者 Captain Sude 在 GitHub 上公開了一個數學專案，宣佈藉助 GPT-6 Astra 成功攻克了一項關於劉維爾函式（Liouville function）的類哥德巴赫猜想。更關鍵的是，整套證明已經完全寫成了 Lean 4 程式碼，並通過了嚴格的形式化機器驗證。

把偶數拆成兩個奇數質因子的數

很多人都知道著名的哥德巴赫猜想：任何大於 2 的偶數，都可以寫成兩個質數之和。質數本身只有它自己一個質因子，數量正好是 1，也就是奇數個。

這次被證明的問題，其實是哥德巴赫猜想的一個著名近親。在數論中，劉維爾函式 $\lambda(n)$ 用來標記一個正整數包含多少個質因子。如果把重數也算進去，質因子總數是奇數，函式值就等於 -1；如果是偶數，函式值就是 1。

這次證明的核心定理是：每一個大於 2 的偶數，都能表示成兩個劉維爾函式值都是 -1 的正整數相加。也就是說，$N = a + b$，且 $a$ 和 $b$ 的質因子個數都是奇數。

這個問題早在 2018 年 8 月就被使用者 Pablo 提到了數學論壇 MathOverflow 上，數學家 Mangerel 的論文則將其歸功於 Shusterman。此前數學界已經有了一些積累，包括 Bloom 的尺度觀察，以及 Mangerel 的剛性和交換缺陷論證。

據專案介紹，GPT-6 Astra 給出的是一條初等證明路線，巧妙利用了兩個交換對稱性、一種下降法以及經典的二次互反律，最終把這塊硬骨頭啃了下來。

Lean 4 零漏洞把關，不給幻覺留退路

AI 做數學題最怕的是一本正經地胡說八道。但這次研究者沒給它留任何鑽空子的機會，而是把整套數學論證完整搬進了互動式定理證明器 Lean 4 裡。

程式碼鎖定了 Lean v4.34.0-rc2 和 mathlib 的特定提交版本。專案記錄的本地構建、公理審計和證明路徑審計全部顯示通過。

根據公開的公理審計日誌，最終定理只依賴了 Lean 語言核心內建的三條基礎邏輯公理：命題外延性（propext）、經典選擇公理（Classical.choice）和商健全性（Quot.sound）。

整套證明裡沒有任何寫著「sorry」的未完工漏洞，也沒有人為偷塞任何未經檢驗的額外數學假設。每一次提交還會通過 GitHub Actions 觸發全新的自動構建和雙重審計，確保每一步推理都堅如磐石。

為什麼重要

我們認為，這項成果最亮眼的地方，在於它再次驗證了大模型與形式化驗證工具結合的巨大威力。

過去大模型參與數學研究，最讓人頭疼的就是人工驗算的成本，往往需要頂尖數學家花上幾個星期去挑刺和排查幻覺。現在藉助 Lean 這樣的定理證明器，AI 負責發散思維尋找巧妙的證明路徑，機器核心負責像編譯器一樣死守邏輯防線。只要程式碼跑通、審計綠燈，整個數學界就能直接承認結論的正確性。

對於純數學研究者來說，這套工作流正在從實驗性玩具變成真正的生產力工具。它不僅能幫學者驗證猜想，甚至能從以往數學家留下的半成品框架中，自己摸索出一條兼顧下降法與互反律的初等路徑。

從大模型的競爭格局來看，OpenAI 等前沿廠商把 Astra 級別的推理能力推向形式化定理證明，直接切中了邏輯推理的最硬核戰場。比起寫寫營銷文案或生成程式碼，這種能在嚴格公理系統裡從頭到尾走通長鏈條演繹的能力，才是通用人工智慧邁向嚴謹科學研究的核心分水嶺。