※ 引述 《Bugquan (靠近邊緣)》 之銘言： : 推 LPH66 : 話說回來, 我看到有一篇論文是他們用 ChatGPT 產生 11/06 20:35 : → LPH66 : 了 Lean 程式碼並且成功編過了, 這種應該算是生成式 11/06 20:36 : → LPH66 : AI 的一種意外應用方式吧 (Lean 程式碼能編過表示 11/06 20:36 : → LPH66 : 邏輯推理是通的) 11/06 20:36 : → LPH66 : 這篇論文的作者有說他們在這之前不會 Lean 11/07 08:52 https://xenaproject.wordpress.com/2025/10/22/formal-or-not-formal-that-is-the-qu estion-in-ai-for-theorem-proving/ 根據 Kevin Buzzard（倫敦帝國學院教授，https://reurl.cc/LQ0Ddx）的觀點，我們來探 討 AI 證明數學猜想時的核心問題。 小知識：關於 Kevin Buzzard 這位數學家正帶領團隊，試圖利用 Lean 形式化證明費馬最後定理。他甚至邀請到他的指導 教授 Richard Taylor（費馬最後定理證明關鍵貢獻者之一）來協助制定一套現代化且更具 可行性的形式化藍圖。 (參考：https://imperialcollegelondon.github.io/FLT/blueprint/) Kevin Buzzard 在文章中指出，AI 證明數學時面臨兩大挑戰： 1. AI 的「幻覺」與證明可靠性 問題核心： 像大型語言模型（LLM）這樣的 AI 存在「幻覺」（Hallucination）問題。 在數學證明中，只要證明過程出現一個幻覺，就足以完全破壞整個數學論證的有效性。 形式化的作用與局限： 如果我們要求 AI 在提供證明的同時，也以 Lean 形式化語言呈 現，是否就能高枕無憂？ 答案是否定的。 雖然 Lean 可以以超人類水平校驗邏輯步驟，但人類仍然需要仔細檢查 ：定理的陳述和證明的過程是否被正確地翻譯成了 Lean 語言。 確保「人類想證明的」與「Lean 實際檢查的」是同一件事，是至關重要的環節。 2. AI 配合 Lean 的發展瓶頸 問題核心： AI 與 Lean 混合系統能走多遠？ Buzzard 的觀點： 他認為目前的瓶頸在於，即便是最好的形式化數學函式庫（如 Lean 的 mathlib），仍不具備理解大多數現代研究級數學所需的「定義」。 範例： 目前的定理證明器尚不了解（或缺乏足夠形式化定義）這些複雜但又極其重要和 常用的數學對象，例如： Tate-Shafarevich 群 Calabi-Yau 簇 代數疊 (algebraic stacks) 自守表示 (automorphic representations) 因此，在 AI 能夠真正協助進行研究級數學證明之前，仍需要人類研究人員投入時間，為 L ean 等證明器提供和形式化這些現代數學的基礎定義。 --

※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 27.53.161.22 (臺灣) ※ 文章網址: https://webptt.com/m.aspx?n=bbs/Math/M.1762480024.A.346.html