Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917415940521984 |
|---|---|
| author | Liu, Chengwu Yin, Yichun Yuan, Ye Xie, Jiaxuan Li, Botao Li, Siqi Shen, Jianhao Xu, Yan Shang, Lifeng Zhang, Ming |
| author_facet | Liu, Chengwu Yin, Yichun Yuan, Ye Xie, Jiaxuan Li, Botao Li, Siqi Shen, Jianhao Xu, Yan Shang, Lifeng Zhang, Ming |
| contents | Most ATP benchmarks embed the final answer within the formal statement -- a convention we call "Easy Mode" -- a design that simplifies the task relative to what human competitors face and may lead to optimistic estimates of model capability. We call the stricter, more realistic setting "Hard Mode": the system must independently discover the answer before constructing a formal proof. To enable Hard Mode research, we make two contributions. First, we release MiniF2F-Hard and FIMO-Hard, expert-reannotated Hard Mode variants of two widely-used ATP benchmarks. Second, we introduce Discover And Prove (DAP), an agentic framework that uses LLM natural-language reasoning with explicit self-reflection to discover answers, then rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. DAP sets the state of the art: on CombiBench it raises solved problems from 7 (previous SOTA, Pass@16) to 10; on PutnamBench it is the first system to formally prove 36 theorems in Hard Mode -- while simultaneously revealing that state-of-the-art LLMs exceed 80% answer accuracy on the same problems where formal provers manage under 10%, exposing a substantial gap that Hard Mode benchmarks are uniquely suited to measure. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_15839 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4 Liu, Chengwu Yin, Yichun Yuan, Ye Xie, Jiaxuan Li, Botao Li, Siqi Shen, Jianhao Xu, Yan Shang, Lifeng Zhang, Ming Artificial Intelligence Computation and Language Logic in Computer Science Most ATP benchmarks embed the final answer within the formal statement -- a convention we call "Easy Mode" -- a design that simplifies the task relative to what human competitors face and may lead to optimistic estimates of model capability. We call the stricter, more realistic setting "Hard Mode": the system must independently discover the answer before constructing a formal proof. To enable Hard Mode research, we make two contributions. First, we release MiniF2F-Hard and FIMO-Hard, expert-reannotated Hard Mode variants of two widely-used ATP benchmarks. Second, we introduce Discover And Prove (DAP), an agentic framework that uses LLM natural-language reasoning with explicit self-reflection to discover answers, then rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. DAP sets the state of the art: on CombiBench it raises solved problems from 7 (previous SOTA, Pass@16) to 10; on PutnamBench it is the first system to formally prove 36 theorems in Hard Mode -- while simultaneously revealing that state-of-the-art LLMs exceed 80% answer accuracy on the same problems where formal provers manage under 10%, exposing a substantial gap that Hard Mode benchmarks are uniquely suited to measure. |
| title | Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4 |
| topic | Artificial Intelligence Computation and Language Logic in Computer Science |
| url | https://arxiv.org/abs/2604.15839 |