发现与证明：用于 Lean 4 困难模式自动定理证明的开源智能体框架

大多数自动定理证明基准将答案嵌入形式陈述中（“简单模式”），低估了任务难度。本文提出更真实的“困难模式”，要求系统独立发现答案后再构建证明。为此，我们发布了 MiniF2F-Hard 和 FIMO-Hard 两个专家重标注的基准，并推出“发现与证明”（DAP）智能体框架。该框架利用大模型的自然语言推理及显式自我反思来发现答案，随后将问题转化为简单模式供现有证明器处理。实验表明，DAP 在 CombiBench 和 PutnamBench 上均创下新纪录，揭示了大模型在答案准确性上远超形式证明器的现状。