作者Bugquan (靠近邊緣)
看板Math
標題Re: [其他] 確定性的失落？創造性的無限？(上)
時間Thu Nov 6 11:24:36 2025
※ 引述 《ginstein (邁向學術之路)》 之銘言：
:
: 本文為前沿數學探索，是數普文非學術文、非公認理論，
:
: 盼能促進 AI 數學家早日到來。
:
現在當然有的數學家引入AI
像是Terence Tao自己就玩的不亦樂乎，還有Timothy Gowers也是
偶爾會分享自己用AI 搞定了什麼
但是最大的問題是，你看這倆菲爾茲獎得主，AI的證明有沒有了唬爛或是跳步之類的
他們兩個稍微排查很快就能得出結果了
但是對於其他人門檻不夠的，最多只能當為輔助工具來用
主要步驟還是得靠自己，不然有時候被AI騙了都不知道
--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 106.64.112.48 (臺灣)
※ 文章網址: https://webptt.com/m.aspx?n=bbs/Math/M.1762399478.A.967.html
1F：→ mantour : AI不斷快速嘗試各種思路，然後可以自己初步排除掉 11/06 14:27
2F：→ mantour : 一些明顯錯誤的，剩下的candidate再給數學家去檢查 11/06 14:27
3F：→ mantour : 。問題是AI提供的解答中黃金：垃圾的比率是否足夠 11/06 14:27
4F：→ mantour : 高，如果垃圾比率太高也是形同浪費數學家檢查的時 11/06 14:27
5F：→ mantour : 間。 11/06 14:27
6F：推 LPH66 : 話說回來, 我看到有一篇論文是他們用 ChatGPT 產生 11/06 20:35
7F：→ LPH66 : 了 Lean 程式碼並且成功編過了, 這種應該算是生成式 11/06 20:36
8F：→ LPH66 : AI 的一種意外應用方式吧 (Lean 程式碼能編過表示 11/06 20:36
9F：→ LPH66 : 邏輯推理是通的) 11/06 20:36
10F：→ LPH66 : 這是那篇論文, 做的是 Erdos 曾經懸賞一千元的猜想 11/06 20:38
12F：推 mantour : 謝謝L大分享的論文 11/06 22:13
13F：推 pmove : LLM靠的還是機率吧，能編過不代表邏輯是通的（回L大 11/07 06:54
14F：→ pmove : ），至於機率是否能產生邏輯，見人見智，但有些人認 11/07 06:54
15F：→ pmove : 為無法，所以AI可能還需要基本架構的革新 11/07 06:54
16F：→ pmove : 編譯過，只代表compile 會過，不代表執行結果正確或 11/07 07:44
17F：→ pmove : 邏輯通 11/07 07:44
18F：推 LPH66 : 那是其他程式語言, 但這篇論文用的是專門用於證明的 11/07 08:50
19F：→ LPH66 : Lean, 就我所知 Lean 程式編過就表示邏輯推論是通的 11/07 08:50
20F：→ LPH66 : 這篇論文的作者有說他們在這之前不會 Lean 11/07 08:52
21F：→ LPH66 : 但經 ChatGPT 的輔助他們能夠將整篇論文的多數結果 11/07 08:54
22F：→ LPH66 : (特別是主要定理) 全部都用 Lean 驗證過 11/07 08:54
23F：推 pmove : 回樓上，受教了，謝謝。 11/07 13:48
25F：→ mantour : LLM很擅長翻譯，把論文的定理轉化成Lean再去檢查推 11/11 07:14
26F：→ mantour : 論是否通過應該辦得到，不過如果使用的數學家本身 11/11 07:14
27F：→ mantour : 也不是很熟悉Lean，有沒有可能在LLM輔助下寫出的Le 11/11 07:14
28F：→ mantour : an跟本來要證的定理其實是不等價的 11/11 07:14
29F：推 LPH66 : 原論文也有討論到這個問題, 但恰巧他們這個問題 11/12 22:58
30F：→ LPH66 : 比較著名 (Erdos 懸賞過的問題) 有其他人已經做好了 11/12 22:59
31F：→ LPH66 : 這種「翻譯」 11/12 22:59
32F：推 ginstein : 創作不易，感謝回文評論！ 11/18 09:12