Lean数学定理库充斥AI生成PR代码

[1/3] Lean 数学定理库现在充斥着大量 AI 生成的 PR 代码，都用 LLM-generated 标签标记出来了。我随手挑了几个有意义的标题（那些重构改名类的除外），目前还没发现一个被合并的。2300 多个等待合并的 PR，昨天一天合并了 74 个，最大的也就100来行改动。几百人一起号称构建整个形式化数学，绝大多数人专挑简单的事情做。我觉得这个项目已经被玩坏了。