ProofGap 用 26,116 个局部 Lean obligations 细粒度评测数学证明模型，而不是只看整题是否完成

ProofGap 从 B. P. Demidovich《数学分析习题集》3,015 道题的自然语言解答中抽取并对齐局部证明缺口，形成 26,116 个 formal proof gaps。每个任务直接给出局部 Lean context 与 target，把“这一步会不会证明”从整条 proof composition 中拆出来，从而能更精确定位模型的 step-level formal reasoning failure；作者同时指出，这类局部 obligations 未来也可用于 proof-verification pipeline，但仍需要可靠的语义翻译与顺序组合。