---
title: "ImProver: Agent-Based Automated Proof Optimization (2024)"
description: "The authors define a new task, automated proof optimization. 28 references, cited by 5 papers here."
authors: ["Riyaz Ahuja", "Jeremy Avigad", "Prasad Tetali", "Sean Welleck"]
year: 2024
venue: "arXiv:2410.04753"
source: "https://arxiv.org/abs/2410.04753"
doi: "10.48550/arxiv.2410.04753"
arxiv: "2410.04753"
licence: "CC BY-NC-SA 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by-nc-sa/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/ahuja-2024-improver-agent-based-automated-proof/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/ahuja-2024-improver-agent-based-automated-proof/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/15/) / ImProver: Agent-Based Automated Proof Optimization

# ImProver: Agent-Based Automated Proof Optimization

**Authors:** Riyaz Ahuja, [Jeremy Avigad](https://md.research.elamur.ai/free/en/authors/jeremy-avigad/), Prasad Tetali and [Sean Welleck](https://md.research.elamur.ai/free/en/authors/sean-welleck/) · **Year:** 2024 · **Venue:** arXiv:2410.04753 · **Licence:** [CC BY-NC-SA 4.0 (arXiv)](https://creativecommons.org/licenses/by-nc-sa/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2410.04753) · [PDF](https://arxiv.org/pdf/2410.04753v2) · [DOI 10.48550/arxiv.2410.04753](https://doi.org/10.48550/arxiv.2410.04753) · [arXiv 2410.04753](https://arxiv.org/abs/2410.04753) · [OpenAlex](https://openalex.org/W4403322869)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [5](https://md.research.elamur.ai/free/en/papers/ahuja-2024-improver-agent-based-automated-proof/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
A Lean proof that compiles may still fall short: it can be verbose, hard to follow, or badly structured for library style rules or for use as machine-learning training data. The authors define a new task, automated proof optimization. Given a theorem, its context and an existing proof, the goal is a new proof that Lean still accepts and that scores better on a chosen metric. Their system, ImProver, is an agent built around a black-box LLM such as GPT-4. Plain prompting often yields broken or barely improved proofs, so ImProver adds several components. The main one is Chain-of-States prompting, which uses Lean metaprogramming to extract the goals and hypotheses at each step and inserts them as comments before every tactic. The agent also uses file context, error correction and retrieval. Tested on undergraduate exercises, competition solutions and research-level Mathlib theorems, ImProver produced considerably shorter and more declarative proofs and could also write proofs from scratch. This is useful for maintaining formal libraries, for teaching, and for creating better-structured training data for neural provers.

## Key points
- Four metrics are defined. **Length** counts tactic invocations. **Declarativity** is the share of explicitly typed `have` steps among all tactics. **Mixed** scores −1 per tactic and +5 per declarative tactic. **Completion** counts errors, which turns optimization into ordinary theorem proving.
- Chain-of-States is presented as a counterpart to chain-of-thought. It builds proof states from Lean's elaboration data (`Lean.Elab.InfoTree`) rather than asking the model to infer them.
- Test material includes Mathematics in Lean (MIL), Compfiles competition solutions (for example IMO 2022 Question 2), Mathlib and MiniF2F.
- In one example, a Mathlib theorem from `FundamentalGroupoid/InducedMaps` shrinks from 3 tactic invocations to 1. In others, an MIL group-theory exercise and MiniF2F `mathd_numbertheory_345` are proved starting from `sorry`.
- The authors warn about degenerate solutions, such as adding unused `have` steps to inflate the declarativity score. They counter this with human-written examples in the prompts. Code is available at github.com/riyazahuja/ImProver.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Carnegie Mellon University](https://md.research.elamur.ai/free/en/universities/carnegie-mellon-university/) — University, Pittsburgh, United States · 633 works · 195,217 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

## Cite

Cite as: Riyaz Ahuja, Jeremy Avigad, Prasad Tetali and Sean Welleck. 2024. ImProver: Agent-Based Automated Proof Optimization. arXiv:2410.04753.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{ahuja2024improver,
  title = {{ImProver: Agent-Based Automated Proof Optimization}},
  author = {Riyaz Ahuja, Jeremy Avigad, Prasad Tetali and Sean Welleck},
  year = {2024},
  doi = {10.48550/arxiv.2410.04753},
  eprint = {2410.04753},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2410.04753}
}
```

- [← previous HATFormer: Historic Handwritten Arabic Text Recognition with Transformers](https://md.research.elamur.ai/free/en/papers/chan-2024-hatformer-historic-handwritten-arabic-text/)
- [next → Improving Arabic Multi-Label Emotion Classification using Stacked Embeddings and Hybrid Loss Function](https://md.research.elamur.ai/free/en/papers/aslam-2024-improving-arabic-multi-label-emotion/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/15/)

## References

28 references, 17 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, and Sean Welleck. [Improver: Agent-based automated proof optimization](https://md.research.elamur.ai/free/en/papers/ahuja-2024-improver-agent-based-automated-proof/). In Y. Yue, A. Garg, N. Peng, F. Sha, and R. Yu (eds.), International Conference on Representation Learning, volume 2025, pp. 29521–29543, 2025. URL [https://proceedings.iclr.cc/paper_files…](https://proceedings.iclr.cc/paper_files…) [↗](https://proceedings.iclr.cc/paper_files…)
2. AlphaProof and AlphaGeometry Teams. AI achieves silver-medal standard solving international mathematical olympiad problems. [https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/), 2024. [↗](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/)
3. Cem Anil, Guodong Zhang, Yuhuai Wu, and Roger Grosse. Learning to give checkable answers with prover-verifier games, 2021. URL https://arxiv.org/abs/2108.12099. — [arXiv:2108.12099](https://arxiv.org/abs/2108.12099) [↗](https://arxiv.org/abs/2108.12099)
4. Serge Autexier and Dominik Dietrich. A tactic language for declarative proofs. In Matt Kaufmann and Lawrence C. Paulson (eds.), Interactive Theorem Proving, pp. 99–114, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. [find](https://scholar.google.com/scholar?q=Serge+Autexier+and+Dominik+Dietrich%2E+A+tactic+language+for+declarative+proofs%2E+In+Matt+Kaufmann+and+Lawrence+C%2E+Paulson+%28eds%2E%29%2C+Interactive+Theorem+Proving%2C+pp%2E+99%E2%80%93114%2C+Berlin%2C+Heidelberg%2C+2010%2E+Sprin)
5. Jaime Carbonell and Jade Goldstein. The use of mmr, diversity-based reranking for reordering documents and producing summaries. In Proceedings of the 21st Annual International ACM SIGIR Conference on Research and Development in Information Retrieval, SIGIR ’98, pp. 335–336, New York, NY, USA, 1998.… [find](https://scholar.google.com/scholar?q=Jaime+Carbonell+and+Jade+Goldstein%2E+The+use+of+mmr%2C+diversity%2Dbased+reranking+for+reordering+documents+and+producing+summaries%2E+In+Proceedings+of+the+21st+Annual+International+ACM+SIGIR+Conference+on+)
6. Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. Teaching large language models to self-debug, 2023. URL https://arxiv.org/abs/2304.05128. [↗](https://arxiv.org/abs/2304.05128)
7. David Renshaw. compfiles. [https://github.com/dwrensha/compfiles](https://github.com/dwrensha/compfiles), 2024. [↗](https://github.com/dwrensha/compfiles)
8. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, [Proceedings, pp](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/). 625–635, Berlin, Heidelberg, 2021. Springer-Verlag. ISBN 978-3-030-79…
9. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. [Baldur: Whole-proof generation and repair with large language models](https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/), 2023.
10. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. [Proof artifact co-training for theorem proving with language models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/). In International Conference on Learning Representations, 2022. URL [https://openreview.net/forum?id=rpxJc9j04U](https://openreview.net/forum?id=rpxJc9j04U). [↗](https://openreview.net/forum?id=rpxJc9j04U)
11. Jiewen Hu, Thomas Zhu, and Sean Welleck. [minictx: Neural theorem proving with (long-)contexts](https://md.research.elamur.ai/free/en/papers/hu-2024-minictx-neural-theorem-proving-long/), 2024. URL https://arxiv.org/abs/2408.03350. [↗](https://arxiv.org/abs/2408.03350)
12. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. [Draft, sketch, and prove: Guiding formal theorem provers with informal proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). In The Eleventh International Conference on Learning Representations, 2023. URL…
13. Kim Morrison. lean-training-data. lean-training-data, 2024. [https://github.com/kim-em/](https://github.com/kim-em/) [↗](https://github.com/kim-em/)
14. Guillaume Lample, Timothee Lacroix, Marie anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information…
15. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. [A survey on deep learning for theorem proving](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/), 2024.
16. Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang. A survey of deep learning for mathematical reasoning. In Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (eds.), Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 146… [find](https://scholar.google.com/scholar?q=Pan+Lu%2C+Liang+Qiu%2C+Wenhao+Yu%2C+Sean+Welleck%2C+and+Kai%2DWei+Chang%2E+A+survey+of+deep+learning+for+mathematical+reasoning%2E+In+Anna+Rogers%2C+Jordan+Boyd%2DGraber%2C+and+Naoaki+Okazaki+%28eds%2E%29%2C+Proceedings+of+the+6)
17. Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. Self-refine: Iterative refinement with self-… [find](https://scholar.google.com/scholar?q=Aman+Madaan%2C+Niket+Tandon%2C+Prakhar+Gupta%2C+Skyler+Hallinan%2C+Luyu+Gao%2C+Sarah+Wiegreffe%2C+Uri+Alon%2C+Nouha+Dziri%2C+Shrimai+Prabhumoye%2C+Yiming+Yang%2C+Shashank+Gupta%2C+Bodhisattwa+Prasad+Majumder%2C+Katherine+Her)
18. The mathlib Community. [The lean mathematical library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/). In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, January 2020. doi: 10.1145/3372885.3373824. URL http://dx.doi.org/10.1145/3372885.3373824. [↗](http://dx.doi.org/10.1145/3372885.3373824)
19. OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, Jeff Belgum, Irwan Bello, Ja… — [GPT-4 Technical Report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/)
20. Stanislas Polu and Ilya Sutskever. [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/), 2020.
21. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. [Formal mathematics statement curriculum learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). CoRR, abs/2202.01344, 2022a. URL https://arxiv.org/abs/2202.01344. [↗](https://arxiv.org/abs/2202.01344)
22. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. [Formal mathematics statement curriculum learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/), 2022b.
23. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. [An in-context learning agent for formal theorem-proving](https://md.research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/), 2024.
24. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed H. Chi, Quoc V Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Proce… — [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://md.research.elamur.ai/free/en/papers/wei-2022-chain-thought-prompting-elicits-reasoning/)
25. Freek Wiedijk. Formal proof sketches. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani (eds.), Types for Proofs and Programs, pp. 378–393, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. ISBN 978-3-540-24849-1. [find](https://scholar.google.com/scholar?q=Freek+Wiedijk%2E+Formal+proof+sketches%2E+In+Stefano+Berardi%2C+Mario+Coppo%2C+and+Ferruccio+Damiani+%28eds%2E%29%2C+Types+for+Proofs+and+Programs%2C+pp%2E+378%E2%80%93393%2C+Berlin%2C+Heidelberg%2C+2004%2E+Springer+Berlin+Heidelberg%2E+I)
26. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. [LeanDojo: Theorem proving with retrieval-augmented language models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). In Neural Information Processing Systems (NeurIPS), 2023.
27. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [minif2f: a cross-system benchmark for formal olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). In International Conference on Learning Representations, 2022. URL [https://openreview.net/forum?id=9ZPegFuFTFv](https://openreview.net/forum?id=9ZPegFuFTFv). [↗](https://openreview.net/forum?id=9ZPegFuFTFv)
28. Shuyan Zhou, Uri Alon, Frank F. Xu, Zhengbao Jiang, and Graham Neubig. Docprompting: Generating code by retrieving the docs. In The Eleventh International Conference on Learning Representations, 2023. URL [https://openreview.net/forum?id=ZTCxT2t2Ru](https://openreview.net/forum?id=ZTCxT2t2Ru). [↗](https://openreview.net/forum?id=ZTCxT2t2Ru)

*Updated 3 November 2026*