# FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving

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

## Key facts

- Cited by 27 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 60 references that are in the map.
- First posted on arXiv 27 Oct 2023.

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

- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [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)
- [GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning](https://mlsanity.com/paper/2105.14517/) (2021)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [A Multi-Modal Neural Geometric Solver with Textual Clauses Parsed from Diagram](https://mlsanity.com/paper/2302.11097/) (2023)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [Plane Geometry Diagram Parsing](https://mlsanity.com/paper/2205.09363/) (2022)
- [PGDP5K: A Diagram Parsing Dataset for Plane Geometry Problems](https://mlsanity.com/paper/2205.09947/) (2022)
- [Gathering Strength, Gathering Storms: The One Hundred Year Study on Artificial Intelligence (AI100) 2021 Study Panel Report](https://mlsanity.com/paper/2210.15767/) (2022)
- [Sequence to General Tree: Knowledge-Guided Geometry Word Problem Solving](https://mlsanity.com/paper/2106.00990/) (2021)
- [Mathematical conjecture generation using machine intelligence](https://mlsanity.com/paper/2306.07277/) (2023)
- [Automated Discovery of Geometrical Theorems in GeoGebra](https://mlsanity.com/paper/2202.04627/) (2022)
- [EuclidNet: Deep Visual Reasoning for Constructible Problems in Geometry](https://mlsanity.com/paper/2301.13007/) (2022)

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

- [Enhancing the Geometric Problem-Solving Ability of Multimodal LLMs via Symbolic-Neural Integration](https://mlsanity.com/paper/2504.12773/) (2025)
- [GeoUni: A Unified Model for Generating Geometry Diagrams, Problems and Problem Solutions](https://mlsanity.com/paper/2504.10146/) (2025)
- [FGeo-HyperGNet: Geometric Problem Solving Integrating FormalGeo Symbolic System and Hypergraph Neural Network](https://mlsanity.com/paper/2402.11461/) (2024)
- [Towards Geometry Problem Solving in the Large Model Era: A Survey](https://mlsanity.com/paper/2506.02690/) (2025)
- [Reliable Proof Generation with LLMs via Analogical Retrieval and Symbolic Verification: A Case Study in Euclidean Geometry](https://mlsanity.com/paper/2505.14479/) (2025)
- [What MLLMs Learn about When they Learn about Multimodal Reasoning](https://mlsanity.com/paper/2510.01719/) (2025)
- [FGeo-DRL: Deductive Reasoning for Geometric Problems through Deep Reinforcement Learning](https://mlsanity.com/paper/2402.09051/) (2024)
- [A Survey of Deep Learning for Geometry Problem Solving](https://mlsanity.com/paper/2507.11936/) (2025)
- [Bridging Formal Language with Chain-of-Thought Reasoning to Geometry Problem Solving](https://mlsanity.com/paper/2508.09099/) (2025)
- [GeoFM: Enhancing Geometric Reasoning of MLLMs via Synthetic Data Generation through Formal Language](https://mlsanity.com/paper/2510.27448/) (2025)
- [Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning](https://mlsanity.com/paper/2605.16385/) (2026)
- [GeoFocus: Blending Efficient Global-to-Local Perception for Multimodal Geometry Problem-Solving](https://mlsanity.com/paper/2602.08524/) (2026)
- [GeoChallenge: A Multi-Answer Multiple-Choice Benchmark for Geometric Reasoning with Diagrams](https://mlsanity.com/paper/2603.19252/) (2026)
- [Beyond Symbolic Solving: Multi Chain-of-Thought Voting for Geometric Reasoning in Large Language Models](https://mlsanity.com/paper/2604.00890/) (2026)
- [Geoparsing: Diagram Parsing for Plane and Solid Geometry with a Unified Formal Language](https://mlsanity.com/paper/2604.11600/) (2026)
- [FormalAnalyticGeo: A Neural-Symbolic Based Framework for Multimodal Analytic Geometry Problem Generation](https://mlsanity.com/paper/2607.12982/) (2026)
- [Concise Geometric Description as a Bridge: Unleashing the Potential of LLM for Plane Geometry Problem Solving](https://mlsanity.com/paper/2601.21164/) (2026)
- [A Survey of Multimodal Mathematical Reasoning: From Perception, Alignment to Reasoning](https://mlsanity.com/paper/2603.08291/) (2026)
- [BiNSGPS: Geometry Problem Solving via Bidirectional Neuro-Symbolic Interaction](https://mlsanity.com/paper/2606.04648/) (2026)
- [Internalizing Geometric Law: Learning from Solver Residuals for Precision-Critical Generation](https://mlsanity.com/paper/2606.09278/) (2026)
- [Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing](https://mlsanity.com/paper/2606.27926/) (2026)
- [Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry](https://mlsanity.com/paper/2608.14585/) (2026)
- [From Atomic to Agentic: Towards Interpretable Evaluation of LLMs' Agentic Mathematical Capabilities](https://mlsanity.com/paper/2608.26950/) (2026)
- [Reactivating Test-Time Scaling for Plane Geometry Problem Solving](https://mlsanity.com/paper/2608.30156/) (2026)
- [From Symbolic Perception to Logical Deduction: A Framework for Guiding Language Models in Geometric Reasoning](https://mlsanity.com/paper/2609.10335/) (2026)
- [Diagnosing Sampled LLM Reasoning in Formal Geometry: Coverage, Realization, and Validity Evidence](https://mlsanity.com/paper/2609.32924/) (2026)
- [Dense Neuro-Symbolic Reasoning in a Unified Geometry State](https://mlsanity.com/paper/2610.04280/) (2026)

## Abstract (arXiv)

This is the first paper in a series of work we have accomplished over the past three years. In this paper, we have constructed a consistent formal plane geometry system. This will serve as a crucial bridge between IMO-level plane geometry challenges and readable AI automated reasoning. Within this formal framework, we have been able to seamlessly integrate modern AI models with our formal system. AI is now capable of providing deductive reasoning solutions to IMO-level plane geometry problems, just like handling other natural languages, and these proofs are readable, traceable, and verifiable. We propose the geometry formalization theory (GFT) to guide the development of the geometry formal system. Based on the GFT, we have established the FormalGeo, which consists of 88 geometric predicates and 196 theorems. It can represent, validate, and solve IMO-level geometry problems. we also have crafted the FGPS (formal geometry problem solver) in Python. It serves as both an interactive assistant for verifying problem-solving processes and an automated problem solver. We've annotated the formalgeo7k and formalgeo-imo datasets. The former contains 6,981 (expand to 133,818 through data augmentation) geometry problems, while the latter includes 18 (expand to 2,627 and continuously increasing) IMO-level challenging geometry problems. All annotated problems include detailed formal language descriptions and solutions. Implementation of the formal system and experiments validate the correctness and utility of the GFT. The backward depth-first search method only yields a 2.42% problem-solving failure rate, and we can incorporate deep learning techniques to achieve lower one. The source code of FGPS and datasets are available at https://github.com/BitSecret/FGPS.