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