Research map / Large language models / Agents, code and math
Autoformalizing Euclidean Geometry
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces LeanEuclid, a Lean-based autoformalization benchmark for Euclidean geometry, with an SMT-based engine that automatically checks semantic equivalence of formalized theorems and fills diagrammatic reasoning gaps in proofs; GPT-4 and GPT-4V are evaluated few-shot.
Problem
Autoformalizing informal Euclidean geometry theorems and proofs into Lean is hard to evaluate automatically, and informal proofs rely on diagrams that leave logical gaps difficult to formalize.
Approach
Use an SMT-based symbolic engine built on a Lean implementation of Avigad's formal system E to (1) check logical equivalence between predicted and ground-truth theorem statements and (2) automatically fill diagrammatic reasoning gaps, so the LLM only autoformalizes explicit textual proof steps.
Key results
- GPT-4 with 5-shot prompting correctly autoformalizes 18.9% of theorem statements; GPT-4V reaches 21.0%, as verified by the SMT-based equivalence engine.
- For UniGeo proofs, GPT-4V 5-shot succeeds on 31% and GPT-4 5-shot on 25%; on Elements, both models fully formalize only 2 of 43 proofs.
- The SMT equivalence checker showed an estimated 15.8% false negative rate versus manual inspection on an 86-sample set, with no soundness bugs found.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use 5-shot rather than 0-shot prompting | GPT-4 theorem autoformalization · LeanEuclid theorem statements, Overall | semantic equivalence accuracy: 2.8% -> 18.9% | Helped |
| Add vision input | GPT-4 theorem autoformalization with 5-shot prompting · LeanEuclid theorem statements, Overall | semantic equivalence accuracy: 18.9% -> 21.0% | Helped |
| Increase demonstrations from 1-shot to 5-shot | GPT-4 proof autoformalization · UniGeo proofs, Overall | proof success rate: 17% -> 25% | Helped |
| Add vision input | GPT-4V proof autoformalization with 5-shot prompting · UniGeo proofs, Overall | proof success rate: 25% -> 31% | Helped |
| Add vision input | GPT-4 proof autoformalization with 5-shot prompting · LeanEuclid proofs | proof success rate: 18.8% -> 23.1% | Helped |
Surprising findings
- Zero-shot GPT-4 and GPT-4V fail to autoformalize any proofs, and the models struggle to formalize theorem statements in the formal system E, attributed to its verbosity and proof-oriented design.
Limitations
- Benchmark is small (173 examples), suitable for testing but not finetuning.
- The equivalence checker is incomplete, producing false negatives (~15.8% estimated), and SMT results are not fully certified by Lean.
- Formal system E is verbose as a specification language, making statements hard for LLMs to produce.
Experimental setup
Datasets: Euclid's Elements (Book I) UniGeo
Benchmarks: LeanEuclid
Metrics: semantic equivalence rate (proved by SMT engine) proof success rate (Lean-verified) Levenshtein similarity to repaired proofs false negative rate vs human evaluation
Baselines: AlphaGeometry GPT-4 0-shot GPT-4 1-shot
Builds on: Avigad formal system E Lean proof assistant LeanDojo AlphaGeometry
Closest papers by meaning
- Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (NeurIPS 2024 · similarity 0.90)
- ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data (NeurIPS 2025 · similarity 0.88)
- FormalAlign: Automated Alignment Evaluation for Autoformalization (ICLR 2025 · similarity 0.86)
- Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization (ICLR 2024 · similarity 0.86)
- Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning (CVPR 2026 · similarity 0.86)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.85)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.