Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4

Idea

Discover and Prove（DAP）将自动定理证明拆成发现答案与形式化证明两个环节，并用 Hard Mode benchmark 显式要求系统自己求出未知量。Discovery Module 先以自然语言推理、自检和修正产生答案，再把答案填入 Lean 4 statement，交给现有 prover 证明，因此可以复用擅长 Easy Mode 的 ATP 模型。

Research Problem

很多 ATP 数据集已在待证 statement 中写入最终答案，系统只需证明已知结论；这会绕开竞赛数学中关键的答案发现过程。部分 formalization 还弱化了原题目标或添加额外前提，导致高证明通过率不能完整反映原问题求解能力。直接把两个 sorry 的 Hard Mode 问题交给传统 prover，也超出了其主要训练任务。

Insight

自然语言 reasoning model 与 formal prover 的优势互补：前者更容易探索候选答案，后者提供机器可检查的推导。以候选答案将两个待完成目标变为一个证明目标，能够连接两类模型，同时分开测量答案发现正确率和形式证明成功率，暴露两者之间的能力差距。自检本身只是发现阶段的启发式，最终证明仍由 Lean 检验。

Method

1. 对原始自然语言题目生成解答过程；同一 reasoning LLM 检查推理并输出 error report，发现错误后据此修正，反复 self-verification/self-correction。实验使用 GPT-OSS-120B，最多尝试 30 轮，失败则退回未经自检的候选答案。
2. 利用原始 Hard Mode Lean statement、题目和推理结果执行 rewriting，将未知答案对应的 sorry 替换为候选解，生成只剩证明 sorry 的 Easy Mode statement。
3. 将重写问题交给 Goedel-Prover-V2-32B，采样正式证明并通过 Lean 4.15.0 与 KiminaServer 检查；主要实验用 32 samples 和 Pass@32，分别比较有无 discovery agent 的配置。
4. 由两名具 Lean 经验的专家独立重标 MiniF2F 与 FIMO，保留原题语义、统一 formalization 风格，修复弱化目标等错误并将 FIMO 移植到 Lean 4；在新 Hard 数据与 PutnamBench、CombiBench 上联合评估。