我们形式化基准中的缺陷：Lean定理证明的数据集缺陷与评估失败

用于LLM辅助Lean定理证明的基准常被视为天然可靠，因为每个解决实例都附带机器校验的证明。但内核只检查证明是否建立了形式化陈述；它不验证该陈述是否忠实编码了预期的非形式化问题，也不验证评估Harness对平凡或对抗性解的鲁棒性。我们审计五个广泛使用的Lean定理证明基准及其分支，使用语料规模的静态检查器发现4,833项发现——包括398项经机械认证的问题如反例、空洞定理和不健全公理。我们还记录了语义缺陷如缺失假设、问题简化、不完整或错误翻译及Lean特有的规范隐患。在修正子集上，缺陷既可虚高也可压低已报告的证明器分数。我们提出缺陷分类、一套自动化检查器与召回导向的语义审计提示，以及指导形式化数学数据集创建的发布标准。检查器、审计提示与修正后的数据集快照发布于https://github.com/Shashi456/atp-checkers。