Type-check filtering + self-consistency 显著提升 Lean autoformalization，并发布 research-level RLM25 与 ProofNetVerif

Poiroux、Weiss、Kunčak 与 Bosselut 系统分析 Lean 4 autoformalization 的生成与评测方法，提出扩大 type-check filtering 并结合 self-consistency，在 ProofNet 上带来最高 +18.4 个百分点的绝对准确率提升。论文同时发布 RLM25 research-level mathematics dataset、修订版 ProofNet 和带正确/错误配对标签的 ProofNetVerif，用于更可靠地评估 formal statement fidelity。