Definition Grounding / ReuseBench 发现：LLM 形式化定义常能 typecheck，却只有 25%–50% 真能支撑后续理论

Pan、Szegedy 等于 10 月 13 日提出 definition grounding：不再只判断 AI 生成的 Lean definition 是否能编译，而是用后续 layered statements 持续测试该定义是否足够一般、idiomatic 且可复用，并据此迭代修订。ReuseBench 实验显示，LLM 从 textbook text 形式化的一组 definitions 中，只有约 25%–50% 能与全部后续 statements 兼容；澄清 informal definitions 后，跨模型平均兼容率最高可到 77.5%。作者还发现，只陈述少量 basic properties、暂不要求证明，就能以约完整 definition-formalization 11% 的成本显著增强 model judges 对 compatibility defects 的检测。