开发者批评 AI 产的 700 个 Lean 证明「潦草难读」是失败

bradneuberg · x · 2026-10-19

工程师 Brad Neuberg 引用 Ted Pavlic 的观点并评论:真正的智能不只是给出(看似合理的)解,还要能清晰传播给使用者——「不传播就不是科学」。

他的核心论点:AI 系统产出的约 700 个 Lean 数学证明潦草、复杂、纠缠不清,我们应当以更高标准要求 AI agent——像要求人类天才一样,产出优雅、干净、可解释的工作;不可理解的代码或证明就是失败,是潦草工作与潦草思考的标志。