LLM 秒级把数学论文转成 Lean 代码,却给 Mathlib 埋下「特洛伊木马」

Machine Learning Street Talk · youtube · 2026-10-27

Machine Learning Street Talk 纪录片片段,《The Proof in the Code》作者 Kevin Hartnett 谈 AI 自动形式化的隐患:LLM 现在能在人力团队一小部分时间内把数学论文转成 Lean 形式化代码,但 Mathlib 社区发现这是一匹「特洛伊木马」——大量涌入的 Lean 代码缺乏 Mathlib 规范性定义所需的精确与简洁。

这本质上是 AI 生成内容泛滥问题的又一个缩影:生成快但质量与社区标准不匹配,维护者反而要为低质量的「快」付出代价。片段出自纪录片《Mathematics Just Changed Forever》,嘉宾包括 Kevin Buzzard、Jeremy Avigad、Leo de Moura 等。