---
title: "Autoformalizing Euclidean Geometry — Murphy 2024"
description: "They build an SMT-based symbolic reasoning engine, E3, with two uses: Grading theorem statements. 47 references, cited by 23 papers here."
authors: ["Logan Murphy", "Kaiyu Yang", "Jialiang Sun", "Zhaoyu Li", "Anima Anandkumar", "Xujie Si"]
year: 2024
venue: "arXiv:2405.17216"
source: "https://arxiv.org/abs/2405.17216"
doi: "10.48550/arxiv.2405.17216"
arxiv: "2405.17216"
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/murphy-2024-autoformalizing-euclidean-geometry/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/murphy-2024-autoformalizing-euclidean-geometry/)

[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/11/) / Autoformalizing Euclidean Geometry

# Autoformalizing Euclidean Geometry

**Authors:** [Logan Murphy](https://md.research.elamur.ai/free/en/authors/logan-murphy/), [Kaiyu Yang](https://md.research.elamur.ai/free/en/authors/kaiyu-yang/), [Jialiang Sun](https://md.research.elamur.ai/free/en/authors/jialiang-sun/), [Zhaoyu Li](https://md.research.elamur.ai/free/en/authors/zhaoyu-li/), [Anima Anandkumar](https://md.research.elamur.ai/free/en/authors/anima-anandkumar/) and [Xujie Si](https://md.research.elamur.ai/free/en/authors/xujie-si/) · **Year:** 2024 · **Venue:** arXiv:2405.17216 · **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/2405.17216) · [PDF](https://arxiv.org/pdf/2405.17216v1) · [DOI 10.48550/arxiv.2405.17216](https://doi.org/10.48550/arxiv.2405.17216) · [arXiv 2405.17216](https://arxiv.org/abs/2405.17216) · [OpenAlex](https://openalex.org/W4399144145)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [23](https://md.research.elamur.ai/free/en/papers/murphy-2024-autoformalizing-euclidean-geometry/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The paper addresses autoformalization, which means converting human-written mathematics into statements and proofs that a machine can check. The authors focus on Euclidean geometry. They argue it is a controllable test domain because two problems that are usually hard become manageable there: checking whether outputs are correct, and dealing with the steps that informal proofs leave to the diagram.

They build an SMT-based symbolic reasoning engine, E3, with two uses:
- **Grading theorem statements.** It tries to prove that a model's theorem is logically equivalent to a reference formalization. This replaces weak proxies such as BLEU and costly manual review.
- **Filling diagram gaps.** Inside Lean, it automatically supplies the facts a reader would normally read off the figure. The authors implement the formal system E (Avigad et al.) for this purpose, so a model only has to translate the explicit textual steps.

They also release LeanEuclid, a hand-formalized benchmark built from Euclid's Elements (Book I) and UniGeo. Experiments with GPT-4 and GPT-4V show low success rates, which marks the task as challenging. Many failed proofs, however, need only small fixes. The work matters because it moves autoformalization evaluation from human inspection toward automatic checking.

## Key points
- **LeanEuclid benchmark:** 173 examples, each with an informal statement, proof and diagram plus a formal Lean version. It covers all 48 propositions of Elements Book I and problems from UniGeo, and is intended for testing only.
- **Theorem autoformalization (5-shot):** GPT-4 gets 18.9% of theorems right and GPT-4V gets 21.0%. E3's automatic equivalence check correlates well with human judgment and produces few false negatives.
- **Proof autoformalization:** whole proofs were generated in single queries, without search. Overall success was 18.8% for GPT-4 and 23.1% for GPT-4V. Among the 43 Elements proofs tested, both models fully succeeded only on Propositions 1 and 17.
- **Repair effort:** proofs that failed were manually fixed. The median Levenshtein similarity to the repaired versions was 61.7% for GPT-4 and 64.0% for GPT-4V. Typical fixes were simple, such as reordering tactic arguments or slightly strengthening a lemma.
- **Main limitation:** the dataset is too small for fine-tuning. The authors suggest translating existing corpora, such as AlphaGeometry's synthetic data, into their formalism.

*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

- [University of Toronto](https://md.research.elamur.ai/free/en/universities/university-of-toronto/) — University, Toronto, Canada · 121 works · 179,943 citations
- [California Institute of Technology](https://md.research.elamur.ai/free/en/universities/california-institute-of-technology/) — University, Pasadena, United States · 16 works · 1,291 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: Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar and Xujie Si. 2024. Autoformalizing Euclidean Geometry. arXiv:2405.17216.

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

```bibtex
@misc{murphy2024autoformalizing,
  title = {{Autoformalizing Euclidean Geometry}},
  author = {Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar and Xujie Si},
  year = {2024},
  doi = {10.48550/arxiv.2405.17216},
  eprint = {2405.17216},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2405.17216}
}
```

- [← previous AI-Assisted Generation of Difficult Math Questions](https://md.research.elamur.ai/free/en/papers/shah-2024-ai-assisted-generation-difficult-math/)
- [next → BOND: Aligning LLMs with Best-of-N Distillation](https://md.research.elamur.ai/free/en/papers/sessa-2024-bond-aligning-llms-best-n/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/11/)

## References

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

1. Agrawal, A., Gadgil, S., Goyal, N., Narayanan, A., and Tadipatri, A. [Towards a mathematics formalisation assistant using large language models](https://md.research.elamur.ai/free/en/papers/agrawal-2022-mathematics-formalisation-assistant-large-language/). arXiv preprint arXiv:2211.07524, 2022.
2. Avigad, J. Notes on ”A formal system for Euclid’s Elements”. [https://www.andrew.cmu.edu/user/avigad/Papers/euclid_notes.htm](https://www.andrew.cmu.edu/user/avigad/Papers/euclid_notes.htm). Avigad, J., Dean, E., and Mumma, J. A formal system for Euclid’s Elements. The Review of Symbolic Logic, 2009. [↗](https://www.andrew.cmu.edu/user/avigad/Papers/euclid_notes.htm)
3. Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E. W., Radev, D., and Avigad, J. [ProofNet: Autoformalizing and formally proving undergraduate-level mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). arXiv preprint arXiv:2302.12433, 2023.
4. Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. [find](https://scholar.google.com/scholar?q=Barras%2C+B%2E%2C+Boutin%2C+S%2E%2C+Cornes%2C+C%2E%2C+Courant%2C+J%2E%2C+Filliatre%2C+J%2E%2DC%2E%2C+Gimenez%2C+E%2E%2C+Herbelin%2C+H%2E%2C+Huet%2C+G%2E%2C+Munoz%2C+C%2E%2C+Murthy%2C+C%2E%2C+et+al%2E+The+Coq+proof+assistant+reference+manual%3A+Version+6%2E1%2E+PhD+thesis%2C)
5. Barrett, C. and Tinelli, C. Satisfiability modulo theories. 2018. [find](https://scholar.google.com/scholar?q=Barrett%2C+C%2E+and+Tinelli%2C+C%2E+Satisfiability+modulo+theories%2E+2018%2E)
6. Beeson, M., Narboux, J., and Wiedijk, F. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, 2019. [find](https://scholar.google.com/scholar?q=Beeson%2C+M%2E%2C+Narboux%2C+J%2E%2C+and+Wiedijk%2C+F%2E+Proof%2Dchecking+Euclid%2E+Annals+of+Mathematics+and+Artificial+Intelligence%2C+2019%2E)
7. Buchberger, B. Applications of gröbner bases in non-linear computational geometry. In Trends in Computer Algebra, 2005. [find](https://scholar.google.com/scholar?q=Buchberger%2C+B%2E+Applications+of+gro%CC%88bner+bases+in+non%2Dlinear+computational+geometry%2E+In+Trends+in+Computer+Algebra%2C+2005%2E)
8. Chen, J., Tang, J., Qin, J., Liang, X., Liu, L., Xing, E., and Lin, L. [GeoQA: A geometric question answering benchmark towards multimodal numerical reasoning](https://md.research.elamur.ai/free/en/papers/chen-2021-geoqa-geometric-question-answering-benchmark/). In Findings of the Association for Computational Linguistics: ACL, 2021a.
9. Chen, J., Li, T., Qin, J., Lu, P., Lin, L., Chen, C., and Liang, X. [UniGeo: Unifying geometry logical reasoning via reformulating mathematical expression](https://md.research.elamur.ai/free/en/papers/chen-2022-unigeo-unifying-geometry-logical-reasoning/). In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2022.
10. Chen, M., Tworek, J., Jun, H., Yuan, Q., Pinto, H. P. d. O., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., et al. [Evaluating large language models trained on code](https://md.research.elamur.ai/free/en/papers/chen-2021-evaluating-large-language-models-trained/). arXiv preprint arXiv:2107.03374, 2021b.
11. Chen, Y., Gandhi, R., Zhang, Y., and Fan, C. NL2TL: Transforming natural languages to temporal logics using large language models. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2023. [find](https://scholar.google.com/scholar?q=Chen%2C+Y%2E%2C+Gandhi%2C+R%2E%2C+Zhang%2C+Y%2E%2C+and+Fan%2C+C%2E+NL2TL%3A+Transforming+natural+languages+to+temporal+logics+using+large+language+models%2E+In+Conference+on+Empirical+Methods+in+Natural+Language+Processing+%28EM)
12. Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., and Trippel, C. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In International Conference on Computer Aided Verification (CAV), 2023. [find](https://scholar.google.com/scholar?q=Cosler%2C+M%2E%2C+Hahn%2C+C%2E%2C+Mendoza%2C+D%2E%2C+Schmitt%2C+F%2E%2C+and+Trippel%2C+C%2E+nl2spec%3A+Interactively+translating+unstructured+natural+language+to+temporal+logics+with+large+language+models%2E+In+International+Confere)
13. Cunningham, G., Bunescu, R. C., and Juedes, D. [Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs](https://md.research.elamur.ai/free/en/papers/cunningham-2022-autoformalization-mathematics-code-correctness-experiments/). arXiv preprint arXiv:2301.02195, 2023. de Moura, L. d. and Ullrich, S. The Lean 4 theorem prover and programming language. In International Conference on…
14. First, E., Rabe, M., 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/). In Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2023.
15. Gao, J., Pi, R., Zhang, J., Ye, J., Zhong, W., Wang, Y., Hong, L., Han, J., Xu, H., Li, Z., et al. [G-LLaVA: Solving geometric problem with multi-modal large language model](https://md.research.elamur.ai/free/en/papers/gao-2023-g-llava-solving-geometric-problem/). arXiv preprint arXiv:2312.11370, 2023.
16. Hales, T., Adams, M., Bauer, G., Dang, T. D., Harrison, J., Le Truong, H., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T. T., et al. [A formal proof of the Kepler conjecture](https://md.research.elamur.ai/free/en/papers/hales-2015-formal-proof-kepler-conjecture/). In Forum of Mathematics, Pi, volume 5, 2017.
17. Han, J. M., Rute, J., Wu, Y., Ayers, E., 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/). In International Conference on Learning Representations (ICLR), 2022.
18. Heiberg, J. L. Euclid’s Elements. 2007. URL [https://github.com/rfitzp/Elements](https://github.com/rfitzp/Elements). [↗](https://github.com/rfitzp/Elements)
19. Hernandez-Espiet, A. feat: synthetic geometry. [https://github.com/leanprover-community/](https://github.com/leanprover-community/) mathlib4/pull/7300, 2023. [↗](https://github.com/leanprover-community/)
20. Hilbert, D. Grundlagen der geometrie. Springer-Verlag, 2013. [find](https://scholar.google.com/scholar?q=Hilbert%2C+D%2E+Grundlagen+der+geometrie%2E+Springer%2DVerlag%2C+2013%2E)
21. Jiang, A., 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/). In International Conference on Learning Representations (ICLR), 2023a.
22. Jiang, A. Q., Li, W., and Jamnik, M. [Multilingual mathematical autoformalization](https://md.research.elamur.ai/free/en/papers/jiang-2023-multilingual-mathematical-autoformalization/). arXiv preprint arXiv:2311.03755, 2023b.
23. Kazemi, M., Alvari, H., Anand, A., Wu, J., Chen, X., and Soricut, R. GeomVerse: A systematic evaluation of large models for geometric reasoning. arXiv preprint arXiv:2312.12241, 2023. — [arXiv:2312.12241](https://arxiv.org/abs/2312.12241) [find](https://scholar.google.com/scholar?q=Kazemi%2C+M%2E%2C+Alvari%2C+H%2E%2C+Anand%2C+A%2E%2C+Wu%2C+J%2E%2C+Chen%2C+X%2E%2C+and+Soricut%2C+R%2E+GeomVerse%3A+A+systematic+evaluation+of+large+models+for+geometric+reasoning%2E+arXiv+preprint+arXiv%3A2312%2E12241%2C+2023%2E+%E2%80%94+%5BarXiv%3A2312%2E12)
24. Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., and Martinet, X. Hyper-Tree proof search for neural theorem proving. In Neural Information Processing Systems (NeurIPS), 2022. [find](https://scholar.google.com/scholar?q=Lample%2C+G%2E%2C+Lacroix%2C+T%2E%2C+Lachaux%2C+M%2E%2DA%2E%2C+Rodriguez%2C+A%2E%2C+Hayat%2C+A%2E%2C+Lavril%2C+T%2E%2C+Ebner%2C+G%2E%2C+and+Martinet%2C+X%2E+Hyper%2DTree+proof+search+for+neural+theorem+proving%2E+In+Neural+Information+Processing+Systems+)
25. Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., and Ferdinand, C. CompCert—a formally verified optimizing compiler. In Embedded Real Time Software and Systems, 2016. [find](https://scholar.google.com/scholar?q=Leroy%2C+X%2E%2C+Blazy%2C+S%2E%2C+Ka%CC%88stner%2C+D%2E%2C+Schommer%2C+B%2E%2C+Pister%2C+M%2E%2C+and+Ferdinand%2C+C%2E+CompCert%E2%80%94a+formally+verified+optimizing+compiler%2E+In+Embedded+Real+Time+Software+and+Systems%2C+2016%2E)
26. Li, Z., Sun, J., Murphy, L., Su, Q., Li, Z., Zhang, X., Yang, K., and Si, X. [A survey on deep learning for theorem proving](https://md.research.elamur.ai/free/en/papers/li-2024-survey-deep-learning-theorem-proving/). arXiv preprint arXiv:2404.09939, 2024.
27. Liang, Z., Yang, T., Zhang, J., and Zhang, X. UniMath: A foundational and multimodal mathematical reasoner. In Conference on Empirical Methods in Natural Language Processing (EMNLP), 2023. [find](https://scholar.google.com/scholar?q=Liang%2C+Z%2E%2C+Yang%2C+T%2E%2C+Zhang%2C+J%2E%2C+and+Zhang%2C+X%2E+UniMath%3A+A+foundational+and+multimodal+mathematical+reasoner%2E+In+Conference+on+Empirical+Methods+in+Natural+Language+Processing+%28EMNLP%29%2C+2023%2E)
28. Lu, P., Gong, R., Jiang, S., Qiu, L., Huang, S., Liang, X., and Zhu, S.-c. [Inter-GPS: Interpretable geometry problem solving with formal language and symbolic reasoning](https://md.research.elamur.ai/free/en/papers/lu-2021-inter-gps-interpretable-geometry-problem/). In Annual Meeting of the Association for Computational Linguistics (ACL), 2021.
29. Miller, N. G. A diagrammatic formal system for Euclidean geometry. 2001. [find](https://scholar.google.com/scholar?q=Miller%2C+N%2E+G%2E+A+diagrammatic+formal+system+for+Euclidean+geometry%2E+2001%2E)
30. Mumma, J. Proofs, pictures, and Euclid. Synthese, 2010. [find](https://scholar.google.com/scholar?q=Mumma%2C+J%2E+Proofs%2C+pictures%2C+and+Euclid%2E+Synthese%2C+2010%2E)
31. Nevins, A. J. Plane geometry theorem proving using forward chaining. Artificial Intelligence, 1975. [find](https://scholar.google.com/scholar?q=Nevins%2C+A%2E+J%2E+Plane+geometry+theorem+proving+using+forward+chaining%2E+Artificial+Intelligence%2C+1975%2E)
32. OpenAI. [GPT-4 technical report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/). arXiv:2303.08774, 2023. arXiv preprint Pan, J., Chou, G., and Berenson, D. Data-efficient learning of natural language to linear temporal logic translators for robot task specification. In International Conference on Robotics and Automation (ICRA), 2023.
33. Papineni, K., Roukos, S., Ward, T., and Zhu, W.-J. [BLEU: a method for automatic evaluation of machine translation](https://md.research.elamur.ai/free/en/papers/papineni-2002-bleu-method-automatic-evaluation-machine/). In Annual Meeting of the Association for Computational Linguistics (ACL), 2002.
34. Peng, S., Fu, D., Liang, Y., Gao, L., and Tang, Z. Geo-DRL: A self-learning framework for geometry problem solving using reinforcement learning in deductive reasoning. In Findings of the Association for Computational Linguistics: ACL, 2023. [find](https://scholar.google.com/scholar?q=Peng%2C+S%2E%2C+Fu%2C+D%2E%2C+Liang%2C+Y%2E%2C+Gao%2C+L%2E%2C+and+Tang%2C+Z%2E+Geo%2DDRL%3A+A+self%2Dlearning+framework+for+geometry+problem+solving+using+reinforcement+learning+in+deductive+reasoning%2E+In+Findings+of+the+Association+f)
35. 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.
36. Schulz, S. System description: E 1.8. In International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, 2013. [find](https://scholar.google.com/scholar?q=Schulz%2C+S%2E+System+description%3A+E+1%2E8%2E+In+International+Conference+on+Logic+for+Programming%2C+Artificial+Intelligence%2C+and+Reasoning%2C+2013%2E)
37. Schwabhäuser, W., Szmielew, W., and Tarski, A. Metamath-ematische methoden in der geometrie. Springer-Verlag, 2013. [find](https://scholar.google.com/scholar?q=Schwabha%CC%88user%2C+W%2E%2C+Szmielew%2C+W%2E%2C+and+Tarski%2C+A%2E+Metamath%2Dematische+methoden+in+der+geometrie%2E+Springer%2DVerlag%2C+2013%2E)
38. Song, P., Yang, K., and Anandkumar, A. Towards large language models as copilots for theorem proving in Lean. arXiv preprint arXiv: Arxiv-2404.12534, 2024. [find](https://scholar.google.com/scholar?q=Song%2C+P%2E%2C+Yang%2C+K%2E%2C+and+Anandkumar%2C+A%2E+Towards+large+language+models+as+copilots+for+theorem+proving+in+Lean%2E+arXiv+preprint+arXiv%3A+Arxiv%2D2404%2E12534%2C+2024%2E)
39. The mathlib Community. [The Lean mathematical library](https://md.research.elamur.ai/free/en/papers/community-2019-lean-mathematical-library/). In Certified Programs and Proofs (CPP), 2020.
40. Trinh, T., Wu, Y., Le, Q., 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, 2023.
41. Wang, Q., Kaliszyk, C., and Urban, J. [First experiments with neural translation of informal to formal mathematics](https://md.research.elamur.ai/free/en/papers/wang-2018-first-experiments-neural-translation-informal/). In Conferences on Intelligent Computer Mathematics (CICM), 2018.
42. Wu, W.-t. On the decision problem and the mechanization of theorem-proving in elementary geometry. In Selected Works Of Wen-Tsun Wu. 2008. [find](https://scholar.google.com/scholar?q=Wu%2C+W%2E%2Dt%2E+On+the+decision+problem+and+the+mechanization+of+theorem%2Dproving+in+elementary+geometry%2E+In+Selected+Works+Of+Wen%2DTsun+Wu%2E+2008%2E)
43. Wu, Y., Jiang, A., Li, W., Rabe, M., Staats, C., Jamnik, M., and Szegedy, C. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). In Neural Information Processing Systems (NeurIPS), 2022.
44. 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 (ICML), 2019.
45. Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A. Lean-Dojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023. [find](https://scholar.google.com/scholar?q=Yang%2C+K%2E%2C+Swope%2C+A%2E%2C+Gu%2C+A%2E%2C+Chalamala%2C+R%2E%2C+Song%2C+P%2E%2C+Yu%2C+S%2E%2C+Godil%2C+S%2E%2C+Prenger%2C+R%2E%2C+and+Anandkumar%2C+A%2E+Lean%2DDojo%3A+Theorem+proving+with+retrieval%2Daugmented+language+models%2E+In+Neural+Information+Proc)
46. Zhang, J.-Z., Chou, S.-C., and Gao, X.-S. Automated production of traditional proofs for theorems in Euclidean geometry I. the Hilbert intersection point theorems. Annals of Mathematics and Artificial Intelligence, 1995. [find](https://scholar.google.com/scholar?q=Zhang%2C+J%2E%2DZ%2E%2C+Chou%2C+S%2E%2DC%2E%2C+and+Gao%2C+X%2E%2DS%2E+Automated+production+of+traditional+proofs+for+theorems+in+Euclidean+geometry+I%2E+the+Hilbert+intersection+point+theorems%2E+Annals+of+Mathematics+and+Artificial)
47. A. The Formal System E We describe our variant of the formal system E in Lean-like pseudocode, including the complete list of axioms. Our design mostly follows E’s original specification (Avigad et al., 2009) with a few minor deviations. [find](https://scholar.google.com/scholar?q=A%2E+The+Formal+System+E+We+describe+our+variant+of+the+formal+system+E+in+Lean%2Dlike+pseudocode%2C+including+the+complete+list+of+axioms%2E+Our+design+mostly+follows+E%E2%80%99s+original+specification+%28Avigad+et+al)

*Updated 3 November 2026*