Elamur Research⌕
☰
home / papers / 2026 / 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

Paper · 2026 · Ioannis Tzachristas and Georgios Tzachristas

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 MunichMunich · Germany55 works · 48,474 citations🎓National Technical University of AthensAthens · Greece8 works · 461 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksComputational Theory and Mathematics · 252 works

🧭 Topics 2Research subjects and languages the work is about.Language models & pretraining · 3,320 worksReasoning · 1,426 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. DOI 10.18653/v1/2026.bigpicture-main.1

@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}
}

References

14 references, 6 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
  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
  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. 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
  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. arXiv:2310.15164.
  6. OpenClaw Contributors. 2026. Openclaw: Personal ai assistant. https://github.com/openclaw/open claw. Open-source software repository. Accessed 2026-05-14. ↗
  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
  8. Minjoon Seo, Hannaneh Hajishirzi, Ali Farhadi, Oren Etzioni, and Clint Malcolm. 2015. Solving geometry problems: Combining text and diagram interpretation. 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. 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
  11. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with 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. arXiv:2306.15626.
  13. Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. SatLM: Satisfiability-aided language models using declarative prompting. In Advances in Neural Information Processing Systems. find
  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

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/tzachristas-2026-natural-language-certified-geometry-proofs/