FormalProofBench 将 formal theorem proving 评测推进到研究生级数学，并同时报告成本、延迟和工具失败

FormalProofBench 构建 private benchmark，每道题同时给自然语言题目与 Lean 4 statement，要求模型输出由 Lean checker 接受的完整证明。题目来自 qualifying exams 与标准教材，覆盖 analysis、algebra、probability、logic 等 advanced undergraduate / graduate-level 数学。作者用 agentic harness 评测多种 frontier models，最佳 foundation model 仅 33.5%，并进一步分析 tool use、failure modes、cost 与 latency。