RLMEval 用真实 Lean Blueprint 项目评测 research-level proving，最佳模型仅 10.3%，揭示 benchmark→研究数学的巨大落差

Poiroux、Bosselut 与 Kunčak 构建 RLMEval，从 6 个真实 Lean Blueprint formalization projects 中抽取 613 个 research-level theorems，用于评测 neural theorem proving 与 proof autoformalization。论文发现已有 curated benchmark 上的进展不能直接迁移到真实研究形式化，最佳模型 pass rate 仅 10.3%。