---
title: "From Natural Language to Certified Geometry Proofs: A Survey"
description: "The authors propose a three-axis taxonomy: the job the LLM performs, how rigorous the produced proof artifact is, what kind… 14 references."
authors: ["Ioannis Tzachristas", "Georgios Tzachristas"]
year: 2026
venue: "Proceedings of The Big Picture v2: Crafting a Research Narrative"
source: "https://aclanthology.org/2026.bigpicture-main.1/"
doi: "10.18653/v1/2026.bigpicture-main.1"
licence: "CC BY 4.0 (ACL Anthology)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/tzachristas-2026-natural-language-certified-geometry-proofs/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/tzachristas-2026-natural-language-certified-geometry-proofs/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2026](https://md.research.elamur.ai/free/en/papers/2026/page/34/) / From Natural Language to Certified Geometry Proofs: A Survey of LLM-Augmented Verification and Neuro-Symbolic Theorem Proving

# From Natural Language to Certified Geometry Proofs: A Survey of LLM-Augmented Verification and Neuro-Symbolic Theorem Proving

**Authors:** [Ioannis Tzachristas](https://md.research.elamur.ai/free/en/authors/ioannis-tzachristas/) and [Georgios Tzachristas](https://md.research.elamur.ai/free/en/authors/georgios-tzachristas/) · **Year:** 2026 · **Venue:** [Proceedings of The Big Picture v2: Crafting a Research Narrative](https://md.research.elamur.ai/free/en/venues/bigpicture/) ([Big Picture v2: Crafting a Research Narrative 2026](https://md.research.elamur.ai/free/en/venues/bigpicture/2026/)) · **Publisher:** [Association for Computational Linguistics](https://md.research.elamur.ai/free/en/publishers/association-for-computational-linguistics/) · **Licence:** [CC BY 4.0 (ACL Anthology)](https://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://aclanthology.org/2026.bigpicture-main.1/) · [PDF](https://aclanthology.org/2026.bigpicture-main.1.pdf) · [DOI 10.18653/v1/2026.bigpicture-main.1](https://doi.org/10.18653/v1/2026.bigpicture-main.1) · [OpenAlex](https://openalex.org/W7166796797)

**Citations:** 0 citations (OpenAlex, 2026-10-14)

## Summary
LLMs can write persuasive geometry arguments, but those arguments may contain hallucinated steps, missing conditions or invalid inferences. Symbolic provers are rigorous, but they need formalized input and often return results that are hard for humans to read. This survey looks at hybrid systems that combine the two. In these systems, problems given as text and diagrams are converted into formal constraints, a learned or heuristic search finds proof steps, and those steps are checked by symbolic provers or proof-assistant kernels.

The authors propose a three-axis taxonomy:
- the job the LLM performs,
- how rigorous the produced proof artifact is,
- what kind of verification backend is used.

Using this taxonomy, they compare symbolic verifiers, dynamic geometry environments, formalized geometry frameworks and Olympiad-level solvers. They also link these systems to general neuro-symbolic NLP methods. Their main argument is that geometry automation should be judged on whether each intermediate step is sound and auditable, not only on whether the final answer is correct. They describe a propose–check–repair workflow and list open problems. This matters for trustworthy mathematical reasoning and for educational tools.

## Key points
- **Taxonomy:**
  - LLM roles: parser, strategist, prover, critic.
  - Proof artifacts: answer-only, informal proof, semi-formal step trace, kernel-checked proof.
  - Backends: numeric/empirical testing, algebraic provers (Wu, Gröbner), synthetic provers (area method), and Lean/Coq/Isabelle kernels.
- **Systems reviewed:** GeoS, Inter-GPS, GeoQA, FormalGeo, FGeo-DRL (RL+MCTS), AlphaGeometry, AlphaGeometry2 and the heuristic-only HAGeo. The broader NLP methods discussed are PAL, SatLM, LINC and autoformalization.
- **Olympiad results:** AlphaGeometry2 served as one component of a system whose IMO-2024 performance matched the silver-medal standard. HAGeo reports high Olympiad solving rates without any neural inference.
- **Example loop with GeoGebra:** the LLM proposes intermediate claims, GeoGebra checks them with Prove/ProveDetails, and failed claims are revised or given missing non-degeneracy conditions (NDGs).
- **Open challenges:**
  - multimodal autoformalization;
  - tracking NDGs;
  - auxiliary constructions;
  - proofs that are both certified and readable;
  - reproducible evaluation that separates formalization errors from reasoning errors.

*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

- [Technical University of Munich](https://md.research.elamur.ai/free/en/universities/technical-university-of-munich/) — University, Munich, Germany · 62 works · 48,970 citations
- [National Technical University of Athens](https://md.research.elamur.ai/free/en/universities/national-technical-university-of-athens/) — University, Athens, Greece · 8 works · 461 citations

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

🧭 Topics (2): [🧠 Language models & pretraining](https://md.research.elamur.ai/free/en/topics/language-models/) · 3,894 works · [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,685 works

## Cite

Cite as: Ioannis Tzachristas and Georgios Tzachristas. 2026. From Natural Language to Certified Geometry Proofs: A Survey of LLM-Augmented Verification and Neuro-Symbolic Theorem Proving. Proceedings of The Big Picture v2: Crafting a Research Narrative.

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

```bibtex
@inproceedings{tzachristas2026natural,
  title = {{From Natural Language to Certified Geometry Proofs: A Survey of LLM-Augmented Verification and Neuro-Symbolic Theorem Proving}},
  author = {Ioannis Tzachristas and Georgios Tzachristas},
  booktitle = {Proceedings of The Big Picture v2: Crafting a Research Narrative},
  year = {2026},
  doi = {10.18653/v1/2026.bigpicture-main.1},
  url = {https://doi.org/10.18653/v1/2026.bigpicture-main.1}
}
```

- [← previous From Narrow Unlearning to Emergent Misalignment in LLMs](https://md.research.elamur.ai/free/en/papers/mushtaq-2026-narrow-unlearning-emergent-misalignment-llms/)
- [next → From News Streams to Narrative Intelligence Briefs: LLM-Assisted Political Discourse Analysis in the Hungarian 2026 Pre-Election Context](https://md.research.elamur.ai/free/en/papers/loginova-2026-news-streams-narrative-intelligence-briefs/)
- [↑ back to papers of 2026](https://md.research.elamur.ai/free/en/papers/2026/page/34/)

## References

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

1. Francisco Botana, Markus Hohenwarter, Predrag Janičić, Zoltán Kovács, Ivan Petrović, Tomás Recio, and Simon Weitzhofer. 2015. Automated theorem proving in GeoGebra: Current achievements. Journal of Automated Reasoning, 55:39–59. [find](https://scholar.google.com/scholar?q=Francisco+Botana%2C+Markus+Hohenwarter%2C+Predrag+Janic%CC%8Cic%CC%81%2C+Zolt%C3%A1n+Kov%C3%A1cs%2C+Ivan+Petrovic%CC%81%2C+Tom%C3%A1s+Recio%2C+and+Simon+Weitzhofer%2E+2015%2E+Automated+theorem+proving+in+GeoGebra%3A+Current+achievements%2E+Journal+of)
2. Filip Marić, Ivan Petrović, Danijela Petrović, and Predrag Janičić. 2012. Formalization and implementation of algebraic methods in geometry. In Theorem Proving Components for Educational Software (THedu’11), EPTCS 79, pages 63–81. [find](https://scholar.google.com/scholar?q=Filip+Maric%CC%81%2C+Ivan+Petrovic%CC%81%2C+Danijela+Petrovic%CC%81%2C+and+Predrag+Janic%CC%8Cic%CC%81%2E+2012%2E+Formalization+and+implementation+of+algebraic+methods+in+geometry%2E+In+Theorem+Proving+Components+for+Educational+Software)
3. Jiaqi Chen, Jianheng Tang, Jinghui Qin, Xiaodan Liang, Lingbo Liu, Eric Xing, and Liang Lin. 2021. [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 Nous Research. 2026. Hermes agent: The self-improving ai agent built by nous research. https://gi…
4. Jia Zou, Xiaokai Zhang, Yiming He, Na Zhu, and Tuo Leng. 2024. Fgeo-drl: Deductive reasoning for geometric problems through deep reinforcement learning. arXiv:2402.09051. — [arXiv:2402.09051](https://arxiv.org/abs/2402.09051) [find](https://scholar.google.com/scholar?q=Jia+Zou%2C+Xiaokai+Zhang%2C+Yiming+He%2C+Na+Zhu%2C+and+Tuo+Leng%2E+2024%2E+Fgeo%2Ddrl%3A+Deductive+reasoning+for+geometric+problems+through+deep+reinforcement+learning%2E+arXiv%3A2402%2E09051%2E+%E2%80%94+%5BarXiv%3A2402%2E09051%5D%28https%3A%2F%2F)
5. Theo X. Olausson, Alex Gu, Benjamin Lipkin, Cedegao E. Zhang, Armando Solar-Lezama, Joshua B. Tenenbaum, and Roger Levy. 2023. [LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers](https://md.research.elamur.ai/free/en/papers/olausson-2023-linc-neurosymbolic-approach-logical-reasoning/). arXiv:2310.15164.
6. OpenClaw Contributors. 2026. Openclaw: Personal ai assistant. [https://github.com/openclaw/open](https://github.com/openclaw/open) claw. Open-source software repository. Accessed 2026-05-14. [↗](https://github.com/openclaw/open)
7. Bowen Ping, Minnan Luo, Zhuohang Dang, Chenxi Wang, and Chengyou Jia. 2025. Autogps: Automated geometry problem solving via multimodal formalization and deductive reasoning. arXiv:2505.23381. — [arXiv:2505.23381](https://arxiv.org/abs/2505.23381) [find](https://scholar.google.com/scholar?q=Bowen+Ping%2C+Minnan+Luo%2C+Zhuohang+Dang%2C+Chenxi+Wang%2C+and+Chengyou+Jia%2E+2025%2E+Autogps%3A+Automated+geometry+problem+solving+via+multimodal+formalization+and+deductive+reasoning%2E+arXiv%3A2505%2E23381%2E+%E2%80%94+%5BarXiv)
8. Minjoon Seo, Hannaneh Hajishirzi, Ali Farhadi, Oren Etzioni, and Clint Malcolm. 2015. [Solving geometry problems: Combining text and diagram interpretation](https://md.research.elamur.ai/free/en/papers/seo-2015-solving-geometry-problems-combining-text/). In Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pages 1466–1476.
9. Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, Thang Luong, et al. 2024. [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.
10. Ioannis Tzachristas and Georgios Tzachristas. 2026. Proofing techniques in geometry using LLMs and GeoGebra: A case study of the triangle-side trisection theorem. In 7th International Congress on Mathematics (MICOM 2026), Thessaloniki, Greece. Mathematical Society of South-Eastern Europe (MASSEE). P… [find](https://scholar.google.com/scholar?q=Ioannis+Tzachristas+and+Georgios+Tzachristas%2E+2026%2E+Proofing+techniques+in+geometry+using+LLMs+and+GeoGebra%3A+A+case+study+of+the+triangle%2Dside+trisection+theorem%2E+In+7th+International+Congress+on+Math)
11. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). In Advances in Neural Information Processing Systems.
12. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. [Leandojo: Theorem proving with retrieval-augmented language models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). arXiv:2306.15626.
13. Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. [SatLM: Satisfiability-aided language models using declarative prompting](https://md.research.elamur.ai/free/en/papers/ye-2023-satlm-satisfiability-aided-language-models/). In Advances in Neural Information Processing Systems.
14. Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang, Xiaoxiao Jin, Yanjun Guo, Chenyang Mao, Yang Li, Zhe Zhu, Dengfeng Yue, Fangzhen Zhu, Yifan Wang, Yiwen Huang, Runan Wang, Cheng Qin, Zhenbing Zeng, Shaorong Xie, Xiangfeng Luo, [find](https://scholar.google.com/scholar?q=Xiaokai+Zhang%2C+Na+Zhu%2C+Yiming+He%2C+Jia+Zou%2C+Qike+Huang%2C+Xiaoxiao+Jin%2C+Yanjun+Guo%2C+Chenyang+Mao%2C+Yang+Li%2C+Zhe+Zhu%2C+Dengfeng+Yue%2C+Fangzhen+Zhu%2C+Yifan+Wang%2C+Yiwen+Huang%2C+Runan+Wang%2C+Cheng+Qin%2C+Zhenbing+Ze)

*Updated 2 November 2026*