TaoBench：自动定理证明大模型能否泛化到 MathLib 之外？

当前自动定理证明（ATP）基准严重依赖 MathLib，导致评估存在偏差。本文提出 TaoBench 基准，基于陶哲轩《分析 I》从零构建数学概念，旨在测试 ATP 系统在新定义框架下的鲁棒性。通过构建代理流水线提取独立环境，并将问题翻译为等价的 MathLib 形式进行对比。实验显示，尽管最先进模型在 MathLib 中表现良好，但在等价定义的 Tao 框架下性能平均下降约 26%，表明主要瓶颈在于跨定义框架的泛化能力而非任务难度。