4 道長期未解數學題被 AI 破解：新創 Axiom 如何把 AI 推向「可驗證推理」的新階段？
專注於數學推理的 AI 新創公司 Axiom，近期因其 AI 系統成功破解多道長期未解的數學問題，引發學界與科技圈關注。
不同於多數大型語言模型著重文字生成，Axiom 的目標是打造能產出並驗證數學證明的 AI 系統，方法結合了大型語言模型與專有的 AI 系統，讓推理結果可被形式化檢驗，從而達到「可證明正確」（provably correct）的解決方案。
Axiom 的 AI 系統 AxiomProver 破解四道長期未解的數學題
Axiom 開發的 AI 系統 AxiomProver，近期為四道長期未解的數學問題提供完整證明，這些成果已在數學研究社群中流傳，顯示 AI 數學能力的穩步進展。
AxiomProver 所解開的其中一項問題，是對 Chen–Gendron 猜想的完整證明：數學家 Dawei Chen 與 Quentin Gendron 五年前因受阻於數論中的一個奇特公式，僅能提出猜想而無法完整證明，過去 Dawei Chen 曾花費數小時嘗試利用 ChatGPT 尋求解答未果，直到與 Axiom 的顧問、知名數學家 Ken Ono 會面後，AxiomProver 在隔天早晨便產出完整證明。
此外，AxiomProver 也生成了對 Fel’s Conjecture（費爾猜想，是關於代數與數論中「數值半群 Numerical Semigroups」的一個數學難題）的證明。費爾猜想長年困擾數學研究者，在這個案例中，AxiomProver 從頭到尾獨立完成了證明，這也讓哈佛商學院教授 Scott Kominers 表示驚嘆，指出這不僅是 AI 全自動解題並即時驗證的成就，更在於其產出的數學具有「優雅與美感」。
AxiomProver 的所有證明皆透過 Lean 形式化語言進行驗證，這是一種專門的數學語言，可以讓推理過程與結果能被機器與人類檢驗正確性。雖然 Google 在 2024 年曾透過 AlphaProof 展示了類似概念，但 Axiom 執行長 Carina Hong 表示，其系統整合了更先進的技術手法，讓 AxiomProver 不僅是搜尋現有文獻，而是能發展出真正新穎的解題方法。
Axiom 正在打造可證明正確的「AI 數學家」
Axiom 由 24 歲的 Carina Hong 在 2025 年 3 月創辦，Carina Hong 曾是羅德學者（Rhodes Scholar）並就讀史丹佛大學博士班，後選擇輟學創業，專注於開發能進行數學推理的 AI 系統，目標是構建一位「AI 數學家」。
創業初期，Axiom 的辦公環境僅有一張塑膠折疊桌與朋友的備用沙發，但成員們從第一天起便對公司的使命感到振奮。Carina Hong 試圖在公司內建立一種「非階級化」的文化，她認為年齡與經驗只是「人為的概念」，並習慣與資深研究人員平起平坐地合作。
Carina Hong 表示，Axiom 的核心理念是讓 AI 不只是生成答案，而是能產出可被正式驗證的數學證明。「數學真的是現實的絕佳試驗場和沙盒，」Carina Hong 認為，這種可被證明正確的推理能力，除了在硬體驗證、量化金融與密碼學等領域具有極高的商業價值外，也能應用於網路安全，開發出對特定攻擊更具韌性的軟體。
Axiom 團隊目前約有 17 人，成員背景來自 Meta FAIR（基礎人工智慧研究實驗室）、Meta Generative AI 與 Google Brain 等頂尖研究團隊。Carina Hong 特別鎖定 FAIR 團隊進行招募，因為該團隊長期持續產出驚人的研究成果。
值得一提的是，Axiom 的技術長 Shubho Sengupta 是 Carina Hong 在咖啡店偶遇後加入的第一位成員。Carina Hong 透露，許多研究人員被公司的使命吸引，這使她在面對科技巨頭的留才方案時仍具競爭力，甚至有員工表示「致力於解決數學超級智慧將成為他們的成就」。
Axiom 透過可形式化驗證的 AI 系統，展示 AI 在數學推理領域的實際能力，並與傳統以語言生成為主的模型路線形成對比，這些成果也讓 Axiom 成為目前少數已實際產出可驗證數學證明的 AI 新創之一。親眼見證自身猜想被解開的數學家 Dawei Chen 比喻：「數學家並沒有因為計算機的發明而忘記九九乘法表。」他相信，AI 將成為一種新穎的智慧工具，甚至是「智慧合作夥伴」，為數學研究開拓更寬廣的視野。
＊本文開放合作夥伴轉載，資料來源：《Business Insider》、《Wired》，首圖來源：Unsplash