Vibe News

大模型最近用Lean证明工具，在纳维斯托克斯方程相关的一条数学命题上跑出机器验证的证明。一位工程师却撰文说，这恰恰是他更看空大模型的理由。他解释，数学证明是最理想的场景：命题经过数十年审核，验证器也被反复审计，很难被蒙混过关。可现实里的知识工作大多没有这种严格规范，写规范是稀缺技能，成本常常比动手做还高，硬件行业验证工程师往往是设计工程师的三倍。人工审核同样靠不住，他举了xz后门和明尼苏达大学伪造补丁混进linux内核的旧案。评论区里，有人说这话在否认现在的实际能力，也有人反问，人类专精一门技能也要靠大量训练。