AI解完題，研究為何還沒完成？25位數學家發聲

（媒角抵加／林承志綜合報導）陶哲軒等25位菲爾茲獎得主於2026年9月11日發表共同聲明，質疑AI公司以解決數學難題競逐模型表現，可能壓縮研究者理解方法與培育學生的過程。AI完成一道證明後，研究仍包括解釋推理、整理程式與建立可重用的方法；美國CMU研究者的球體堆積計畫，正呈現這些後續工作，也為台灣課堂與研究團隊提供檢視AI成果的具體方向。

關鍵資訊

• 聲明事件：25位菲爾茲獎得主共同署名，關注AI解題與數學研究目標的差異。
• 案例任務：研究者與Math, Inc.的Gauss合作，將既有球體堆積證明轉成Lean可檢查的程式。
• 人工工作：檢查定義與推理前提、改善程式結構、整理成其他研究者可使用的知識。
• 研究門檻：Lean為開源工具；理解進階證明及修改相關程式，仍需要數學與形式化訓練。

25位得主要求保留理解與傳授方法的時間

這份聲明以「數學領域中AI的嚴重目標錯位」為題，簽署者包括陶哲軒、Maryna Viazovska及Peter Scholze。聲明肯定AI促進數學研究與理解的潛力，同時認為，企業競逐解題成果的方向，與數學界重視的知識累積出現落差。

聲明指出，一個著名難題獲得解答後，數學家還會透過討論、簡化與寫作，整理其中的新方法，逐步形成學生能學習的內容。快速增加答案，仍需要有人解釋方法如何成立，以及它能用來研究哪些其他問題。

球體堆積計畫，讓電腦逐步檢查既有證明

球體堆積研究的是：同樣大小、互不重疊的球，在指定空間裡可以排得多密。Viazovska於2016年解決8維情況，之後與合作者完成24維結果。後來的形式化計畫，則把這些既有證明改寫成電腦可以檢查的形式。

Lean是一種程式語言與證明輔助工具。研究者必須明確寫下數學對象、假設及推理步驟，再由系統檢查。IEEE Spectrum報導，Sidharth Hariharan與合作者先建立人能閱讀的證明藍圖，標明各部分的關係與待完成工作，AI再參與補足程式。

Math, Inc.在官方成果說明中表示，Gauss以5天完成8維結果剩餘的形式化工作，接著用2週完成24維情況。公司也列出Hariharan等人先前建立的藍圖、定義與程式基礎，將成果描述為協助完成形式驗證。

驗證通過後，團隊繼續拆分與整理程式

計畫維護者在3月2日公開的紀錄中說明，收到Gauss的程式後，團隊檢查數學定義有無被修改、使用哪些推理公理，並進行人工與工具檢查。確認程式後，雙方同意共同公布成果。

後續工作包括精簡、重構、整理成可分別使用的部分，以及讓證明方法適用於更廣的情況。維護者肯定Gauss成果的規模與數學深度，也希望把程式整理到適合併入公共研究計畫、持續維護的程度。

到了9月8日，CMU（Carnegie Mellon University）刊出的訪談仍談到這項工作。Hariharan表示，團隊認為Math, Inc.的程式不易閱讀，因此繼續改善原有程式，讓其他人更容易重用與重現。他將AI成果視為重要里程碑，並持續使用Claude協助編輯及製作較小的程式片段。

學生還要練習說明每一步為何成立

Hariharan參與計畫的起點就包含學習。依維護者的回顧，他希望透過把Viazovska的證明寫成Lean程式，理解其中的數學。逐一補齊定義與步驟，也是他建立研究能力的過程。

25位得主的聲明同樣關注學生：教師安排研究題目時，也在培養提出新問題與理解方法的能力。研究成果的用途包含教學與傳承，學習者需要有機會追問每一步理由，並嘗試將方法用在其他題目上。

台灣研究與課堂，可要求答案附上推理與來源

對台灣使用AI協助研究或教學的團隊，可把交付要求訂得更具體：除了結果，還要附上問題的定義、推理說明、引用來源，以及可供檢查的程式。討論成果時，再請作者說明哪些步驟由AI協助、自己如何核對，以及方法的適用條件。

今年6月公布的《萊頓AI與數學宣言》已提出相近做法，包括揭露工具使用、提供完整引用，並由人類作者承擔結果正確性的責任。這些要求適用於研究流程；課堂評量則可依學生程度，保留自行說明、修改與延伸答案的練習。

Lean的官方文件與開源程式可供學習。若要進一步處理球體堆積這類進階計畫，參與者仍須理解相關數學與程式環境。先讓另一個人能沿著說明檢查推理、使用其中的方法，才能看見一份AI成果後續可以支持哪些工作。

資料來源與更新紀錄

• Math and AI：25位菲爾茲獎得主共同聲明，查閱日期2026年9月13日。
• 陶哲軒：聲明發布紀錄，2026年9月11日。
• CMU：AI Claimed to Verify a Proof; A Ph.D. Student Says Work Remains，2026年9月8日。
• 球體堆積計畫維護者：The Sphere Packing Project — The Story，2026年3月2日。
• Math, Inc.：Completing the formal proof of higher-dimensional sphere packing，公司成果說明，列示2026年2月形式化成果。
• IEEE Spectrum：Watershed Moment for AI–Human Collaboration in Math，文末註明刊於2026年5月紙本，查閱日期2026年9月13日。
• Lean官方網站與學習入口，查閱日期2026年9月13日。
• Leiden Declaration on Artificial Intelligence and Mathematics，2026年6月2日，與9月11日共同聲明為不同文件。
• 更新紀錄：2026年9月13日完成文字稿；球體堆積案例依公司、研究團隊與獨立媒體材料交代形式驗證及後續整理工作。