# Autoformalizing Euclidean Geometry

arXiv: https://arxiv.org/abs/2405.17216 · HTML: https://mlsanity.com/paper/2405.17216/

## Key facts

- Cited by 27 papers in the map (data through 14 Oct 2026).
- Builds on 25 of its 98 references that are in the map.
- First posted on arXiv 27 May 2024.

## Builds on (most cited first, 25 of 25)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning](https://mlsanity.com/paper/2105.04165/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning](https://mlsanity.com/paper/2105.14517/) (2021)
- [G-LLaVA: Solving Geometric Problem with Multi-Modal Large Language Model](https://mlsanity.com/paper/2312.11370/) (2023)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [GeomVerse: A Systematic Evaluation of Large Models for Geometric Reasoning](https://mlsanity.com/paper/2312.12241/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [First Experiments with Neural Translation of Informal to Formal Mathematics](https://mlsanity.com/paper/1805.06502/) (2018)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [Data-Efficient Learning of Natural Language to Linear Temporal Logic Translators for Robot Task Specification](https://mlsanity.com/paper/2303.08006/) (2023)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [Towards a Mathematics Formalisation Assistant using Large Language Models](https://mlsanity.com/paper/2211.07524/) (2022)
- [Proof-checking Euclid](https://mlsanity.com/paper/1710.00787/) (2017)

## Built on by (most cited first, 27 of 27)

- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs](https://mlsanity.com/paper/2502.00963/) (2025)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)
- [Premise-Augmented Reasoning Chains Improve Error Identification in Math reasoning with LLMs](https://mlsanity.com/paper/2502.02362/) (2025)
- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [Proposing and solving olympiad geometry with guided tree search](https://mlsanity.com/paper/2412.10673/) (2024)
- [miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward](https://mlsanity.com/paper/2511.03108/) (2025)
- [MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?](https://mlsanity.com/paper/2506.06034/) (2025)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [FMC: Formalization of Natural Language Mathematical Competition Problems](https://mlsanity.com/paper/2507.11275/) (2025)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [FormalRx: Rectify and eXamine Semantic Failures in Autoformalization](https://mlsanity.com/paper/2607.04655/) (2026)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [Improving Autoformalization Using Direct Dependency Retrieval](https://mlsanity.com/paper/2511.11990/) (2025)
- [Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean](https://mlsanity.com/paper/2607.19374/) (2026)
- [An Ontology-Based Approach to Optimizing Geometry Problem Sets for Skill Development](https://mlsanity.com/paper/2509.02758/) (2025)
- [Towards Autoformalization of LLM-generated Outputs for Requirement Verification](https://mlsanity.com/paper/2511.11829/) (2025)
- [Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy](https://mlsanity.com/paper/2604.02709/) (2026)
- [Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models](https://mlsanity.com/paper/2605.15131/) (2026)
- [Lean-GAP: A Dataset of Formalized Graduate Algebra Problems](https://mlsanity.com/paper/2606.02588/) (2026)
- [Analyzing the Narration Gap in LLM-Solver Loops](https://mlsanity.com/paper/2606.19588/) (2026)
- [Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry](https://mlsanity.com/paper/2608.14585/) (2026)
- [Diagnosing Sampled LLM Reasoning in Formal Geometry: Coverage, Realization, and Validity Evidence](https://mlsanity.com/paper/2609.32924/) (2026)
- [Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation](https://mlsanity.com/paper/2610.10604/) (2026)

## Abstract (arXiv)

Autoformalization involves automatically translating informal math into formal theorems and proofs that are machine-verifiable. Euclidean geometry provides an interesting and controllable domain for studying autoformalization. In this paper, we introduce a neuro-symbolic framework for autoformalizing Euclidean geometry, which combines domain knowledge, SMT solvers, and large language models (LLMs). One challenge in Euclidean geometry is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. To address this issue, we use theorem provers to fill in such diagrammatic information automatically, so that the LLM only needs to autoformalize the explicit textual steps, making it easier for the model. We also provide automatic semantic evaluation for autoformalized theorem statements. We construct LeanEuclid, an autoformalization benchmark consisting of problems from Euclid's Elements and the UniGeo dataset formalized in the Lean proof assistant. Experiments with GPT-4 and GPT-4V show the capability and limitations of state-of-the-art LLMs on autoformalizing geometry problems. The data and code are available at https://github.com/loganrjmurphy/LeanEuclid.