TheoremBench

TheoremBench 用 Lean4 中近百个经典定理评估 theorem prover 在长依赖链上的表现。它有 plain main 与 premised 两种版本，后者把一个主定理展开成相关 supporting subtheorems，用来衡量内部证明结构上的部分进展；实验显示 explicit premises 明显改善 Lean4-capable prover。它比竞赛题更接近真实形式化数学开发，因为指标会暴露模型是否只是刷容易子定理和输出冗长 tactic traces。