Re: [其他] 確定性的失落？創造性的無限？(上)

[Bugquan (靠近邊緣)]

※ 引述 《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://www.ptt.cc/bbs/Math/M.1762480024.A.346.html
→ xcycl       : 這邊有點太神話 Lean ，它並不具備「理解」的能力
→ xcycl       : 簡單說是數理邏輯（或型別論）的實作，能夠檢查證明
→ xcycl       : 的有效性。因為語言很底層，要把現代數學完整形式化
→ xcycl       : 而且要能夠以數學家可以理解的形式是還有一段路要走
→ mantour     : 意思是在把我要證明的定理，翻譯成Lean語言，跟Lea
→ mantour     : n語言中發現的定理翻譯成人能懂的命題，這兩個轉換
→ mantour     : 的過程可能還有困難和錯誤。結果是機器實際證明出
→ mantour     : 的東西，跟我以為機器證明出的東西，可能根本是不
→ mantour     : 同的。是這樣嗎？
→ xcycl       : 這兩個翻譯是普遍性的問題，就想像教科書所有的命題
→ xcycl       : 全部都只用數理邏輯的符號表達
→ xcycl       : 旁邊可以用自然語言的註解，但 Lean 只看符號的部分
→ xcycl       : 就跟寫程式一樣，預期的行為跟實際可能不一樣
→ ginstein    : 創作不易，感謝回文評論！
→ ginstein    : B大比較理想,我設想利用轉譯原理翻譯標準分析就好
→ ginstein    : https://www.zhihu.com/pin/1966294562063513595
→ ginstein    : 可以參考上篇想法，理想是自發從零到一，現實給一
→ ginstein    : 讓 AI 產生十百千萬的結果比較實際