AI 是對TAO 已經做出的論文進行形式化

還得先有論文，或者至少是解法大綱。 AI 來做基本的證明補充。

所以，你得先有一個能行得通的證明辦法，然後才可能去問AI， 中間的證明它是否能補充上。尤其是那些需要驗證好多case的證明，AI才拿手。  整個program 是否成功，需要 （1）有個人設計的證明途徑，把大問題分成很多小部分 （2）你的AI program 能完成那些小部分。

“ 而陶哲軒在這篇博文裏，把需要死記硬背的勞動都抽象出來，交給了機器 ” 

“ 11 月，陶哲軒與 Yael Dillies 和 Bhavik Mehta 啟動了一個合作項目，目的是利用 Lean4 對自己之前關於 Freiman-Ruzsa（PFR）猜想的預印本論文進行形式化。” 

所有跟帖： 

• 這些本來是助手的工作 -wzg69- ♂ (105 bytes) () 12/07/2023 postreply 13:15:25

• 數學家沒助手。 -trivial- ♀ (0 bytes) () 12/07/2023 postreply 15:57:09