TheoremBench：评估大语言模型在形式化数学中的定理证明能力

针对现有评估多集中于竞赛题而忽视长依赖数学推导的问题，本文提出 TheoremBench，一个基于 Lean4 的基准测试。该基准包含近百个经典定理，提供纯目标版和含前提版两种形式，后者将定理扩展为包含自动提取子定理的结构化任务族，以评估部分证明进展。实验表明，显式前提显著提升模型性能。新引入的定理覆盖率和令牌效率指标揭示了当前证明器偏向简单子定理且证明轨迹冗长低效的局限，为形式化推理能力提供了更细粒度的评估视角。