[1/3] 我上个学期含辛茹苦地给两个学生讲 HOL 定理证明和形式化概率论，其中那个印度女学生一直忙着打工赚钱，然后又因 ”家庭原因“ 回国了两个月，三天前她终于发给我阶段性成果。竟然是用 “生成式 AI” 从现有的 Isabelle 形式化证明代码翻译到 HOL4 的，还让我帮忙 “调试”。这些生成的代码表面上看像那么回事，其实根本狗屁不通，就是个 Standard ML+OCaml+HOL4+HOL-Light+Isabelle 的大杂烩儿。我今天跟这个学生开例会特地邀请我导师一同参加。我导师说的很含蓄——他说这些生成代码就是垃圾，调试它们比从头写要难多了。由此可见 ”生成式 AI” 目前在交互式定理证明领域毫无用处，除了能保证左右括号互相匹配以外，就只剩下满口喷粪了。