【導讀】星星之火，可以燎原！證明的尊嚴在於可驗證；這一次，GPT-5讓數學證據落在了代碼裡。
一雪前恥，ChatGPT為OpenAI「正名」！
被Hassabis吐槽太尷尬之後，GPT-5真啟發了新的數學結論。
OpenAI的科學家Sebastien Bubeck高調宣揚GPT-5破解了十道Erdős難題。
但被指出GPT並非解決了Erdős問題，而是找到了已經解決這些問題的文獻。
之後，他刪除了推文並表示自己並非有意誤導。
Yann LeCun斥之為「自食其果」：OpenAI被他們自己的GPTards所害。
之後，他在LinkedIn上的發帖，明顯低調多了：
現在，事情來了反轉——
Sebastien Bubeck被「冤枉」了，AI的確在加速科學進步。
反轉，ChatGPT為OpenAI「正名」
昨天，這個故事來了一個反轉——
普林斯頓大學數學博士Boris Alexeev（下圖左）和俄亥俄州立大學副教授Dustin G. Mixon（下圖右）發現，懸賞1000美元的707號Erdős問題，在被提出前30年，就已經被解決了。
論文地址：https://borisalexeev.com/pdf/erdos707.pdf
事情有些離譜，堪稱數學家的「虛空索敵」——
答案比問題早30年，但直到前不久，外界還普遍以為問題沒有被解決！
目前，707號Erdős問題已被標註為「Disproved」（被證偽）。
傳送門：https://www.erdosproblems.com/go_to/707
這次，Sebastien Bubeck扳回一局，發推表示：
看來文獻檢索，終究不是件簡單的事😅。
潛臺詞是說，GPT-5過去找到的10個已有解答，並非易事。
但後面的更精彩。
ChatGPT輔助數學證明，陶哲軒點贊
兩位數學家也懷疑結果，於是決定用GPT5在Lean中生成形式化證明。最後，居然成功了！
注意⚠️：ChatGPT和Lean被列入了合作者，但論文內容中還是作者「手搓」。
不過，人類在這個過程中可沒少花功夫，需要不斷給GPT5提供反饋，完善形式化論證。
在「Erdős的難題」網站上，近期湧現了不少成功案例，研究者利用大語言模型在現有文獻中找到了埃爾德什問題的解法。
值得一提的是，用AI找到Erdős問題的「已有答案」，陶哲軒之前已經成功展示過概念驗證。
陶哲軒也注意到了這次新證明，認為這是計算機輔助證明的有趣例子。
在研究過程中，兩位數學家確信Lean能幫助驗證已有論文的真偽，但當時既不熟悉Lean，又覺得其操作界面不夠友好。
然而由於ChatGPT能編寫Lean代碼，他們決定通過氛圍編程（vibe coding）方式形式化整個證明。
這個過程耗時約一週，體驗頗為煎熬，但最終意外成功了——
形式系統中，ChatGPT嚴格證明了Erdős猜想的否命題。
最終生成的證明超過6000行代碼，包含26個定義、169個引理和4個定理（最終的反例驗證部分）。在普通筆記本電腦上，代碼驗證耗時不足半分鐘。
經過數輪往復的互動後，Boris和Dustin認為，如果大語言模型的接口能與Lean深度整合，並針對這種交互方式進行適當微調，許多問題都會大大緩解。
即使是少量的針對性優化，也足以讓這種「人機協作證明」的體驗更加流暢、自然。
陶哲軒高度認可這次AI輔助證明。他表示，這是在研究論文中負責任地使用LLM輸出的罕見用例之一：
重要的是，沒有任何LLM生成的輸出被直接放入正文（除了為了說明目的引用LLM生成的 Lean 代碼片段外）；
相反，這種輸出僅用於完全可驗證的上下文中（在本例中，用於生成可由 Lean進行類型檢查的代碼）。
不過，陶哲軒強調：「Lean形式化只是對人類證明的補充，並不能取而代之。」
此外，他幾乎可以預見會有一些誇張的報道——「這回LLM真解決了一個Erdős問題！」
—— 但事實遠比這複雜微妙。要得出任何結論，都需要先把來龍去脈仔細梳理清楚。
GPT-5推動研究，端倪初現
加州大學歐文分校數學教授Paata Ivanisvili，也把ChatGPT列為論文合作者。
新論文由數學教授Paata Ivanisvili、2022屆中科大本科校友Xinyuan Xie (謝新元)合作，ChatGPT是第一作者。
這一探索起源於兩人請GPT-5 Pro在公開的未解問題（下文👇）中尋找反例。
- 鏈接：https://simons.berkeley.edu/sites/default/files/openprobsmerged.pdf
- 標題：Real Analysis in Computer Science：A collection of Open Problems
經過若干數值實驗後，它提出了一個關於帶擦除的非交互相關蒸餾問題（Non-Interactive Correlation Distillation, NICD with erasures）的反例：
一個定義在5比特上的布爾函數，在擦除參數p=0.40時，其 E∣f(z)∣值 嚴格大於 5比特多數函數（majority function）的對應值。
他們記錄了這一發現並驗證全部計算過程。
這一結果與線性閾值函數中關於「Majority is Least Stable」的經典反例，形成了呼應：即便AI只是將已知的反例模式應用於新場景並加以驗證，其貢獻依然值得肯定。
傳送門：https://arxiv.org/abs/1703.07657
這是理論計算機科學中AI的「星星之火」：以往大語言模型（LLMs）多用於文獻檢索或數值輔助，而此次則真正生成了一個具體、有限且可驗證的反例。
此外，UCLA的數學教授Ernest Ryu，藉助GPT-5 Pro解決了一個凸優化領域的開放問題。
儘管模型約有80%的證明嘗試是錯誤的，卻提出了多條新穎思路。
GPT-5 Pro的具體貢獻：
- 給出了最終可行的證明思路與論證框架
- 通過快速排除無效路線，大幅加速了探索進程
這項工作耗時約12小時，分3天完成。事後，Ernest Ryu回想起來，這個證明其實非常簡單。
ChatGPT生成的證明的關鍵步驟：
Ernest Ryu總結了他自己的貢獻：
- 篩選出不正確的論點，並積累一系列正確的事實。
- 識別有前景的新推理思路，並引導 ChatGPT 進一步探索這些思路
- 認識到何時某個策略已被充分探索，並決定何時轉向其他方向。
他還將繼續開發這個項目，並將結果發表在專業的優化理論期刊上，並分享更新和未來的部分。
被吐槽的OpenAI科學家Sebastien Bubeck，也復現了類似的場景——
GPT-5可以證明有趣的數學結論。
不過，人類實際上搶先了gpt-5 一步:-)。另一位作者完全填補了差距，證明了新的界限。
GPT-5提出的證明：
GPT-5已經提出了多個具有研究價值的新想法。不僅如此，它實際上自己想出了大部分提示詞：
傳送門：https://github.com/Dicklesworthstone/model_guided_research
AI輔助研究大門，正在打開。
或許，歷史銘記的不是那句「太尷尬了」，而是那行悄無聲息通過編譯的qed。
參考資料：
https://x.com/SebastienBubeck/status/1980804267524116569
https://x.com/PI010101/status/1981014478969033156
https://borisalexeev.com/pdf/erdos707.pdf
https://mathstodon.xyz/@tao/115416211466664814
https://x.com/slow_developer/status/1980990021248160009
本文來自微信公眾號“新智元”，編輯：KingHZ ，36氪經授權發佈。
