Discover and Prove 提出 Hard Mode：要求模型先独立发现答案，再用 Lean 完成形式证明

Discover and Prove 指出许多 ATP benchmark 把最终答案编码进 formal statement，导致任务比人类实际面对的问题更简单。作者发布 MiniF2F-Hard 与 FIMO-Hard，并提出 DAP：先由 reasoning LLM 在自然语言中发现答案、自检与修正，再把 Hard Mode statement 重写成 Easy Mode 交给既有 prover。论文报告 DAP 在 PutnamBench Hard Mode 上首次形式证明 36 个 theorem，同时显示同一问题上 LLM answer accuracy 可超过 80%，而 formal proving success 仍低于 10%。