---
title: "An In-Context Learning Agent for Formal Theorem-Proving (2023)"
description: "This paper presents COPRA, an agent that instead relies only on in-context learning. 43 references, cited by 43 papers here."
authors: ["Amitayush Thakur", "George Tsoukalas", "Yeming Wen", "Jimmy Xin", "Swarat Chaudhuri"]
year: 2023
venue: "arXiv:2310.04353"
source: "https://arxiv.org/abs/2310.04353"
doi: "10.48550/arxiv.2310.04353"
arxiv: "2310.04353"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2023](https://md.research.elamur.ai/free/en/papers/2023/page/11/) / An In-Context Learning Agent for Formal Theorem-Proving

# An In-Context Learning Agent for Formal Theorem-Proving

**Authors:** [Amitayush Thakur](https://md.research.elamur.ai/free/en/authors/amitayush-thakur/), [George Tsoukalas](https://md.research.elamur.ai/free/en/authors/george-tsoukalas/), [Yeming Wen](https://md.research.elamur.ai/free/en/authors/yeming-wen/), [Jimmy Xin](https://md.research.elamur.ai/free/en/authors/jimmy-xin/) and [Swarat Chaudhuri](https://md.research.elamur.ai/free/en/authors/swarat-chaudhuri/) · **Year:** 2023 · **Venue:** arXiv:2310.04353 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

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

**Citations:** 4 citations (OpenAlex, 2026-10-14) · [43](https://md.research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Formal proof assistants such as Lean and Coq require proofs written as sequences of tactics. The strongest neural provers have so far been trained or finetuned on proof data from one specific system. This paper presents COPRA, an agent that instead relies only on in-context learning. A general-purpose black-box model, GPT-4-turbo, is queried repeatedly inside a depth-first search that can backtrack. Each suggested tactic is executed in the proof assistant. The next prompt then combines the resulting error messages, tactics already known to fail at that state, the search history and lemmas fetched from an external database. A symbolic progress check, adopted from Proverbot9001, rejects steps that do not make the proof easier, which also rules out cycles.

COPRA was evaluated on miniF2F (Lean) and on Coq tasks drawn from CompCert. It clearly beats few-shot GPT-4 prompting and outperforms the finetuned ReProver on pass@1. It also finds proofs with fewer model queries than ReProver and Proverbot9001. The work suggests that a strong general LLM, combined with environment feedback, can rival system-specific training and carries over easily between proof systems.

## Key points
- COPRA, short for "In-context Prover Agent", is described by the authors as the first open-source theorem prover that works with both Lean and Coq.
- The search keeps two structures: a stack of proof states and a "Bad" dictionary that records unproductive tactics for each state. Both are serialized into the prompt, along with retrieved lemmas and optional natural-language hints.
- The benchmarks are miniF2F (competition mathematics in Lean) and CompCert-based Coq tasks. The baselines are few-shot GPT-4, ReProver, Proverbot9001 and a GPT-3.5 variant of COPRA, which performed noticeably worse.
- For cost reasons, each problem was limited to at most 60 GPT-4 queries, and temperature was set to zero for reproducibility.
- Code and data are available at https://github.com/trishullab/copra; running it requires the user's own OpenAI API keys.

*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

- [The University of Texas at Austin](https://md.research.elamur.ai/free/en/universities/the-university-of-texas-at-austin/) — University, Austin, United States · 126 works · 58,144 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

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin and Swarat Chaudhuri. 2023. An In-Context Learning Agent for Formal Theorem-Proving. arXiv:2310.04353.

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

```bibtex
@misc{thakur2023context,
  title = {{An In-Context Learning Agent for Formal Theorem-Proving}},
  author = {Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin and Swarat Chaudhuri},
  year = {2023},
  doi = {10.48550/arxiv.2310.04353},
  eprint = {2310.04353},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2310.04353}
}
```

- [← previous Resolving Knowledge Conflicts in Large Language Models](https://md.research.elamur.ai/free/en/papers/wang-2023-resolving-knowledge-conflicts-large-language/)
- [next → Counting the Bugs in ChatGPT's Wugs: A Multilingual Investigation into the Morphological Capabilities of a Large Language Model](https://md.research.elamur.ai/free/en/papers/weissweiler-2023-chatgpt-wugs-morphology/)
- [↑ back to papers of 2023](https://md.research.elamur.ai/free/en/papers/2023/page/11/)

## References

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

1. Andrews, P. B. and Brown, C. E. Tps: A hybrid automatic-interactive system for developing proofs. Journal of Applied Logic, 4(4):367–395, 2006. [find](https://scholar.google.com/scholar?q=Andrews%2C+P%2E+B%2E+and+Brown%2C+C%2E+E%2E+Tps%3A+A+hybrid+automatic%2Dinteractive+system+for+developing+proofs%2E+Journal+of+Applied+Logic%2C+4%284%29%3A367%E2%80%93395%2C+2006%2E)
2. Azerbayev, Z., Schoelkopf, H., Paster, K., Santos, M. D., McAleer, S., Jiang, A. Q., Deng, J., Biderman, S., and Welleck, S. [Llemma: An open language model for mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-llemma-open-language-model-mathematics/), 2023.
3. Blanchette, J. C., Bulwahn, L., and Nipkow, T. Automatic proof and disproof in isabelle/hol. In Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings 8, pp. 12–27. [find](https://scholar.google.com/scholar?q=Blanchette%2C+J%2E+C%2E%2C+Bulwahn%2C+L%2E%2C+and+Nipkow%2C+T%2E+Automatic+proof+and+disproof+in+isabelle%2Fhol%2E+In+Frontiers+of+Combining+Systems%3A+8th+International+Symposium%2C+FroCoS+2011%2C+Saarbru%CC%88cken%2C+Germany%2C+October)
4. Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J. D., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al. [Language models are few-shot learners](https://md.research.elamur.ai/free/en/papers/brown-2020-language-models-few-shot-learners/). Advances in neural information processing systems, 33:1877–1901, 2020.
5. Bundy, A. The use of explicit plans to guide inductive proofs. In 9th International Conference on Automated Deduction: Argonne, Illinois, USA, May 23–26, 1988 Proceedings 9, pp. 111–120. [find](https://scholar.google.com/scholar?q=Bundy%2C+A%2E+The+use+of+explicit+plans+to+guide+inductive+proofs%2E+In+9th+International+Conference+on+Automated+Deduction%3A+Argonne%2C+Illinois%2C+USA%2C+May+23%E2%80%9326%2C+1988+Proceedings+9%2C+pp%2E+111%E2%80%93120%2E)
6. De Moura, L. and Bjørner, N. Z3: an efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pp. 337–340, Berlin, Heidelberg, 2008. Springer-Verlag. ISBN 3540787… [find](https://scholar.google.com/scholar?q=De+Moura%2C+L%2E+and+Bj%C3%B8rner%2C+N%2E+Z3%3A+an+efficient+smt+solver%2E+In+Proceedings+of+the+Theory+and+Practice+of+Software%2C+14th+International+Conference+on+Tools+and+Algorithms+for+the+Construction+and+Analysis)
7. First, E., Rabe, M. N., Ringer, T., and Brun, Y. [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/). arXiv preprint arXiv:2303.04910, 2023.
8. Han, J. M., Rute, J., Wu, Y., Ayers, E. W., and Polu, S. [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/). arXiv preprint arXiv:2102.06203, 2021.
9. Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., and Steinhardt, J. [Measuring mathematical problem solving with the math dataset](https://md.research.elamur.ai/free/en/papers/hendrycks-2021-measuring-mathematical-problem-solving-math/). 2021.
10. Huang, D., Dhariwal, P., Song, D., and Sutskever, I. [Gamepad: A learning environment for theorem proving](https://md.research.elamur.ai/free/en/papers/huang-2018-gamepad-learning-environment-theorem-proving/). In ICLR, 2019.
11. Huet, G., Kahn, G., and Paulin-Mohring, C. The coq proof assistant a tutorial. Rapport Technique, 178, 1997. [find](https://scholar.google.com/scholar?q=Huet%2C+G%2E%2C+Kahn%2C+G%2E%2C+and+Paulin%2DMohring%2C+C%2E+The+coq+proof+assistant+a+tutorial%2E+Rapport+Technique%2C+178%2C+1997%2E)
12. Jiang, A. Q., Li, W., Han, J. M., and Wu, Y. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pp. 378–392, 2021. [find](https://scholar.google.com/scholar?q=Jiang%2C+A%2E+Q%2E%2C+Li%2C+W%2E%2C+Han%2C+J%2E+M%2E%2C+and+Wu%2C+Y%2E+Lisa%3A+Language+models+of+isabelle+proofs%2E+In+6th+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+pp%2E+378%E2%80%93392%2C+2021%2E)
13. Jiang, A. Q., Li, W., Tworkowski, S., Czechowski, K., Odrzygóźdź, T., Miłoś, P., Wu, Y., and Jamnik, M. [Thor: Wielding hammers to integrate language models and automated theorem provers](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/). Advances in Neural Information Processing Systems, 35:8360–8373, 2022a.
14. Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., and Lample, G. [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/). arXiv preprint arXiv:2210.12283, 2022b.
15. Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). Advances in Neural Information Processing Systems, 35:26337–26349, 2022.
16. Leroy, X. Formal verification of a realistic compiler. Communications of the ACM, 52(7): 107–115, 2009. mathlib Community, T. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. [find](https://scholar.google.com/scholar?q=Leroy%2C+X%2E+Formal+verification+of+a+realistic+compiler%2E+Communications+of+the+ACM%2C+52%287%29%3A+107%E2%80%93115%2C+2009%2E+mathlib+Community%2C+T%2E+The+lean+mathematical+library%2E+In+Proceedings+of+the+9th+ACM+SIGPLAN+Inter)
17. ACM, January 2020. [doi: 10.1145/3372885.3373824](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/). URL http://dx.doi.org/10.1145/3372885.3373824. [↗](http://dx.doi.org/10.1145/3372885.3373824)
18. Newell, A., Shaw, J. C., and Simon, H. A. Empirical explorations of the logic theory machine: a case study in heuristic. In Papers presented at the February 26-28, 1957, western joint computer conference: Techniques for reliability, pp. 218–230, 1957. [find](https://scholar.google.com/scholar?q=Newell%2C+A%2E%2C+Shaw%2C+J%2E+C%2E%2C+and+Simon%2C+H%2E+A%2E+Empirical+explorations+of+the+logic+theory+machine%3A+a+case+study+in+heuristic%2E+In+Papers+presented+at+the+February+26%2D28%2C+1957%2C+western+joint+computer+confere)
19. OpenAI. [GPT-4 technical report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/), 2023a.
20. OpenAI. GPT-4 and GPT-4 turbo, 2023b. URL [https://platform.openai.com/docs/models/gpt-4-and-gpt-4-turbo](https://platform.openai.com/docs/models/gpt-4-and-gpt-4-turbo). [↗](https://platform.openai.com/docs/models/gpt-4-and-gpt-4-turbo)
21. Paulson, L. and Blanchette, J. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. 02 2015. doi: 10.29007/tnfd. [find](https://scholar.google.com/scholar?q=Paulson%2C+L%2E+and+Blanchette%2C+J%2E+Three+years+of+experience+with+sledgehammer%2C+a+practical+link+between+automatic+and+interactive+theorem+provers%2E+02+2015%2E+doi%3A+10%2E29007%2Ftnfd%2E)
22. Paulson, L. C. Isabelle: A generic theorem prover. Springer, 1994. [find](https://scholar.google.com/scholar?q=Paulson%2C+L%2E+C%2E+Isabelle%3A+A+generic+theorem+prover%2E+Springer%2C+1994%2E)
23. Polu, S. and Sutskever, I. [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). arXiv preprint arXiv:2009.03393, 2020.
24. Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., and Sutskever, I. [Formal mathematics statement curriculum learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). arXiv preprint arXiv:2202.01344, 2022.
25. Ramesh, A., Pavlov, M., Goh, G., Gray, S., Voss, C., Radford, A., Chen, M., and Sutskever, I. [Zero-shot text-to-image generation](https://md.research.elamur.ai/free/en/papers/ramesh-2021-zero-shot-text-image-generation/). In International Conference on Machine Learning, pp. 8821–8831. PMLR, 2021.
26. Roziere, B., Gehring, J., Gloeckle, F., Sootla, S., Gat, I., Tan, X. E., Adi, Y., Liu, J., Remez, T., Rapin, J., et al. [Code llama: Open foundation models for code](https://md.research.elamur.ai/free/en/papers/roziere-2024-code-llama-open-foundation-models/). arXiv preprint arXiv:2308.12950, 2023.
27. Sanchez-Stern, A., Alhessi, Y., Saul, L., and Lerner, S. [Generating correctness proofs with neural networks](https://md.research.elamur.ai/free/en/papers/stern-2019-generating-correctness-proofs-neural-networks/). In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, pp. 1–10, 2020.
28. Schick, T., Dwivedi-Yu, J., Dessı̀, R., Raileanu, R., Lomeli, M., Zettlemoyer, L., Cancedda, N., and Scialom, T. [Toolformer: Language models can teach themselves to use tools](https://md.research.elamur.ai/free/en/papers/schick-2023-toolformer-language-models-can-teach/). arXiv preprint arXiv:2302.04761, 2023.
29. Schulz, S. E - a brainiac theorem prover. AI Commun., 15(2,3):111–126, aug 2002. ISSN 0921-7126. [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E+E+%2D+a+brainiac+theorem+prover%2E+AI+Commun%2E%2C+15%282%2C3%29%3A111%E2%80%93126%2C+aug+2002%2E+ISSN+0921%2D7126%2E)
30. Shinn, N., Cassano, F., Labash, B., Gopinath, A., Narasimhan, K., and Yao, S. [Reflexion: Language agents with verbal reinforcement learning](https://md.research.elamur.ai/free/en/papers/shinn-2023-reflexion-language-agents-verbal-reinforcement/). arXiv preprint arXiv:2303.11366, 2023.
31. Significant-Gravitas. Autogpt. [https://github.com/Significant-Gravitas/Auto-GPT](https://github.com/Significant-Gravitas/Auto-GPT), 2023. [↗](https://github.com/Significant-Gravitas/Auto-GPT)
32. Touvron, H., Lavril, T., Izacard, G., Martinet, X., Lachaux, M.-A., Lacroix, T., Rozière, B., Goyal, N., Hambro, E., Azhar, F., et al. [Llama: Open and efficient foundation language models](https://md.research.elamur.ai/free/en/papers/touvron-2023-llama-open-efficient-foundation-language/). arXiv preprint arXiv:2302.13971, 2023.
33. Trinh, T. H., Wu, Y., Le, Q. V., He, H., and Luong, T. [Solving olympiad geometry without human demonstrations](https://md.research.elamur.ai/free/en/papers/trinh-2024-solving-olympiad-geometry-without-human/). Nature, 625(7995):476–482, 2024.
34. Wang, G., Xie, Y., Jiang, Y., Mandlekar, A., Xiao, C., Zhu, Y., Fan, L., and Anandkumar, A. Voyager: An open-ended embodied agent with large language models. arXiv preprint arXiv:2305.16291, 2023a. [find](https://scholar.google.com/scholar?q=Wang%2C+G%2E%2C+Xie%2C+Y%2E%2C+Jiang%2C+Y%2E%2C+Mandlekar%2C+A%2E%2C+Xiao%2C+C%2E%2C+Zhu%2C+Y%2E%2C+Fan%2C+L%2E%2C+and+Anandkumar%2C+A%2E+Voyager%3A+An+open%2Dended+embodied+agent+with+large+language+models%2E+arXiv+preprint+arXiv%3A2305%2E16291%2C+2023a%2E)
35. Wang, H., Xin, H., Zheng, C., Li, L., Liu, Z., Cao, Q., Huang, Y., Xiong, J., Shi, H., Xie, E., Yin, J., Li, Z., Liao, H., and Liang, X. [Lego-prover: Neural theorem proving with growing libraries](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/). 2023b.
36. Wei, J., Wang, X., Schuurmans, D., Bosma, M., Xia, F., Chi, E., Le, Q. V., Zhou, D., et al. [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/). Advances in Neural Information Processing Systems, 35:24824–24837, 2022.
37. Yang, K. and Deng, J. [Learning to prove theorems via interacting with proof assistants](https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/). In International Conference on Machine Learning, pp. 6984–6994. PMLR, 2019.
38. Yang, K., Swope, A. M., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A. [Leandojo: Theorem proving with retrieval-augmented language models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). arXiv preprint arXiv:2306.15626, 2023.
39. Yao, S., Zhao, J., Yu, D., Du, N., Shafran, I., Narasimhan, K., and Cao, Y. [React: Synergizing reasoning and acting in language models](https://md.research.elamur.ai/free/en/papers/yao-2022-react-synergizing-reasoning-acting-language/). arXiv preprint arXiv:2210.03629, 2022.
40. Yao, S., Yu, D., Zhao, J., Shafran, I., Griffiths, T. L., Cao, Y., and Narasimhan, K. Tree of thoughts: Deliberate problem solving with large language models. arXiv preprint arXiv:2305.10601, 2023. [find](https://scholar.google.com/scholar?q=Yao%2C+S%2E%2C+Yu%2C+D%2E%2C+Zhao%2C+J%2E%2C+Shafran%2C+I%2E%2C+Griffiths%2C+T%2E+L%2E%2C+Cao%2C+Y%2E%2C+and+Narasimhan%2C+K%2E+Tree+of+thoughts%3A+Deliberate+problem+solving+with+large+language+models%2E+arXiv+preprint+arXiv%3A2305%2E10601%2C+2023%2E)
41. Zhao, X., Li, W., and Kong, L. [Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving](https://md.research.elamur.ai/free/en/papers/zhao-2023-decomposing-enigma-subgoal-based-demonstration/). 2023.
42. Zheng, C., Wang, H., Xie, E., Liu, Z., Sun, J., Xin, H., Shen, J., Li, Z., and Li, Y. [Lyra: Orchestrating dual correction in automated theorem proving](https://md.research.elamur.ai/free/en/papers/zheng-2023-lyra-orchestrating-dual-correction-automated/). arXiv preprint arXiv:2309.15806, 2023.
43. Zheng, K., Han, J. M., and Polu, S. [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/). arXiv preprint arXiv:2109.00110, 2021.

*Updated 3 November 2026*