论文
Discover and Prove：面向Lean 4困难模式自动定理证明的开源智能体框架
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
摘要
大多数自动定理证明（ATP）基准把最终答案嵌入形式化命题之中——我们将这一惯例称为“Easy Mode”（简单模式）——相对于人类参赛者所面对的情形，这种设计简化了任务，并可能导致对模型能力的高估。我们把更严格、更贴近现实的设定称为“Hard Mode”（困难模式）：系统必须在构造形式化证明之前独立发现答案。为支持 Hard Mode 研究，我们做出两项贡献。其一，我们发布 MiniF2F-Hard 与 FIMO-Hard，即两个广泛使用的 ATP 基准经专家重新标注的 Hard Mode 版本。其二，我们提出 Discover And Prove（DAP），一个智能体框架：它使用带显式自我反思的 LLM 自然语言推理来发现答案，然后将 Hard Mode 命题改写为 Easy Mode 命题交给现有 ATP 证明器。DAP 创下新的最优水平：在 CombiBench 上，它将解决的问题数从 7（此前 SOTA，Pass@16）提高到 10；在 PutnamBench 上，它成为首个在 Hard Mode 下形式化证明 36 个定理的系统——同时揭示出：在最先进 LLM 答案准确率超过 80% 的同一批问题上，形式化证明器只能搞定不足 10%，暴露出一个 Hard Mode 基准特别适合度量的巨大差距。
