IXThinker·2025-11-07 11:00

陶哲軒與ChatGPT合作 完成千行Lean證明

數學家陶哲軒讓ChatGPT把複雜數學論文翻譯成Lean代碼，人機合作完成形式化證明。AI能理解內容並寫出正確命題，卻常在關鍵步驟卡關，最終以1125行通過驗證的代碼收結。

一場實驗

陶哲軒盯着屏幕，Lean像刻薄裁判不斷吐出紅字；反覆拉扯後報錯歸於寂靜，1125行代碼落定——埃爾德什第613號問題的複雜反例，被逐行核查進形式化世界。寫手是ChatGPT，思路由陶哲軒把舵。