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

[Bugquan (靠近邊緣)]

※ 引述 《ginstein (邁向學術之路)》 之銘言：
: 　
: 本文為前沿數學探索，是數普文非學術文、非公認理論，
: 　
: 盼能促進 AI 數學家早日到來。
: 　

現在當然有的數學家引入AI

像是Terence Tao自己就玩的不亦樂乎，還有Timothy Gowers也是

偶爾會分享自己用AI 搞定了什麼

但是最大的問題是，你看這倆菲爾茲獎得主，AI的證明有沒有了唬爛或是跳步之類的

他們兩個稍微排查很快就能得出結果了

但是對於其他人門檻不夠的，最多只能當為輔助工具來用

主要步驟還是得靠自己，不然有時候被AI騙了都不知道

--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 106.64.112.48 (臺灣)
※ 文章網址: https://www.ptt.cc/bbs/Math/M.1762399478.A.967.html
→ mantour     : AI不斷快速嘗試各種思路，然後可以自己初步排除掉
→ mantour     : 一些明顯錯誤的，剩下的candidate再給數學家去檢查
→ mantour     : 。問題是AI提供的解答中黃金：垃圾的比率是否足夠
→ mantour     : 高，如果垃圾比率太高也是形同浪費數學家檢查的時
→ mantour     : 間。
推 LPH66       : 話說回來, 我看到有一篇論文是他們用 ChatGPT 產生
→ LPH66       : 了 Lean 程式碼並且成功編過了, 這種應該算是生成式
→ LPH66       : AI 的一種意外應用方式吧 (Lean 程式碼能編過表示
→ LPH66       : 邏輯推理是通的)
→ LPH66       : 這是那篇論文, 做的是 Erdos 曾經懸賞一千元的猜想
→ LPH66       : https://arxiv.org/abs/2510.19804
推 mantour     : 謝謝L大分享的論文
推 pmove       : LLM靠的還是機率吧，能編過不代表邏輯是通的（回L大
→ pmove       : ），至於機率是否能產生邏輯，見人見智，但有些人認
→ pmove       : 為無法，所以AI可能還需要基本架構的革新
→ pmove       : 編譯過，只代表compile 會過，不代表執行結果正確或
→ pmove       : 邏輯通
推 LPH66       : 那是其他程式語言, 但這篇論文用的是專門用於證明的
→ LPH66       : Lean, 就我所知 Lean 程式編過就表示邏輯推論是通的
→ LPH66       : 這篇論文的作者有說他們在這之前不會 Lean
→ LPH66       : 但經 ChatGPT 的輔助他們能夠將整篇論文的多數結果
→ LPH66       : (特別是主要定理) 全部都用 Lean 驗證過
推 pmove       : 回樓上，受教了，謝謝。
→ pmove       : https://reurl.cc/KOxz1j
→ mantour     : LLM很擅長翻譯，把論文的定理轉化成Lean再去檢查推
→ mantour     : 論是否通過應該辦得到，不過如果使用的數學家本身
→ mantour     : 也不是很熟悉Lean，有沒有可能在LLM輔助下寫出的Le
→ mantour     : an跟本來要證的定理其實是不等價的
推 LPH66       : 原論文也有討論到這個問題, 但恰巧他們這個問題
→ LPH66       : 比較著名 (Erdos 懸賞過的問題) 有其他人已經做好了
→ LPH66       : 這種「翻譯」
推 ginstein    : 創作不易，感謝回文評論！