MathAdv：定理证明者知道什么、推理、形式化和概括

形式定理证明能够对数学推理进行机器验证的评估，但现有的基准通常强调聚合证明的准确性，集中于狭窄的数学范围，并为等效重新表述提供有限的稳健性证据。我们推出 MathAdv，这是一个跨越本科生和研究生数学 13 个领域的诊断基准。除了 Lean 4 定理证明之外，MathAdv 还提供最多三个辅助任务：探索数学知识的多项选择题、隔离非正式推理的填空题以及测试问题呈现稳健性的专家设计的转换。我们对当代定理证明者的评估得出了四个发现：形式化仍然是一个主要瓶颈；不同数学领域的表现差异很大；自然语言指导有助于通用 LLM，但可能会阻碍证明专用模型；数学上等效的重新表述暴露了巨大的鲁棒性限制。总之，这些结果显示了组件式评估如何揭示模型功能和故障模式，从而聚合定理证明准确性所掩盖的内容。数据集和评估脚本可在 https://github.com/margotyjx/MathAdv.git 获取。