Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry

# A Unified Neuro-Symbolic Framework for Plane Geometry
Source: [https://arxiv.org/html/2608.14585](https://arxiv.org/html/2608.14585)
Zhaoyu Li2, Hangrui Bi211footnotemark:1, Youyuan Zhang2, Wenjie Ma3 Zenan Li4, Zhaolei Zhang2, Xujie Si2, Kaiyu Yang1 1Apodex,2University of Toronto,3UC Berkeley,4ETH Zürich zhaoyu@cs\.toronto\.edu,hangruibi@outlook\.com, windsey@berkeley\.edu,zenan\.li@inf\.ethz\.ch, zhaolei\.zhang@utoronto\.ca, six@cs\.toronto\.edu,kaiyu@apodex\.com Equal contribution\. This work was partially done during Zhaoyu’s internship at Meta FAIR and Kaiyu Yang’s employment at Meta FAIR\.

###### Abstract

Euclidean geometry is a compelling testbed for AI reasoning, as it demands the combination of intuitive diagram understanding, axiomatic deduction, and algebraic computation\. Yet, existing approaches typically address only a subset of these abilities or struggle with competition\-level problems\. We introduceEuclid\-Omni, a unified neuro\-symbolic framework that couples a formal geometry system with Large Language Models \(LLMs\) and Vision\-Language Models \(VLMs\) to tackle both calculation\- and proving\-style problems, in formal and natural languages, up to Olympiad\-level difficulty\. At its core, we developEuclidea, a versatile symbolic geometry solver that automatically generates reasoning steps through deductive inference and algebraic computation\. Building on this, we develop a data\-generation pipeline that synthesizes symbolic problems and solutions, renders diagrams, and translates them into natural language, producing large\-scale, diverse datasets for training LLMs and VLMs across a wide range of reasoning settings\. Experiments show that VLMs trained on our synthetic data achieve superior performance on calculation tasks, and that LLMs combined withEuclideaare competitive with state\-of\-the\-art systems on Olympiad\-level proving problems, despite using orders of magnitude less compute and training data\. Code and scripts are publicly available at[https://github\.com/20171130/Euclid\-Omni](https://github.com/20171130/Euclid-Omni)\.

## 1Introduction

Plane geometry has been a cornerstone of mathematical education for over two millennia, ever since Euclid’s*Elements*, with problems ranging from elementary classroom exercises to International Mathematical Olympiad \(IMO\) challenges\. It also occupies a special place in the history of artificial intelligence, where it inspired some of the earliest symbolic systems for automated theorem proving\[[13](https://arxiv.org/html/2608.14585#bib.bib13)\]\. With the recent surge of large language models \(LLMs\) and vision\-language models \(VLMs\), plane geometry has once again become a popular testbed for probing and improving machine reasoning\[[45](https://arxiv.org/html/2608.14585#bib.bib45),[31](https://arxiv.org/html/2608.14585#bib.bib31),[60](https://arxiv.org/html/2608.14585#bib.bib60)\], and state\-of\-the\-art systems\[[57](https://arxiv.org/html/2608.14585#bib.bib57),[11](https://arxiv.org/html/2608.14585#bib.bib11),[8](https://arxiv.org/html/2608.14585#bib.bib8)\]have now reached the level of IMO gold medalists, marking a new milestone in automated geometric reasoning\.

These advances, however, remain limited in both scope and accessibility\. On the scope side, IMO\-level systems are tailored almost exclusively to competition\-style theorem proving and offer little support for the algebraic computation that calculation\-based problems require, even though such problems are equally common in plane geometry\. They also tend to produce solutions that are far from how humans reason and rarely engage with natural language or visual diagrams, which restricts their usefulness in educational settings\. The complementary line of work that targets calculation tasks faces the opposite problem: it covers only a narrow set of theorems and stops well short of competition\-level difficulty\[[6](https://arxiv.org/html/2608.14585#bib.bib6),[30](https://arxiv.org/html/2608.14585#bib.bib30),[7](https://arxiv.org/html/2608.14585#bib.bib7)\]\. On the accessibility side, training IMO\-level systems consumes enormous compute, and to date none has released its data\-generation pipeline or training data\. Public datasets, in turn, remain small, lack diversity, and are poorly stratified by difficulty\[[6](https://arxiv.org/html/2608.14585#bib.bib6),[30](https://arxiv.org/html/2608.14585#bib.bib30),[4](https://arxiv.org/html/2608.14585#bib.bib4),[7](https://arxiv.org/html/2608.14585#bib.bib7)\], which makes them inadequate for training modern LLMs and VLMs at scale\. Taken together, these gaps make existing approaches difficult to build on as a general foundation for research in geometric reasoning\.

To bridge this gap, we introduceEuclid\-Omni, a unified neuro\-symbolic framework that targets a broad range of geometric reasoning settings\. At the heart of Euclid\-Omni isEuclidea, a symbolic engine that exhaustively applies admissible inference rules until the deductive closure is reached\. Most existing IMO\-level systems are built on full\-angle notation\[[14](https://arxiv.org/html/2608.14585#bib.bib14)\], which is convenient for certain competition\-style proofs\. However, it cannot distinguish an angle or arc from its supplement and is therefore ill\-suited to calculation problems\. Euclidea instead grounds its axiomatic foundation directly in Euclid’s*Elements*\[[1](https://arxiv.org/html/2608.14585#bib.bib1)\]\. This allows it to handle both calculation and proving tasks within a single framework, and yields reasoning steps that closely resemble those taught in school geometry\. We evaluate Euclidea on Geometry3K\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\], JGEX\-AG\-231\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], and IMO\-AG\-30\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], which together cover both calculation and proving, and find that it solves more problems than existing formal geometry systems while producing notably more human\-readable solutions\.

Built on top of Euclidea, our second contribution is a versatile data\-generation pipeline for training LLMs and VLMs\. The pipeline produces geometry problems across text and vision modalities, in formal and natural language, and for both calculation and proving tasks\. It is highly configurable, so the resulting datasets can be tailored to specific training objectives and difficulty levels, from elementary problems to IMO\-level challenges\. To assess the pipeline, we use its synthetic data to train models for two settings that sit at opposite ends of the geometric reasoning spectrum: \(i\) multimodal geometric calculation with diagram visualizations and natural\-language descriptions, and \(ii\) Olympiad\-level formal theorem proving\. In the first setting, we train VLMs on our synthetic data and evaluate them on GeoQA\[[6](https://arxiv.org/html/2608.14585#bib.bib6)\], Geometry3K\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\], MathVista\[[31](https://arxiv.org/html/2608.14585#bib.bib31)\], and MathVerse\[[60](https://arxiv.org/html/2608.14585#bib.bib60)\]; despite using substantially less training data than prior work, our models match or surpass existing approaches across these benchmarks\. In the second setting, we evaluate an LLM trained on our synthetic data on JGEX\-AG\-231\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]and IMO\-AG\-30\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], which consistently outperforms proprietary LLM baselines and is competitive with state\-of\-the\-art systems\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]while using orders of magnitude less compute and training data\.

## 2Related Work

Symbolic Approaches\.Classical formal geometry solvers follow two main paradigms\[[13](https://arxiv.org/html/2608.14585#bib.bib13)\]: synthetic deduction and algebraic computation\. Synthetic methods, such as the deductive database approach\[[15](https://arxiv.org/html/2608.14585#bib.bib15),[56](https://arxiv.org/html/2608.14585#bib.bib56)\], employ forward chaining to systematically apply geometric rules and derive new facts, but they struggle with problems requiring complex algebraic manipulation\. Algebraic methods, including Gröbner basis\[[26](https://arxiv.org/html/2608.14585#bib.bib26)\]and Wu’s method\[[50](https://arxiv.org/html/2608.14585#bib.bib50)\], encode geometric relations as polynomial equations and solve them algebraically, offering strong reasoning power but often producing proofs that are difficult to interpret\. Hybrid systems, such as NGS\[[6](https://arxiv.org/html/2608.14585#bib.bib6)\]and Inter\-GPS\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\]for calculation, LeanEuclid\[[37](https://arxiv.org/html/2608.14585#bib.bib37)\]and DD\+AR\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]for theorem proving, attempt to combine deductive and algebraic reasoning, yet remain specialized in certain task types with limited generality\. Other frameworks, including FormalGeo\[[62](https://arxiv.org/html/2608.14585#bib.bib62)\]and PyEuclid\[[28](https://arxiv.org/html/2608.14585#bib.bib28)\], pursue a unified approach, but still struggle to scale efficiently to Olympiad\-level problems\.

Datasets and Benchmarks\.Many geometry datasets are derived from textbooks, exercises, and competitions, where problems are paired with manually constructed symbolic formulations\[[4](https://arxiv.org/html/2608.14585#bib.bib4),[7](https://arxiv.org/html/2608.14585#bib.bib7),[59](https://arxiv.org/html/2608.14585#bib.bib59),[62](https://arxiv.org/html/2608.14585#bib.bib62)\]\. Examples include calculation\-oriented datasets such as GeoQA\[[6](https://arxiv.org/html/2608.14585#bib.bib6)\]and Geometry3K\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\], as well as theorem proving datasets such as UniGeo\[[7](https://arxiv.org/html/2608.14585#bib.bib7)\], JGEX\-AG\-231\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], and IMO\-AG\-30\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]\. Due to the high cost of manual annotation, these resources remain relatively small in scale\. To expand coverage, recent work\[[21](https://arxiv.org/html/2608.14585#bib.bib21),[61](https://arxiv.org/html/2608.14585#bib.bib61)\]leverages LLMs and VLMs to generate larger datasets by augmenting existing problems, though their diversity remains bounded by the underlying sources\. In parallel, several synthetic pipelines\[[25](https://arxiv.org/html/2608.14585#bib.bib25),[17](https://arxiv.org/html/2608.14585#bib.bib17),[39](https://arxiv.org/html/2608.14585#bib.bib39),[19](https://arxiv.org/html/2608.14585#bib.bib19),[9](https://arxiv.org/html/2608.14585#bib.bib9),[49](https://arxiv.org/html/2608.14585#bib.bib49)\]generate symbolic problems using basic geometric primitives and predicates, but the resulting instances are always constrained in both difficulty and variety\. Other benchmarks\[[58](https://arxiv.org/html/2608.14585#bib.bib58),[46](https://arxiv.org/html/2608.14585#bib.bib46),[42](https://arxiv.org/html/2608.14585#bib.bib42),[53](https://arxiv.org/html/2608.14585#bib.bib53)\], including MathVista\[[31](https://arxiv.org/html/2608.14585#bib.bib31)\]and MathVerse\[[60](https://arxiv.org/html/2608.14585#bib.bib60)\], collect a wide variety of geometry questions in natural language to evaluate the reasoning abilities of VLMs\. Beyond solving geometry problems, auxiliary datasets have also been introduced for related tasks such as autoformalization\[[37](https://arxiv.org/html/2608.14585#bib.bib37)\], diagram parsing\[[22](https://arxiv.org/html/2608.14585#bib.bib22)\], diagram understanding\[[23](https://arxiv.org/html/2608.14585#bib.bib23)\], and geometric image generation\[[3](https://arxiv.org/html/2608.14585#bib.bib3)\]\.

Learning\-Based Methods\.Recent advances in LLMs and VLMs have spurred a wave of learning\-based approaches to geometric reasoning\[[65](https://arxiv.org/html/2608.14585#bib.bib65),[32](https://arxiv.org/html/2608.14585#bib.bib32)\]\. One line of work adopts neuro\-symbolic methods that operate over symbolic representations\[[6](https://arxiv.org/html/2608.14585#bib.bib6),[30](https://arxiv.org/html/2608.14585#bib.bib30),[7](https://arxiv.org/html/2608.14585#bib.bib7),[40](https://arxiv.org/html/2608.14585#bib.bib40),[52](https://arxiv.org/html/2608.14585#bib.bib52),[21](https://arxiv.org/html/2608.14585#bib.bib21),[48](https://arxiv.org/html/2608.14585#bib.bib48),[45](https://arxiv.org/html/2608.14585#bib.bib45),[57](https://arxiv.org/html/2608.14585#bib.bib57),[18](https://arxiv.org/html/2608.14585#bib.bib18),[64](https://arxiv.org/html/2608.14585#bib.bib64),[63](https://arxiv.org/html/2608.14585#bib.bib63),[41](https://arxiv.org/html/2608.14585#bib.bib41)\]: these approaches leverage LLMs or VLMs to generate solution steps in symbolic form and delegate execution to a solver, ensuring both correctness and interpretability\. For example, Inter\-GPS\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\]predicts program sequences to compute numerical quantities, while AlphaGeometry\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]predicts auxiliary constructions and integrates them with its symbolic engine for theorem proving\. Such systems enable faithful reasoning but heavily rely on the solver’s design and symbolic coverage\. In contrast, purely neural methods reason directly in natural language\[[21](https://arxiv.org/html/2608.14585#bib.bib21),[54](https://arxiv.org/html/2608.14585#bib.bib54),[17](https://arxiv.org/html/2608.14585#bib.bib17),[49](https://arxiv.org/html/2608.14585#bib.bib49)\], typically targeting calculation problems with verifiable numerical answers and using chain\-of\-thought reasoning\[[47](https://arxiv.org/html/2608.14585#bib.bib47)\]to produce step\-by\-step solutions\. While effective on simple problems, these approaches often generate hallucinated intermediate steps and are difficult to verify, limiting their reliability for theorem proving and other complex scenarios\. Some methods\[[38](https://arxiv.org/html/2608.14585#bib.bib38),[29](https://arxiv.org/html/2608.14585#bib.bib29),[27](https://arxiv.org/html/2608.14585#bib.bib27),[51](https://arxiv.org/html/2608.14585#bib.bib51),[12](https://arxiv.org/html/2608.14585#bib.bib12)\]also aim to improve visual perception and diagram understanding in VLMs for geometric reasoning\. Nevertheless, no unified framework yet exists for training LLMs and VLMs to flexibly support diverse geometry tasks across both formal and natural languages\.

## 3Method

![Refer to caption](https://arxiv.org/html/2608.14585v1/x1.png)Figure 1:An illustrative example of Euclidea solving a proving\-style geometry problem\.### 3\.1Euclidea

Euclidea is a Python\-based formal plane geometry system that encodes information from both text and diagrams\. Its reasoning engine integrates deductive inference with algebraic computation\. An overview of Euclidea is shown in Figure[1](https://arxiv.org/html/2608.14585#S3.F1)\.

Problem Formalization\.Euclidea formalizes plane geometry by combining two established approaches to geometric representation\[[15](https://arxiv.org/html/2608.14585#bib.bib15),[1](https://arxiv.org/html/2608.14585#bib.bib1)\][A\.1](https://arxiv.org/html/2608.14585#A1.SS1)\. It treats points as the basic primitives, while all other objects \(e\.g\., lines, triangles\) are defined in terms of points\[[15](https://arxiv.org/html/2608.14585#bib.bib15)\]\. A diagram is then formalized as a set of points together with their relations, which fall into two categories\[[1](https://arxiv.org/html/2608.14585#bib.bib1)\]:

- •Metric relationsencode quantitative properties, such asPerpendicular\(a,b,c,d\)\(ab⟂\\perpcd\) orAngle\(a,b,c\)=π/2\\texttt\{Angle\(a,b,c\)\}=\\pi/2\(∠​a​b​c=90∘\\angle abc=90^\{\\circ\}\), and include algebraic equations over geometric quantities such as lengths, angles, ratios, and areas\.
- •Diagrammatic relationscapture topological configurations that can be read off directly from the diagram, such asSameSide\(a,b,c,d\)\(pointsaandblie on the same side of linecd\)\.

As in human reasoning, metric relations must be stated explicitly—either given in the problem statement or derived through geometric theorems—whereas diagrammatic relations are typically implicit and inferred from the diagram\.

Reasoning Engine\.Given a diagram, Euclidea combines a deductive database with an algebraic system to derive new relations from the initial conditions\. The deductive component extends existing approaches\[[56](https://arxiv.org/html/2608.14585#bib.bib56),[45](https://arxiv.org/html/2608.14585#bib.bib45)\]with a richer and more fine\-grained set of inference rules defined over our formal representations, and these rules are systematically enumerated to identify applicable theorems\. For example, the Angle Bisector Theorem can be formalized as:

AngleBisectorTheorem\(a,b,c,d\): Angle\(d,a,b\) = Angle\(d,a,c\)∧\\landCollinear\(d,b,c\)∧\\landBetween\(d,b,c\)∧\\landNot\(Collinear\(a,b,c\)\)⇒\\RightarrowLength\(d,b\)/Length\(d,c\) = Length\(a,b\)/Length\(a,c\)

where pointdlies on linebcand on the angle bisector of∠​b​a​c\\angle bac\. Note that, unlike previous approaches\[[15](https://arxiv.org/html/2608.14585#bib.bib15)\]which treat equal\-angle as an atomic proposition, Euclidea treats it as a relation between interpreted variables, which is key to bridging geometry and algebra and to handling both calculation and proving tasks\. An SQL database\[[20](https://arxiv.org/html/2608.14585#bib.bib20)\]is used to efficiently enumerate applicable rules: relations and equivalence classes of variables are stored in tables, and conditions are represented as table joins\. This design makes the deductive database easily extensible: new inference rules can be added without requiring manual implementation of dedicated enumerators\. Further details are provided in Appendix[A\.2](https://arxiv.org/html/2608.14585#A1.SS2)\.

Complementing the deductive database, Euclidea integrates a symbolic algebraic system built on SymPy\[[35](https://arxiv.org/html/2608.14585#bib.bib35)\]to simplify equations and solve for unknown quantities\. Inspired by DD\+AR\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], equations are categorized into four types: \(i\)*angle\-based*\(fixed angle, angle sum, and angle ratio\), \(ii\)*length\-based*\(fixed length, length sum, and length ratio\), \(iii\)*length\-ratio\-based*\(fixed length, length ratio, and equalities between ratios or between an area and the product of two lengths\), and \(iv\)*complex*\(all remaining forms, e\.g\., trigonometric or higher\-order polynomial ones\)\. The first two types can be transformed into a linear systemA​𝐱=𝐛A\\mathbf\{x\}=\\mathbf\{b\}, where𝐱\\mathbf\{x\}is a vector of geometric quantities andAAand𝐛\\mathbf\{b\}denote the corresponding coefficients and constants, which is then solved via Gaussian elimination\. The third type can be reduced to a log\-linear form and solved analogously\. For typical geometry problems, the diagram retains some degrees of freedom and the known conditions are underdetermined\. Rather than producing a unique solution, Gaussian elimination reduces the system to a minimal set of free variables and expresses all other variables in terms of them\. We can then determine whether an expression evaluates to a constant, or whether an equation holds, by substituting the values into the equation and checking whether the free variables can be eliminated\. For complex equations, Euclidea leverages the accumulated linear/log\-linear results for simplification and substitution, often reducing them to single\- or double\-variable equations that can be further simplified into new relations or solved directly for unknown quantities\. Some examples are provided in Appendix[A\.3](https://arxiv.org/html/2608.14585#A1.SS3)\.

Euclidea invokes the deductive database and the algebraic system in tandem, with each component reinforcing the other, incrementally expanding the state with new relations\. A problem is solved once the goal is either contained in the derived relations or evaluated to a numerical value\. The engine halts once closure is reached and no further conclusions can be derived\.

Solution Generation\.To generate human\-readable reasoning traces, each relation produced by the deductive database is labeled with its originating inference rule and conditions\. For each equationeesolved via Gaussian elimination, we cast the tracking process as an optimization problem:

min𝐳⁡‖𝐳‖t,s\.t\.\[A\|𝐛\]⊤​𝐳=𝐜,\\min\_\{\\mathbf\{z\}\}\\;\\\|\\mathbf\{z\}\\\|\_\{t\},\\quad\\text\{s\.t\.\}\\quad\[A\\;\|\\;\\mathbf\{b\}\]^\{\\top\}\\mathbf\{z\}=\\mathbf\{c\},where\[A\|𝐛\]\[A\\;\|\\;\\mathbf\{b\}\]is the augmented coefficient matrix of the linear systemA​𝐱=𝐛A\\mathbf\{x\}=\\mathbf\{b\},𝐜\\mathbf\{c\}is the coefficient vector of the query equationee,𝐳\\mathbf\{z\}denotes the coefficients of the equations contributing to the query, andttspecifies the chosen norm \(0 or 1\) to promote sparsity and yield a minimal set of traced equations\. The optimization is solved with PySCIPOpt\[[33](https://arxiv.org/html/2608.14585#bib.bib33)\]\. For quantities derived from complex equations, Euclidea records the original complex equation together with the substituted equations from the previous linear systems\. Detailed examples are provided in Appendix[A\.4](https://arxiv.org/html/2608.14585#A1.SS4)\.

Starting from the goal, Euclidea recursively traces all dependent relations until each is grounded in the initial conditions\. This yields a dependency graph in which the goal is the root, the given conditions are the leaves, the inferred relations form the intermediate nodes, and the edges represent their dependencies\. A post\-order traversal then linearizes these relations into an ordered sequence of reasoning steps, which is formatted into a coherent, human\-readable symbolic solution\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/x2.png)Figure 2:An illustrative example of Euclid\-Omni generating a calculation\-style geometry problem\.
### 3\.2Euclid\-Omni

Building on the formalization and reasoning of Euclidea, Euclid\-Omni provides a unified framework that integrates a synthetic problem generator, a diagram renderer, and a natural language translator to produce large\-scale, diverse training data with flexible configurations for a variety of geometry tasks\. An overview of Euclid\-Omni is shown in Figure[2](https://arxiv.org/html/2608.14585#S3.F2)\.

Synthetic Problem Generation\.Euclid\-Omni synthesizes plane geometry problems*from scratch*, allowing fine\-grained control over problem structure\. Inspired by AlphaGeometry\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], we extend a library of artificial*construction rules*, each of which corresponds to a ruler\-and\-compass operation that bundles a set of condition and conclusion relations to construct new points, optionally conditioned on previously constructed ones\. For example,x = construct\_foot\(a,b,c\)constructs the foot of the perpendicular from pointato linebc, and is formalized as:

∃\\existsx, Not\(Collinear\(a,b,c\)\)⇒\\RightarrowPerpendicular\(x,a,b,c\)∧\\landCollinear\(x,b,c\)

To generate a new problem, Euclid\-Omni iteratively applies construction rules until the desired complexity is reached\. For each selected rule, Euclid\-Omni samples numerical coordinates that satisfy all required conditions, and then adds the corresponding conclusions to the current state of Euclidea\. To support calculation\-style problems, Euclid\-Omni also parameterizes a subset of construction rules with explicit geometric quantities such as lengths or angles\. For example,a,b,c,d = construct\_square\_q\(l\)constructs a squareabcdwith side lengthl, represented as:

∃\\existsa,b,c,d, True⇒\\RightarrowSquare\(a,b,c,d\)∧\\landLength\(a,b\) = l

Notably, even when the same sequence of construction rules is applied, the randomly sampled point coordinates can give rise to distinct topological configurations across runs\. An illustrative example is provided in Appendix[B\.1](https://arxiv.org/html/2608.14585#A2.SS1)\.

Given a sampled diagram, Euclidea infers all possible conclusions from the construction and generates the corresponding reasoning steps\. To generate a problem from a diagram, we filter and select specific conclusions as target goals according to the task requirements\. For each selected goal, we trace its minimal supporting set of construction rules from the inferred solution and remove any redundant constructions, thereby preserving the structural minimality of the synthesized problem\.

Diagram Rendering\.We implement a diagram renderer that visualizes each sampled problem by drawing geometric objects such as segments and circles from their point coordinates\. For each construction rule, we predefine the set of objects and annotations to display, and render them on a Matplotlib\[[24](https://arxiv.org/html/2608.14585#bib.bib24)\]canvas\. For example,x = construct\_foot\(a,b,c\)draws the segmentsbc,xa,xb, andxc, as well as the right angle∠\\angleaxb\.

Natural Language Translation\.To train models to perform geometric reasoning in natural language, Euclid\-Omni supports translating symbolic problems and solutions into fluent textual form\. However, translating directly via prompting would require specifying the full formal language and its semantics, which inevitably leads to lengthy prompts and offers no guarantees of correctness or consistency\. Instead, we adopt a hybrid strategy\[[23](https://arxiv.org/html/2608.14585#bib.bib23)\]: we construct a library of manually verified natural language templates that cover each construction rule appearing in the problem and each relation appearing in the solution\. Given a symbolic problem and its solution, we parse their structure and instantiate the templates to produce aligned drafts, and then prompt an LLM to paraphrase these drafts into more natural and diverse problem statements and reasoning steps\. Examples of templates and prompts are provided in Appendix[B\.2](https://arxiv.org/html/2608.14585#A2.SS2)\.

Task Configuration\.With Euclid\-Omni, we can generate formal and natural language problems together with their corresponding solutions and diagrams\. The pipeline allows users to flexibly configure each component to produce data tailored to specific geometric reasoning tasks\. In this paper, we focus on two representative settings: \(i\) following standard visual reasoning benchmarks\[[31](https://arxiv.org/html/2608.14585#bib.bib31),[60](https://arxiv.org/html/2608.14585#bib.bib60)\], we evaluate VLMs on calculation problems solved end\-to\-end from natural\-language statements and diagrams; and \(ii\) following IMO\-oriented systems\[[45](https://arxiv.org/html/2608.14585#bib.bib45),[11](https://arxiv.org/html/2608.14585#bib.bib11)\], we adopt a neuro\-symbolic workflow in which an LLM proposes auxiliary constructions in a formal language and a symbolic solver integrates these candidates to solve Olympiad\-level proving problems\.

For the first setting, the problem generator samples construction rules, optionally with quantitative parameterization, and restricts target goals to those involving geometric quantities such as lengths, angles, and areas\. Variable\-based formulations are also supported by defining linear equations over lengths or angles \(e\.g\.,x\+10∘=∠​a​b​cx\+10^\{\\circ\}=\\angle abc\) and treating the variable as the goal\. To support the multiple\-choice format used by existing benchmarks, we adapt the LLM prompts during natural language translation to generate plausible distractors of a scale comparable to the correct answer\. For training, we translate the generated problem and solution into natural language using the methods described above\. The supervised fine\-tuning template is:Inputs: <diagram\> <natural language problem\> Outputs: <natural language solution\> \\boxed\{<final answer/choice\>\}\.

For the theorem proving setting, auxiliary constructions are constructions that are necessary for proving the target goal but are not directly involved in constructing it\. Finding such auxiliary constructions is typically the most challenging part of competition\-level theorem proving\. Therefore, when training LLMs for theorem proving, we remove the auxiliary constructions from the problem and train the model to recover them\. We sample 8–10 construction rules and restrict goals to common Olympiad\-style targets such as midpoint, collinearity, similarity, congruence, concyclicity, and equality of lengths or angles\. Following prior work\[[57](https://arxiv.org/html/2608.14585#bib.bib57)\], only the formal problem statement and the auxiliary constructions are retained for training\. The supervised fine\-tuning template is:Inputs: <formal problem\> Outputs: <formal auxiliary constructions\>\.

We provide several examples of synthetic instances for these two tasks in Appendix[B\.3](https://arxiv.org/html/2608.14585#A2.SS3)\. Note that the Euclid\-Omni pipeline can also be configured to generate data for other tasks, such as autoformalization\[[37](https://arxiv.org/html/2608.14585#bib.bib37)\], diagram generation\[[10](https://arxiv.org/html/2608.14585#bib.bib10)\], and diagram understanding\[[23](https://arxiv.org/html/2608.14585#bib.bib23)\]\. We discuss these potential applications in Section[5](https://arxiv.org/html/2608.14585#S5)and leave them as future directions for the community to explore\.

## 4Experiments

### 4\.1Symbolic Solvers

Setup\.We evaluate Euclidea against open\-source formal geometry systems on three benchmarks: \(i\) Geometry3K\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\], SAT\-style calculation problems; \(ii\) JGEX\-AG\-231\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], textbook theorems and Olympiad\-level problems; and \(iii\) IMO\-AG\-30\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], IMO problems from 2000–2022\. For Geometry3K, we adopt the PyEuclid formalization\[[28](https://arxiv.org/html/2608.14585#bib.bib28)\]with minor modifications and correct several annotation errors in the released logical forms\. For JGEX\-AG\-231 and IMO\-AG\-30, we adopt the original formalizations with minor adjustments for compatibility with our formal language\. For calculation tasks, we compare against Inter\-GPS\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\]and PyEuclid\[[28](https://arxiv.org/html/2608.14585#bib.bib28)\]; for proving, against DD\+AR\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], Newclid\[[43](https://arxiv.org/html/2608.14585#bib.bib43)\], and PyEuclid\[[28](https://arxiv.org/html/2608.14585#bib.bib28)\]\. Following PyEuclid’s protocol, a numerical prediction is correct if within 2% of the labeled answer, while a proving solution must output a valid proof\. We use a 600\-second time limit per problem\.

Table 1:Solved problems by formal geometry solvers on three calculation and proving benchmarks \(totals in parentheses\)\. –: unsupported task or formalization;†: reported in prior work\.SolverCalculationProvingGeometry3K \(601\)JGEX\-AG\-231 \(231\)IMO\-AG\-30 \(30\)Inter\-GPS†426––PyEuclid†567202–DD\+AR†–19814Newclid–18814Euclidea59520716w/o algebraic system1740w/o deductive database3620Results\.Table[1](https://arxiv.org/html/2608.14585#S4.T1)shows that Euclidea consistently outperforms all existing systems, solving 99% of Geometry3K and two additional challenging IMO problems\. The ablation confirms that the deductive database and the algebraic system are individually insufficient; their integration is crucial and enables Euclidea to solve an order of magnitude more problems\. The remaining unsolved problems fall into three categories: those that cannot be formalized within Euclidea, outliers with too many points \(yielding prohibitively large search spaces and timeouts\), and those requiring auxiliary constructions\. Beyond higher solve rates, Euclidea also produces higher\-quality symbolic proofs that are more human\-like and better aligned with diagrams than those of DD\+AR and Newclid, while remaining significantly more compact than those of PyEuclid \(Appendix[C\.1](https://arxiv.org/html/2608.14585#A3.SS1)\)\.

### 4\.2Natural\-Language Calculation Problems

Setup\.Using Euclid\-Omni, we synthesize 10K training instances and translate each into natural language with Gemini 2\.5 Flash\[[16](https://arxiv.org/html/2608.14585#bib.bib16)\], which serves as the LLM component of Euclid\-Omni\. Since benchmark diagrams may include non\-geometric objects such as buildings, trees, or tables, we follow prior work\[[39](https://arxiv.org/html/2608.14585#bib.bib39),[17](https://arxiv.org/html/2608.14585#bib.bib17)\]and augment with 10K examples randomly sampled from Geo170K\[[21](https://arxiv.org/html/2608.14585#bib.bib21)\]to better match the benchmark distribution\. We fine\-tune Qwen2\.5\-VL\[[2](https://arxiv.org/html/2608.14585#bib.bib2)\]on the combined 20K examples for 3 epochs on 8×\\timesH100 GPUs using LLaMA\-Factory\[[66](https://arxiv.org/html/2608.14585#bib.bib66)\]\. We compare against G\-LLaVA\[[21](https://arxiv.org/html/2608.14585#bib.bib21)\], MAVIS\[[61](https://arxiv.org/html/2608.14585#bib.bib61)\], Qwen2\.5\-VL\[[2](https://arxiv.org/html/2608.14585#bib.bib2)\], and recent Qwen2\.5\-VL\-based methods \(GeoGen\[[39](https://arxiv.org/html/2608.14585#bib.bib39)\], TR\-COT\[[17](https://arxiv.org/html/2608.14585#bib.bib17)\], NeSyGeo\[[49](https://arxiv.org/html/2608.14585#bib.bib49)\]\), all of which are trained via supervised fine\-tuning on synthesized data\. We evaluate on four benchmarks: GeoQA\[[6](https://arxiv.org/html/2608.14585#bib.bib6)\], Geometry3K\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\], and the plane\-geometry subsets of MathVista \(testmini\)\[[31](https://arxiv.org/html/2608.14585#bib.bib31)\]and MathVerse \(vision\-intensive\)\[[60](https://arxiv.org/html/2608.14585#bib.bib60)\], reporting multiple\-choice accuracy when options are provided and exact match to the ground\-truth value otherwise\.

Table 2:Accuracy \(%\) of VLMs on four calculation benchmarks\. –: not reported in prior work\.Model\#TrainGeoQAGeometry3KMathVistaMathVersePrior VLM baselinesG\-LLaVA\-7B117K64\.2–53\.4–MAVIS\-7B834K––64\.127\.9Qwen2\.5\-VL variantsQwen2\.5\-VL\-7B–69\.456\.472\.244\.1\+ NeSyGeo100K71\.8––46\.7\+ GeoGen224K77\.658\.474\.0–\+ TR\-COT183K79\.2–74\.5–\+ Ours20K76\.661\.074\.751\.0Results\.Table[2](https://arxiv.org/html/2608.14585#S4.T2)shows that our model achieves state\-of\-the\-art accuracy on three of the four datasets, improves over the base model by 5\.3% on average, and remains competitive on GeoQA—all with orders of magnitude less training data than prior methods\. Since our rendered diagrams differ substantially from those in the evaluation benchmarks, this also underscores the generalization enabled by our synthetic data\. Section[4\.4](https://arxiv.org/html/2608.14585#S4.SS4)analyzes the synthetic dataset, Appendix[C\.2](https://arxiv.org/html/2608.14585#A3.SS2)ablates the training mix, and Appendix[C\.3](https://arxiv.org/html/2608.14585#A3.SS3)provides qualitative comparisons against the base model\.

### 4\.3Symbolic Olympiad\-level Proving Problems

Setup\.We synthesize 100K training problems that require auxiliary constructions and fine\-tune Qwen2\.5\-Math\-7B\[[55](https://arxiv.org/html/2608.14585#bib.bib55)\]for one epoch on 8×\\timesH100 GPUs with LLaMA\-Factory\[[66](https://arxiv.org/html/2608.14585#bib.bib66)\]\. At inference time, we use beam search to propose auxiliary constructions: candidates are ranked by log probability, and the search is progressively expanded whenever the solver fails to reach the target goal\. We set the branching factor to 32, the beam size to 128, and the maximum depth to 4\. As baselines, we include AlphaGeometry\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]and two prompted proprietary models, GPT\-4o and Gemini 2\.5 Flash, chosen for strong reasoning performance and favorable cost under the high query volume induced by beam search; both are prompted with the formal semantics of DD\+AR\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]and Euclidea to generate auxiliary constructions\. We evaluate on JGEX\-AG\-231\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]and IMO\-AG\-30\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]with a 90\-minute timeout per problem, matching the standard IMO duration\.

Table 3:Solved problems by neuro\-symbolic systems on two proving benchmarks\. –: model/result is not released/reported\.EngineModel\#TrainJGEX\-AG\-231IMO\-AG\-30DD\+ARGPT\-4o–21317Gemini 2\.5 Flash–21617AlphaGeometry100M22825AlphaGeometry20M–21EuclideaGPT\-4o–21317Gemini 2\.5 Flash–21317Ours100K22322Results\.Prompting proprietary models yields only modest gains and typically solves easier instances that require at most one auxiliary construction\. In contrast, our hybrid system solves 223 problems on JGEX\-AG\-231 and 22 on IMO\-AG\-30—competitive with AlphaGeometry trained on 100M problems and exceeding the 20M variant, despite using only 100K samples, highlighting both the computational efficiency and the data effectiveness of our approach\. Beyond aggregate counts, our solver frequently discovers auxiliary constructions that differ from AlphaGeometry’s and often reaches a proof in fewer reasoning steps \(Appendix[C\.4](https://arxiv.org/html/2608.14585#A3.SS4)\)\.

### 4\.4Synthetic Data

Setup\.To assess the quality of the data generated by Euclid\-Omni, we compare our natural\-language calculation dataset against Geo170K\[[21](https://arxiv.org/html/2608.14585#bib.bib21)\], GeoGen\[[39](https://arxiv.org/html/2608.14585#bib.bib39)\], and TR\-CoT\[[17](https://arxiv.org/html/2608.14585#bib.bib17)\]along three axes\. For*correctness*, we sample 1K problems and prompt Gemini 2\.5 Flash to solve them from the natural\-language statements and diagrams, reporting answer accuracy\. For*difficulty*, we use solution token length as a proxy for the length of multi\-step reasoning chains\. For*diversity*, we embed question texts and visualize their distribution with t\-SNE on 5K random examples from each dataset\.

Results\.

Table 4:Solution length statistics across four synthetic datasets\.Geo170KGeoGenTR\-CoTOursAverage109\.3210\.386\.9247\.5Median103\.0177\.078\.0230\.0Gemini 2\.5 Flash solves only 69\.6% of the 1K sampled problems, suggesting that purely VLM\-generated solutions contain a substantial fraction of errors\. In contrast, when Euclidea provides the symbolic solution and Gemini 2\.5 Flash is used only for translation, all instances remain consistent with the ground truth, underscoring the importance of Euclidea for correctness in the Euclid\-Omni pipeline\.

Table[4](https://arxiv.org/html/2608.14585#S4.T4)shows that our dataset has the largest average and median solution lengths, indicating more challenging instances that require longer, multi\-step reasoning\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/tsne_geogen.png)\(a\)GeoGen
![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/tsne_rcot.png)\(b\)TR\-CoT
![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/tsne_ours.png)\(c\)Ours

Figure 3:t\-SNE visualization of question\-text embeddings across three synthetic datasets\.Figure[3](https://arxiv.org/html/2608.14585#S4.F3)further shows that our data is more uniformly distributed in the text\-embedding space, while other datasets exhibit denser clusters of similar or repetitive samples\. Qualitatively, Euclid\-Omni also covers a broader set of goal types—angles, lengths, areas, and variable\-bound quantities—mirroring real benchmarks, whereas prior pipelines rarely generate area\-based or variable\-binding goals\.

## 5Limitations and Future Work

More Expressive and Human\-Like Euclidea\.Although the current design of Euclidea aims to mimic human reasoning and produce human\-interpretable solutions, the resulting proofs can be lengthy, particularly for Olympiad\-level problems, and differ from those written by IMO contestants\. A natural extension is to enrich the deductive database with more sophisticated rules \(e\.g\., well\-known theorems\) such as Menelaus’ or Desargues’ theorem\. This could yield more compact proofs and expand the range of solvable problems\. Another direction is to enhance the algebraic system by incorporating projective or inversive geometry, thereby increasing expressivity\. Finally, since many primitives of LeanEuclid\[[37](https://arxiv.org/html/2608.14585#bib.bib37)\]are already included in Euclidea, a compelling avenue is to ground its representations in Lean\[[36](https://arxiv.org/html/2608.14585#bib.bib36)\]\. This would allow Euclidea to function as an automatic tactic and integrate with existing libraries\[[34](https://arxiv.org/html/2608.14585#bib.bib34),[44](https://arxiv.org/html/2608.14585#bib.bib44)\], bridging automated geometry solvers with general\-purpose proof assistants\.

Better Design and Broader Usage of Euclid\-Omni\.Currently, construction rules in Euclid\-Omni are sampled uniformly, without leveraging human priors or empirical distributions observed in existing problems\. Future work could incorporate statistics from existing problems\[[57](https://arxiv.org/html/2608.14585#bib.bib57)\]or exploit structural priors such as symmetries to better align generated problems with specific target tasks\. In addition, while current Euclid\-Omni trains LLMs and VLMs via supervised finetuning, there is significant potential to explore reinforcement learning, using Euclidea to provide verifiable rewards\. Beyond the tasks studied here, Euclid\-Omni has broader potential applications: it could support autoformalization and problem solving to produce verifiable solutions from natural\-language descriptions \(useful for pedagogy\) or serve as a pretraining resource for VLMs to improve vision–language alignment and diagram understanding\.

## Broader Impact

This paper presents work whose goal is to advance machine learning for geometric reasoning\. We expect its broader impact to be positive, and we do not anticipate societal risks beyond common concerns such as misuse or overreliance\.

## References

- Avigad et al\. \[2009\]J\. Avigad, E\. Dean, and J\. Mumma\.A formal system for euclid’s elements\.*The Review of Symbolic Logic*, 2\(4\):700–768, 2009\.
- Bai et al\. \[2025\]S\. Bai, K\. Chen, X\. Liu, J\. Wang, W\. Ge, S\. Song, K\. Dang, P\. Wang, S\. Wang, J\. Tang, et al\.Qwen2\. 5\-vl technical report\.*arXiv preprint arXiv:2502\.13923*, 2025\.
- Cai et al\. \[2024\]S\. Cai, K\. Bao, H\. Guo, J\. Zhang, J\. Song, and B\. Zheng\.Geogpt4v: Towards geometric multi\-modal large language models with geometric image generation\.*arXiv preprint arXiv:2406\.11503*, 2024\.
- Cao and Xiao \[2022\]J\. Cao and J\. Xiao\.An augmented benchmark dataset for geometric question answering through dual parallel text encoding\.In*Proceedings of the 29th international conference on computational linguistics*, pages 1511–1520, 2022\.
- Chen et al\. \[2021a\]J\. Chen, J\. Tang, J\. Qin, X\. Liang, L\. Liu, E\. P\. Xing, and L\. Lin\.Geoqa: A geometric question answering benchmark towards multimodal numerical reasoning\.*arXiv preprint arXiv:2105\.14517*, 2021a\.
- Chen et al\. \[2021b\]J\. Chen, J\. Tang, J\. Qin, X\. Liang, L\. Liu, E\. P\. Xing, and L\. Lin\.Geoqa: A geometric question answering benchmark towards multimodal numerical reasoning\.*arXiv preprint arXiv:2105\.14517*, 2021b\.
- Chen et al\. \[2022\]J\. Chen, T\. Li, J\. Qin, P\. Lu, L\. Lin, C\. Chen, and X\. Liang\.Unigeo: Unifying geometry logical reasoning via reformulating mathematical expression\.*arXiv preprint arXiv:2212\.02746*, 2022\.
- Chen et al\. \[2025a\]L\. Chen, J\. Gu, L\. Huang, W\. Huang, Z\. Jiang, A\. Jie, X\. Jin, X\. Jin, C\. Li, K\. Ma, et al\.Seed\-Prover: Deep and broad reasoning for automated theorem proving\.*arXiv preprint arXiv:2507\.23726*, 2025a\.
- Chen et al\. \[2025b\]S\. Chen, R\. Zhang, and X\. Zhang\.Geoilp: A synthetic dataset to guide large\-scale rule induction\.In*The Thirteenth International Conference on Learning Representations*, 2025b\.
- Cheng et al\. \[2025\]J\.\-K\. Cheng, Z\. Zhang, R\. Chen, J\. Deng, Z\. Qin, and J\. Ma\.Geouni: A unified model for generating geometry diagrams, problems and problem solutions\.*arXiv preprint arXiv:2504\.10146*, 2025\.
- Chervonyi et al\. \[2025\]Y\. Chervonyi, T\. H\. Trinh, M\. Olšák, X\. Yang, H\. Nguyen, M\. Menegali, J\. Jung, V\. Verma, Q\. V\. Le, and T\. Luong\.Gold\-medalist performance in solving olympiad geometry with AlphaGeometry2\.*arXiv preprint arXiv:2502\.03544*, 2025\.
- Cho et al\. \[2025\]S\. Cho, Z\. Qin, Y\. Liu, Y\. Choi, S\. Lee, and D\. Kim\.Geodano: Geometric vlm with domain agnostic vision encoder\.*arXiv preprint arXiv:2502\.11360*, 2025\.
- Chou and Gao \[2001\]S\.\-C\. Chou and X\.\-S\. Gao\.Automated reasoning in geometry\.*Handbook of automated reasoning*, 1:707–749, 2001\.
- Chou et al\. \[1996\]S\.\-C\. Chou, X\.\-S\. Gao, and J\.\-Z\. Zhang\.Automated generation of readable proofs with geometric invariants: Ii\. theorem proving with full\-angles\.*Journal of Automated Reasoning*, 17\(3\):349–370, 1996\.
- Chou et al\. \[2000\]S\.\-C\. Chou, X\.\-S\. Gao, and J\.\-Z\. Zhang\.A deductive database approach to automated geometry theorem proving and discovering\.*Journal of Automated Reasoning*, 25\(3\):219–246, 2000\.
- Comanici et al\. \[2025\]G\. Comanici, E\. Bieber, M\. Schaekermann, I\. Pasupat, N\. Sachdeva, I\. Dhillon, M\. Blistein, O\. Ram, D\. Zhang, E\. Rosen, et al\.Gemini 2\.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities\.*arXiv preprint arXiv:2507\.06261*, 2025\.
- Deng et al\. \[2024\]L\. Deng, Y\. Liu, B\. Li, D\. Luo, L\. Wu, C\. Zhang, P\. Lyu, Z\. Zhang, G\. Zhang, E\. Ding, et al\.R\-cot: Reverse chain\-of\-thought problem generation for geometric reasoning in large multimodal models\.*arXiv preprint arXiv:2410\.17885*, 2024\.
- Duan et al\. \[2024\]X\. Duan, D\. Tan, L\. Fang, Y\. Zhou, C\. He, Z\. Chen, L\. Wu, G\. Chen, Z\. Gong, W\. Luo, et al\.Reason\-and\-execute prompting: Enhancing multi\-modal large language models for solving geometry questions\.In*Proceedings of the 32nd ACM International Conference on Multimedia*, pages 6959–6968, 2024\.
- Fu et al\. \[2025\]D\. Fu, Z\. Chen, R\. Xia, Q\. Liu, Y\. Feng, H\. Zhou, R\. Zhang, S\. Feng, P\. Gao, J\. Yan, et al\.Trustgeogen: Scalable and formal\-verified data engine for trustworthy multi\-modal geometric problem solving\.*arXiv preprint arXiv:2504\.15780*, 2025\.
- Gaffney et al\. \[2022\]K\. P\. Gaffney, M\. Prammer, L\. Brasfield, D\. R\. Hipp, D\. Kennedy, and J\. M\. Patel\.Sqlite: past, present, and future\.*Proceedings of the VLDB Endowment*, 15\(12\), 2022\.
- Gao et al\. \[2023\]J\. Gao, R\. Pi, J\. Zhang, J\. Ye, W\. Zhong, Y\. Wang, L\. Hong, J\. Han, H\. Xu, Z\. Li, et al\.G\-llava: Solving geometric problem with multi\-modal large language model\.*arXiv preprint arXiv:2312\.11370*, 2023\.
- Hao et al\. \[2022\]Y\. Hao, M\. Zhang, F\. Yin, and L\.\-L\. Huang\.Pgdp5k: A diagram parsing dataset for plane geometry problems\.In*2022 26th international conference on pattern recognition \(ICPR\)*, pages 1763–1769\. IEEE, 2022\.
- Huang et al\. \[2025\]Z\. Huang, T\. Wu, W\. Lin, S\. Zhang, J\. Chen, and F\. Wu\.Autogeo: Automating geometric image dataset creation for enhanced geometry understanding\.*IEEE Transactions on Multimedia*, 2025\.
- Hunter \[2007\]J\. D\. Hunter\.Matplotlib: A 2d graphics environment\.*Computing in science & engineering*, 9\(03\):90–95, 2007\.
- Kazemi et al\. \[2023\]M\. Kazemi, H\. Alvari, A\. Anand, J\. Wu, X\. Chen, and R\. Soricut\.Geomverse: A systematic evaluation of large models for geometric reasoning\.*arXiv preprint arXiv:2312\.12241*, 2023\.
- Kutzler and Stifter \[1986\]B\. Kutzler and S\. Stifter\.On the application of buchberger’s algorithm to automated geometry theorem proving\.*Journal of Symbolic Computation*, 2\(4\):389–397, 1986\.
- Li et al\. \[2024\]Z\. Li, Y\. Du, Y\. Liu, Y\. Zhang, Y\. Liu, M\. Zhang, and X\. Cai\.Eagle: Elevating geometric reasoning through llm\-empowered visual instruction tuning\.*arXiv preprint arXiv:2408\.11397*, 2024\.
- Li et al\. \[2025\]Z\. Li, H\. Bi, J\. Sun, Z\. Li, K\. Yang, and X\. Si\.PyEuclid: A versatile formal plane geometry system in Python\.In*International Conference on Computer Aided Verification \(CAV\)*, 2025\.
- Li et al\. \[2023\]Z\.\-Z\. Li, M\.\-L\. Zhang, F\. Yin, and C\.\-L\. Liu\.Lans: A layout\-aware neural solver for plane geometry problem\.*arXiv preprint arXiv:2311\.16476*, 2023\.
- Lu et al\. \[2021\]P\. Lu, R\. Gong, S\. Jiang, L\. Qiu, S\. Huang, X\. Liang, and S\.\-C\. Zhu\.Inter\-gps: Interpretable geometry problem solving with formal language and symbolic reasoning\.*arXiv preprint arXiv:2105\.04165*, 2021\.
- Lu et al\. \[2024\]P\. Lu, H\. Bansal, T\. Xia, J\. Liu, C\. Li, H\. Hajishirzi, H\. Cheng, K\.\-W\. Chang, M\. Galley, and J\. Gao\.MathVista: Evaluating mathematical reasoning of foundation models in visual contexts\.In*International Conference on Learning Representations \(ICLR\)*, 2024\.
- Ma et al\. \[2025\]J\. Ma, W\. Wang, and Q\. Jin\.A survey of deep learning for geometry problem solving\.*arXiv preprint arXiv:2507\.11936*, 2025\.
- Maher et al\. \[2016\]S\. Maher, M\. Miltenberger, J\. P\. Pedroso, D\. Rehfeldt, R\. Schwarz, and F\. Serrano\.Pyscipopt: Mathematical programming in python with the scip optimization suite\.In*International Congress on Mathematical Software*, pages 301–307\. Springer, 2016\.
- Mathlib community \[2020\]Mathlib community\.The Lean mathematical library\.In*Certified Programs and Proofs \(CPP\)*, 2020\.
- Meurer et al\. \[2017\]A\. Meurer, C\. P\. Smith, M\. Paprocki, O\. Čertík, S\. B\. Kirpichev, M\. Rocklin, A\. Kumar, S\. Ivanov, J\. K\. Moore, S\. Singh, et al\.Sympy: symbolic computing in python\.*PeerJ Computer Science*, 3:e103, 2017\.
- Moura and Ullrich \[2021\]L\. d\. Moura and S\. Ullrich\.The lean 4 theorem prover and programming language\.In*International Conference on Automated Deduction*, pages 625–635\. Springer, 2021\.
- Murphy et al\. \[2024\]L\. Murphy, K\. Yang, J\. Sun, Z\. Li, A\. Anandkumar, and X\. Si\.Autoformalizing euclidean geometry\.*arXiv preprint arXiv:2405\.17216*, 2024\.
- Ning et al\. \[2023\]M\. Ning, Q\.\-F\. Wang, K\. Huang, and X\. Huang\.A symbolic characters aware model for solving geometry problems\.In*Proceedings of the 31st ACM international conference on multimedia*, pages 7767–7775, 2023\.
- Pan et al\. \[2025\]Y\. Pan, Z\. Zhang, P\. Hu, J\. Ma, J\. Du, J\. Zhang, Q\. Liu, J\. Gao, and F\. Ma\.Enhancing the geometric problem\-solving ability of multimodal llms via symbolic\-neural integration\.*arXiv preprint arXiv:2504\.12773*, 2025\.
- Peng et al\. \[2023\]S\. Peng, D\. Fu, Y\. Liang, L\. Gao, and Z\. Tang\.Geodrl: A self\-learning framework for geometry problem solving using reinforcement learning in deductive reasoning\.In*Findings of the Association for Computational Linguistics: ACL 2023*, pages 13468–13480, 2023\.
- Ping et al\. \[2025\]B\. Ping, M\. Luo, Z\. Dang, C\. Wang, and C\. Jia\.Autogps: Automated geometry problem solving via multimodal formalization and deductive reasoning\.*arXiv preprint arXiv:2505\.23381*, 2025\.
- Qiao et al\. \[2024\]R\. Qiao, Q\. Tan, G\. Dong, M\. Wu, C\. Sun, X\. Song, Z\. GongQue, S\. Lei, Z\. Wei, M\. Zhang, et al\.We\-math: Does your large multimodal model achieve human\-like mathematical reasoning?*arXiv preprint arXiv:2407\.01284*, 2024\.
- Sicca et al\. \[2024\]V\. Sicca, T\. Xia, M\. Fédérico, P\. J\. Gorinski, S\. Frieder, and S\. Jui\.Newclid: A user\-friendly replacement for alphageometry\.*arXiv preprint arXiv:2411\.11938*, 2024\.
- Song et al\. \[2025\]C\. Song, Z\. Wang, F\. Pu, H\. Wang, X\. Lin, J\. Liu, J\. Li, and Z\. Liu\.Leangeo: Formalizing competitional geometry problems in lean\.*arXiv preprint arXiv:2508\.14644*, 2025\.
- Trinh et al\. \[2024\]T\. H\. Trinh, Y\. Wu, Q\. V\. Le, H\. He, and T\. Luong\.Solving olympiad geometry without human demonstrations\.*Nature*, 2024\.
- Wang et al\. \[2024\]K\. Wang, J\. Pan, W\. Shi, Z\. Lu, H\. Ren, A\. Zhou, M\. Zhan, and H\. Li\.Measuring multimodal mathematical reasoning with math\-vision dataset\.*Advances in Neural Information Processing Systems*, 37:95095–95169, 2024\.
- Wei et al\. \[2022\]J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, F\. Xia, E\. Chi, Q\. V\. Le, D\. Zhou, et al\.Chain\-of\-thought prompting elicits reasoning in large language models\.*Advances in neural information processing systems*, 35:24824–24837, 2022\.
- Wu et al\. \[2024\]W\. Wu, L\. Zhang, J\. Liu, X\. Tang, Y\. Wang, S\. Wang, and Q\. Wang\.E\-gps: Explainable geometry problem solving via top\-down solver and bottom\-up generator\.In*Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition*, pages 13828–13837, 2024\.
- Wu et al\. \[2025\]W\. Wu, Z\.\-k\. Wang, J\. Ye, Z\. Zhou, Y\.\-F\. Li, and L\.\-Z\. Guo\.Nesygeo: A neuro\-symbolic framework for multimodal geometric reasoning data generation\.*arXiv preprint arXiv:2505\.17121*, 2025\.
- Wu \[1986\]W\.\-T\. Wu\.Basic principles of mechanical theorem proving in elementary geometries\.*Journal of automated Reasoning*, 2:221–252, 1986\.
- Xia et al\. \[2024\]R\. Xia, M\. Li, H\. Ye, W\. Wu, H\. Zhou, J\. Yuan, T\. Peng, X\. Cai, X\. Yan, B\. Wang, et al\.Geox: Geometric problem solving through unified formalized vision\-language pre\-training\.*arXiv preprint arXiv:2412\.11863*, 2024\.
- Xiao et al\. \[2024\]T\. Xiao, J\. Liu, Z\. Huang, J\. Wu, J\. Sha, S\. Wang, and E\. Chen\.Learning to solve geometry problems via simulating human dual\-reasoning process\.*arXiv preprint arXiv:2405\.06232*, 2024\.
- Xu et al\. \[2025\]L\. Xu, Y\. Zhao, J\. Wang, Y\. Wang, B\. Pi, C\. Wang, M\. Zhang, J\. Gu, X\. Li, X\. Zhu, et al\.Geosense: Evaluating identification and application of geometric principles in multimodal reasoning\.*arXiv preprint arXiv:2504\.12597*, 2025\.
- Xu et al\. \[2024\]S\. Xu, Y\. Luo, and W\. Shi\.Geo\-llava: A large multi\-modal model for solving geometry math problems with meta in\-context learning\.In*Proceedings of the 2nd Workshop on Large Generative Models Meet Multimodal Applications*, pages 11–15, 2024\.
- Yang et al\. \[2024\]A\. Yang, B\. Zhang, B\. Hui, B\. Gao, B\. Yu, C\. Li, D\. Liu, J\. Tu, J\. Zhou, J\. Lin, et al\.Qwen2\. 5\-math technical report: Toward mathematical expert model via self\-improvement\.*arXiv preprint arXiv:2409\.12122*, 2024\.
- Ye et al\. \[2011\]Z\. Ye, S\.\-C\. Chou, and X\.\-S\. Gao\.An introduction to java geometry expert\.In*Automated Deduction in Geometry: 7th International Workshop, ADG 2008, Shanghai, China, September 22\-24, 2008\. Revised Papers 7*, pages 189–195\. Springer, 2011\.
- Zhang et al\. \[2024a\]C\. Zhang, J\. Song, S\. Li, Y\. Liang, Y\. Ma, W\. Wang, Y\. Zhu, and S\.\-C\. Zhu\.Proposing and solving olympiad geometry with guided tree search\.*arXiv preprint arXiv:2412\.10673*, 2024a\.
- Zhang et al\. \[2024b\]J\. Zhang, Z\. Li, M\. Zhang, F\. Yin, C\. Liu, and Y\. Moshfeghi\.Geoeval: benchmark for evaluating llms and multi\-modal models on geometry problem\-solving\.*arXiv preprint arXiv:2402\.10104*, 2024b\.
- Zhang et al\. \[2023a\]M\.\-L\. Zhang, F\. Yin, and C\.\-L\. Liu\.A multi\-modal neural geometric solver with textual clauses parsed from diagram\.*arXiv preprint arXiv:2302\.11097*, 2023a\.
- Zhang et al\. \[2024c\]R\. Zhang, D\. Jiang, Y\. Zhang, H\. Lin, Z\. Guo, P\. Qiu, A\. Zhou, P\. Lu, K\.\-W\. Chang, P\. Gao, et al\.MathVerse: Does your multi\-,odal LLM truly see the diagrams in visual math problems?In*European Conference on Computer Vision \(ECCV\)*, 2024c\.
- Zhang et al\. \[2024d\]R\. Zhang, X\. Wei, D\. Jiang, Y\. Zhang, Z\. Guo, C\. Tong, J\. Liu, A\. Zhou, B\. Wei, S\. Zhang, et al\.Mavis: Mathematical visual instruction tuning\.*arXiv e\-prints*, pages arXiv–2407, 2024d\.
- Zhang et al\. \[2023b\]X\. Zhang, N\. Zhu, Y\. He, J\. Zou, Q\. Huang, X\. Jin, Y\. Guo, C\. Mao, Y\. Li, Z\. Zhu, et al\.Formalgeo: An extensible formalized framework for olympiad geometric problem solving\.*arXiv preprint arXiv:2310\.18021*, 2023b\.
- Zhang et al\. \[2025\]Z\. Zhang, J\.\-K\. Cheng, J\. Deng, L\. Tian, J\. Ma, Z\. Qin, X\. Zhang, N\. Zhu, and T\. Leng\.Diagram formalization enhanced multi\-modal geometry problem solver\.In*ICASSP 2025\-2025 IEEE International Conference on Acoustics, Speech and Signal Processing \(ICASSP\)*, pages 1–5\. IEEE, 2025\.
- Zhao et al\. \[2025a\]J\. Zhao, T\. Zhang, J\. Sun, M\. Tian, and H\. Huang\.Pi\-gps: Enhancing geometry problem solving by unleashing the power of diagrammatic information\.*arXiv preprint arXiv:2503\.05543*, 2025a\.
- Zhao et al\. \[2025b\]Y\. Zhao, X\. Wang, J\. Liu, I\. King, and Z\. Huang\.Towards geometry problem solving in the large model era: A survey\.*arXiv preprint arXiv:2506\.02690*, 2025b\.
- Zheng et al\. \[2024\]Y\. Zheng, R\. Zhang, J\. Zhang, Y\. Ye, Z\. Luo, Z\. Feng, and Y\. Ma\.Llamafactory: Unified efficient fine\-tuning of 100\+ language models\.*arXiv preprint arXiv:2403\.13372*, 2024\.

## Appendix AEuclidea

### A\.1Problem Formalization

Following the established framework of geometric formalization introduced by E\[[1](https://arxiv.org/html/2608.14585#bib.bib1)\], all relations in Euclidea fall into two categories:*metric relations*and*diagrammatic relations*\. A metric relation is encoded either as a predicate proposition \(e\.g\.,Parallel\(x,a,b,c\)\) or as an equation \(e\.g\.,Angle\(a,x,b\)=π/3=\\pi/3\)\. A diagrammatic relation asserts certain topological configurations of the diagram, which are encoded as predicate propositions, such asBetween\(a,b,c\)andSameSide\(a,b,c,d\)\. These relations are directly extracted from the diagram and are typically not used as target goals in geometry problems\. Moreover, for certain relations such asCollinearandBetween, their negated forms can also be represented using theNotpredicate to assert that the corresponding property does not hold\.

Examples of metric relations include:

Collinear\(a,b,c\): pointsa,b, andcare collinear\.

Parallel\(a,b,c,d\): linesabandcdare parallel\.

Midpoint\(a,b,c\): pointais the midpoint of segmentbc\.

Perpendicular\(a,b,c,d\): linesabandcdare perpendicular\.

Congruent3\(a,b,c,d,e,f\): trianglesabcanddefare congruent\.

Similar3\(a,b,c,d,e,f\): trianglesabcanddefare similar\.

Examples of diagrammatic relations include:

Between\(a,b,c\): pointalies between pointsbandc\.

SameSide\(a,b,c,d\): pointsaandblie on the same side of linecd\.

Not\(Collinear\(a,b,c\)\): pointsa,b, andcare not collinear\.

OppositeSide\(a,b,c,d\): pointsaandblie on opposite sides of linecd\.

Note thatCollinearbelongs to metric relations, whereas its negated counterpartNot\(Collinear\)falls under diagrammatic relations\. This distinction arises because collinearity often needs to be formally proved, whereas non\-collinearity can typically be inferred directly from the diagram and thus is not treated as a goal in a geometry problem\.

It is also worth noting that a key feature of the formalization in Euclidea is its extensibility\. Fordiagrammatic relations, new predicates can be easily introduced to capture richer geometric semantics\. For instance, to indicate whether an angle is acute or obtuse, or whether one segment is longer than another, as inferred directly from the diagram\. Similarly, the set ofmetric relationsis extensible and can incorporate higher\-level or composite semantics derived from existing relations by specifying their correspondence with previously defined ones\. For example,

Square\(a,b,c,d\):=Rectangle\(a,b,c,d\)∧Length\(a,b\) = Length\(a,d\)\\texttt\{Square\(a,b,c,d\)\}:=\\texttt\{Rectangle\(a,b,c,d\)\}\\wedge\\texttt\{Length\(a,b\) = Length\(a,d\)\}Such high\-level relations can make the problem formalization more concise and streamline the reasoning steps based on higher\-level geometric properties\.

Compared with geometric formalization in existing IMO\-level systems\[[45](https://arxiv.org/html/2608.14585#bib.bib45),[11](https://arxiv.org/html/2608.14585#bib.bib11),[8](https://arxiv.org/html/2608.14585#bib.bib8)\], the key innovation of Euclidea lies in its integration of*diagrammatic relations*to support human\-like reasoning about angular and topological relationships\.

For humans, two angles are considered equal if and only if the underlying azimuths have the same cosine value\. Consider the inscribed angle theorem illustrated in Figure[4\(a\)](https://arxiv.org/html/2608.14585#A1.F4.sf1)\. If pointsA,B,C,Dlie on the same circle, thenAngle\(A,C,B\)is either equal or supplementary toAngle\(A,D,B\), depending on whetherAandDlie on the same side or on opposite sides of lineAB\.

Without diagrammatic relations, however, formal systems such as DD\+AR\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]cannot distinguish between these two scenarios\. Instead, they adopt the*full\-angle notation*\[[14](https://arxiv.org/html/2608.14585#bib.bib14)\], where two angles are treated as equal if and only if their azimuths have the same sine value\.

For instance, in Figure[4\(b\)](https://arxiv.org/html/2608.14585#A1.F4.sf2), under the conventional definition:

Angle\(A,O,C\)=Angle\(C,O,A\),Angle\(A,O,C\)\+Angle\(A,O,D\)=π\\texttt\{Angle\(A,O,C\)\}=\\texttt\{Angle\(C,O,A\)\},\\qquad\\texttt\{Angle\(A,O,C\)\}\+\\texttt\{Angle\(A,O,D\)\}=\\piHowever, in full\-angle notation:

Angle\(A,O,C\)=Angle\(A,O,D\),Angle\(A,O,C\)=−Angle\(C,O,A\)\\texttt\{Angle\(A,O,C\)\}=\\texttt\{Angle\(A,O,D\)\},\\qquad\\texttt\{Angle\(A,O,C\)\}=\-\\texttt\{Angle\(C,O,A\)\}This misalignment prevents faithful translation between natural language and formal language\. In theorem\-proving settings, the equality of two angles must therefore be expressed as “equal or supplementary,” rather than strictly equal\. The issue becomes even more pronounced in calculation\-oriented tasks, where such ambiguity prevents the unique determination of an angle’s value and can lead to inconsistent numerical results\. Consequently, it also hinders the formal system’s ability to perform complex algebraic computations, which inherently rely on precise angle representations\.

Moreover, diagrammatic inferences, as illustrated in Figure[4\(c\)](https://arxiv.org/html/2608.14585#A1.F4.sf3), are rarely made explicit in human geometric reasoning, except occasionally in formal logic\. Therefore, we extract them directly from the diagram as part of the initial conditions\. Integrating these inference rules into the deduction system would increase its complexity by introducing reasoning through contradiction and disjunction, and would also make proofs unnecessarily verbose and less aligned with human reasoning patterns\.

In contrast to the formal system E\[[1](https://arxiv.org/html/2608.14585#bib.bib1)\], which distinguishes three types of geometric objects—points, lines, and circles—Euclidea treats*points*as the only first\-class entities, assuming all points are implicitly connected\. For example, our assertion

is equivalent to the formal formulation in E\[[1](https://arxiv.org/html/2608.14585#bib.bib1)\]:

a,b,c: Point,l: Line,on\(a,l\),on\(b,l\),on\(c,l\)\\texttt\{a,b,c: Point\},\\quad\\texttt\{l: Line\},\\quad\\texttt\{on\(a,l\)\},\\;\\texttt\{on\(b,l\)\},\\;\\texttt\{on\(c,l\)\}
This simplification reduces the complexity of our rule\-based deduction system and avoids trivial auxiliary constructions such as “connect pointaand pointb\.”

![Refer to caption](https://arxiv.org/html/2608.14585v1/x3.png)\(a\)Inscribed angle theorem:Angle\(A,C,B\)is equal toAngle\(A,D1,B\), but supplementary toAngle\(A,D2,B\)\.
![Refer to caption](https://arxiv.org/html/2608.14585v1/x4.png)\(b\)Under the conventional definition of angles:Angle\(A,O,C\)=Angle\(C,O,A\)\\texttt\{Angle\(A,O,C\)\}=\\texttt\{Angle\(C,O,A\)\}, andAngle\(A,O,C\)is supplementary toAngle\(A,O,D\)\.
![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/pasch.png)\(c\)An example of diagrammatic inference fromAvigad et al\. \[[1](https://arxiv.org/html/2608.14585#bib.bib1)\]: ifbis betweenaandc, andaandcare on the same side of lineLL, thenaandbare on the same side ofLL\.

### A\.2Deductive Database

Given the current state, Euclidea stores all geometric entities \(i\.e\., points\) and predicates \(e\.g\.,Perpendicular,Collinear\) in an in\-memorySQLdatabase, where each predicate is represented as a relational table\. To efficiently manage algebraic dependencies, aunion\-finddata structure is used to maintain equivalence relationships among geometric quantities\. For example, if the system containsLength\(a,b\) = Length\(b,c\)andLength\(b,c\) = Length\(c,d\), it can automatically inferLength\(a,b\) = Length\(c,d\)\. All such equivalence relations, including those involving angles, angle sums, lengths, and length ratios, are first organized into equivalence classes within Euclidea and then synchronized with the correspondingSQLtables\. Under this design, a conjunction of conditions is naturally expressed as a series of table joins, allowing all applicable inference rules to be enumerated declaratively throughSQLqueries\.

For example, the condition definingMidpoint\(a,b,c\)can be expressed as:

Length\(a,b\) = Length\(a,c\)∧Collinear\(a,b,c\)∧Between\(a,b,c\),\\texttt\{Length\(a,b\) = Length\(a,c\) $\\wedge$ Collinear\(a,b,c\) $\\wedge$ Between\(a,b,c\)\},which can be translated into the followingSQLquery:

[⬇](data:text/plain;base64,U0VMRUNUIGEubmFtZSBBUyBhLCBiLm5hbWUgQVMgYiwgYy5uYW1lIEFTIGMKRlJPTSBwb2ludHMgYQpKT0lOIHBvaW50cyBiCkpPSU4gcG9pbnRzIGMKSk9JTiBsZW5ndGggcjBsCiAgT04gKChyMGwucDAgPSBhLm5hbWUgQU5EIHIwbC5wMSA9IGIubmFtZSkgT1IgKHIwbC5wMSA9IGEubmFtZSBBTkQgcjBsLnAwID0gYi5uYW1lKSkKSk9JTiBsZW5ndGggcjByCiAgT04gKChyMHIucDAgPSBhLm5hbWUgQU5EIHIwci5wMSA9IGMubmFtZSkgT1IgKHIwci5wMSA9IGEubmFtZSBBTkQgcjByLnAwID0gYy5uYW1lKSkKICBBTkQgcjBsLmNvbXBvbmVudCA9IHIwci5jb21wb25lbnQKSk9JTiBjb2xsaW5lYXIgcjEKICBPTiAoKGEubmFtZSA9IHIxLnAwIEFORCBiLm5hbWUgPSByMS5wMSBBTkQgYy5uYW1lID0gcjEucDIpCiAgICAgIE9SIChhLm5hbWUgPSByMS5wMCBBTkQgYy5uYW1lID0gcjEucDEgQU5EIGIubmFtZSA9IHIxLnAyKQogICAgICBPUiAoYi5uYW1lID0gcjEucDAgQU5EIGEubmFtZSA9IHIxLnAxIEFORCBjLm5hbWUgPSByMS5wMikKICAgICAgT1IgKGIubmFtZSA9IHIxLnAwIEFORCBjLm5hbWUgPSByMS5wMSBBTkQgYS5uYW1lID0gcjEucDIpCiAgICAgIE9SIChjLm5hbWUgPSByMS5wMCBBTkQgYS5uYW1lID0gcjEucDEgQU5EIGIubmFtZSA9IHIxLnAyKQogICAgICBPUiAoYy5uYW1lID0gcjEucDAgQU5EIGIubmFtZSA9IHIxLnAxIEFORCBhLm5hbWUgPSByMS5wMikpCkpPSU4gYmV0d2VlbiByMgogIE9OICgoYS5uYW1lID0gcjIucDAgQU5EIGIubmFtZSA9IHIyLnAxIEFORCBjLm5hbWUgPSByMi5wMikKICAgICAgT1IgKGEubmFtZSA9IHIyLnAwIEFORCBjLm5hbWUgPSByMi5wMSBBTkQgYi5uYW1lID0gcjIucDIpKQpXSEVSRSBiLm5hbWUgPCBjLm5hbWU7)SELECTa\.nameASa,b\.nameASb,c\.nameAScFROMpointsaJOINpointsbJOINpointscJOINlengthr0lON\(\(r0l\.p0=a\.nameANDr0l\.p1=b\.name\)OR\(r0l\.p1=a\.nameANDr0l\.p0=b\.name\)\)JOINlengthr0rON\(\(r0r\.p0=a\.nameANDr0r\.p1=c\.name\)OR\(r0r\.p1=a\.nameANDr0r\.p0=c\.name\)\)ANDr0l\.component=r0r\.componentJOINcollinearr1ON\(\(a\.name=r1\.p0ANDb\.name=r1\.p1ANDc\.name=r1\.p2\)OR\(a\.name=r1\.p0ANDc\.name=r1\.p1ANDb\.name=r1\.p2\)OR\(b\.name=r1\.p0ANDa\.name=r1\.p1ANDc\.name=r1\.p2\)OR\(b\.name=r1\.p0ANDc\.name=r1\.p1ANDa\.name=r1\.p2\)OR\(c\.name=r1\.p0ANDa\.name=r1\.p1ANDb\.name=r1\.p2\)OR\(c\.name=r1\.p0ANDb\.name=r1\.p1ANDa\.name=r1\.p2\)\)JOINbetweenr2ON\(\(a\.name=r2\.p0ANDb\.name=r2\.p1ANDc\.name=r2\.p2\)OR\(a\.name=r2\.p0ANDc\.name=r2\.p1ANDb\.name=r2\.p2\)\)WHEREb\.name<c\.name;

Note that we impose a lexical partial order on variable names to eliminate redundant permutations\. For instance,Midpoint\(a,b,c\)andMidpoint\(a,c,b\)describe the same configuration; therefore, the constraintb\.name < c\.nameensures that only one canonical ordering is retained\.

### A\.3Algebraic System

At each iteration, Euclidea first uses Gaussian elimination to solve three types of equations: \(i\) linear equations of angles, \(ii\) linear equations of lengths, and \(iii\) log\-linear equations of lengths\. The results from these systems are then combined to solve \(iv\) other nonlinear equations\.

Examples of linear equations of angles include:

Angle\(d,a,c\) =π\\pi/6

Angle\(a,b,c\) \+ Angle\(a,c,b\) \+ Angle\(b,a,c\) =π\\pi

Angle\(a,b,c\) = 2×\\timesAngle\(a,c,b\)

Examples of linear equations of lengths include:

Length\(a,b\) = 3

Length\(a,m\) \+ Length\(b,m\) = Length\(a,b\)

Length\(a,m\) = 2×\\timesLength\(b,m\)

Examples of log\-linear equations of lengths include:

Length\(a,b\) = 3

Length\(a,m\) = 2×\\timesLength\(b,m\)

Length\(a,m\)/Length\(b,m\) = Length\(a,n\)/Length\(c,n\)

Area\(a,b,c\) = Length\(a,b\)×\\timesLength\(a,c\)/2

Examples of non\-linear equations include:

Length\(a,b\)2\+ Length\(a,c\)2= Length\(b,c\)2

Length\(a,b\) = Length\(b,c\)×\\timescos\(Angle\(a,b,c\)\)

Area\(a,b,c,d\) = Length\(a,b\)×\\timesLength\(b,c\)×\\timessin\(Angle\(a,b,c\)\)

Although the linear and log\-linear equations of lengths involve the same set of variables and could theoretically be solved together, doing so easily leads to high\-order polynomials, making symbolic solutions intractable\. To avoid this, Euclidea solves the three \(log\-\)linear systems independently and then substitutes their solutions into all remaining non\-linear equations, including those involving trigonometric or higher\-order polynomials\.

If the resulting equation only involves a single variable, the corresponding geometric quantity has been determined\. If the equation becomes \(log\-\)linear after substitution, it is reintroduced into the appropriate subsystem\. This mechanism enables constraint propagation among the three \(log\-\)linear systems without requiring the entire nonlinear system to be solved simultaneously\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/x5.png)Figure 5:An example diagram of rectangleABCD\.As a concrete example, consider Figure[5](https://arxiv.org/html/2608.14585#A1.F5), where the rectangleABCDis defined with the following conditions:

AD \+ AB=7,AD \- AB=1\.\\texttt\{AD \+ AB\}=7,\\quad\\texttt\{AD \- AB\}=1\.Together with the properties of a rectangle, the set of linear equations of lengths can be represented as the following matrix equation:

\(1100−1100100−101−10\)​\(ABADBCCD\)=\(7100\)\\begin\{pmatrix\}1&1&0&0\\\\ \-1&1&0&0\\\\ 1&0&0&\-1\\\\ 0&1&\-1&0\\end\{pmatrix\}\\begin\{pmatrix\}\\texttt\{AB\}\\\\ \\texttt\{AD\}\\\\ \\texttt\{BC\}\\\\ \\texttt\{CD\}\\end\{pmatrix\}=\\begin\{pmatrix\}7\\\\ 1\\\\ 0\\\\ 0\\end\{pmatrix\}
First, Gaussian elimination is applied to the system of linear equations to findAB=3\\texttt\{AB\}=3andBC=4\\texttt\{BC\}=4\. Using the Pythagorean theorem, we have

AC2=AB2\+BC2\\texttt\{AC\}^\{2\}=\\texttt\{AB\}^\{2\}\+\\texttt\{BC\}^\{2\}Substituting the solutions from the linear system, we obtain

After post\-processing the solution and eliminating negative values for lengths, we obtainAC=5\\texttt\{AC\}=5\. Since the equationAC=5\\texttt\{AC\}=5satisfies both the linear and log\-linear forms of length equations, it is added back to both systems for potential use in subsequent iterations\.

### A\.4Solution Generation

For each relation inferred in the deductive database, Euclidea records its inference rule and conditions as the source\. For instance, consider the SAS \(Side–Angle–Side\) congruence rule for triangles:

SAS\(a,b,c,d,e,f\): Not\(Collinear\(a,b,c\)\)∧\\land Length\(a,b\) = Length\(d,e\)∧\\landAngle\(a,b,c\) = Angle\(d,e,f\)∧\\land Length\(b,c\) = Length\(e,f\)⇒\\RightarrowCongruent3\(a,b,c,d,e,f\)

If the relationCongruent3\(a,b,c,d,e,f\)is inferred via this rule, its source is the SAS rule, as well as its conditionsNot\(Collinear\(a,b,c\)\),Length\(a,b\) = Length\(d,e\),Angle\(a,b,c\) = Angle\(d,e,f\), andLength\(b,c\) = Length\(e,f\)\.

For the equations inferred from the algebraic system, we adopt different dependency\-tracing strategies, since \(log\-\)linear equations are solved using Gaussian elimination, whereas nonlinear equations are solved through substitution and symbolic solving\.

Continuing the example in Figure[5](https://arxiv.org/html/2608.14585#A1.F5), supposeAC = 5is the target goal\. Since it results from substitutingAB = 3andBC = 4intoAC2= AB2\+ BC2, the source ofAC = 5includes these three equations\. Next, the system recursively traces the dependencies ofAB = 3andBC = 4\.

To identify the source ofAB = 3, we introduce a coefficient vector𝐳=\(z1,z2,z3,z4\)⊤\\mathbf\{z\}=\(z\_\{1\},z\_\{2\},z\_\{3\},z\_\{4\}\)^\{\\top\}, whereziz\_\{i\}represents the weight assigned to theii\-th equation that contributes to the query equationAB = 3\. We then solve the following optimization problem \(using theℓ0\\ell\_\{0\}\-norm\):

min𝐳⁡‖𝐳‖0s\.t\.\(ABADBCCDconst11007−11001100−1001−100\)⊤​\(z1z2z3z4\)=\(10003\),\\min\_\{\\mathbf\{z\}\}\\;\\\|\\mathbf\{z\}\\\|\_\{0\}\\quad\\text\{s\.t\.\}\\quad\\begin\{pmatrix\}\\texttt\{AB\}&\\texttt\{AD\}&\\texttt\{BC\}&\\texttt\{CD\}&\\texttt\{const\}\\\\ 1&1&0&0&7\\\\ \-1&1&0&0&1\\\\ 1&0&0&\-1&0\\\\ 0&1&\-1&0&0\\end\{pmatrix\}^\{\\top\}\\begin\{pmatrix\}z\_\{1\}\\\\ z\_\{2\}\\\\ z\_\{3\}\\\\ z\_\{4\}\\end\{pmatrix\}=\\begin\{pmatrix\}1\\\\ 0\\\\ 0\\\\ 0\\\\ 3\\end\{pmatrix\},where the right\-hand vector\(1,0,0,0,3\)⊤\(1,\\,0,\\,0,\\,0,\\,3\)^\{\\top\}encodes the query coefficients corresponding to the equationAB = 3\. Solving yieldsz1=0\.5z\_\{1\}=0\.5,z2=−0\.5z\_\{2\}=\-0\.5, andz3=z4=0z\_\{3\}=z\_\{4\}=0, indicating thatAB = 3depends on the two equationsAD \+ AB = 7andAD \- AB = 1\. A similar process can be applied to identify the source equations forBC = 4\.

Note that theℓ0\\ell\_\{0\}\-norm formulation yields the minimal number of source equations but can be computationally expensive, whereas theℓ1\\ell\_\{1\}\-norm provides an efficient approximation that minimizes the total weights but does not always guarantee minimal sparsity\. In practice, Euclidea can adaptively choose between theℓ0\\ell\_\{0\}andℓ1\\ell\_\{1\}formulations depending on system complexity and user requirements\.

We perform this backtracking process starting from the target goal of the problem and continue until all traced relations and equations are reduced to the initial conditions\. A dependency graph is then constructed, with the goal as the root, the initial conditions as the leaves, and intermediate relations as internal nodes\. A post\-order traversal of this graph produces the sequential proof steps\.

To make the proofs more human\-like and concise, Euclidea merges steps that share common conditions or exhibit hierarchical relationships \(e\.g\., the properties of a square subsume those of a rectangle\)\. Furthermore, certain diagrammatic relations are omitted from the conditions of proof steps, as they are typically trivial and rarely stated explicitly in human\-written proofs\.

## Appendix BEuclid\-Omni

### B\.1Problem Synthesis

To synthesize a geometry problem, Euclid\-Omni first samples a sequence of construction rules and then samples a corresponding diagram consistent with these rules\. For calculation problems, parameterized construction rules are used so that the resulting diagram is fully determined by its parameters, up to global translation, rotation, and reflection\. In contrast, for proving problems, the framework also employs construction rules with unspecified degrees of freedom, since the target theorem typically holds across a family of diagrams rather than a single instance\.

Consider the constructions illustrated in Figures[6\(a\)](https://arxiv.org/html/2608.14585#A2.F6.sf1)and[6\(b\)](https://arxiv.org/html/2608.14585#A2.F6.sf2):

a,b,c = construct\_triangle\(\);x = construct\_foot\(a,b,c\)To sample a diagram, the coordinates of all points are drawn according to the specified construction rules\. Certain conclusions hold for all diagrams generated from these constructions, yielding invariant relations such asPerpendicular\(x,a,b,c\)\. In contrast, diagrammatic relations depend on the specific sampled diagram and can be directly extracted from it\. For example,Between\(x,b,c\)andOppositeSide\(b,c,a,x\)in Figure[6\(a\)](https://arxiv.org/html/2608.14585#A2.F6.sf1)\. Even with the same construction rules, different diagram samples may yield distinct diagrammatic relations\. For instance, ifAngle\(a,b,c\)\>π/2\\texttt\{Angle\(a,b,c\)\}\>\\pi/2, the resulting diagram instead satisfiesBetween\(b,x,c\)andSameSide\(b,c,a,x\), as shown in Figure[6\(b\)](https://arxiv.org/html/2608.14585#A2.F6.sf2)\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/x6.png)\(a\)A sampled figure with diagrammatic relationsBetween\(x,b,c\)andOppositeSide\(b,c,a,x\)\.
![Refer to caption](https://arxiv.org/html/2608.14585v1/x7.png)\(b\)An alternative configuration withBetween\(b,x,c\)andSameSide\(b,c,a,x\)\.

### B\.2Examples of Templates and Prompts for Natural Language Translation

Following prior work\[[23](https://arxiv.org/html/2608.14585#bib.bib23)\], we construct multiple natural language templates for each construction rule \(in the problem\) and relation \(in the solution\) within our formalization\. When converting a formal expression into natural language, one template is randomly sampled and instantiated to generate the corresponding textual description\. For instance, the construction rulex = construct\_circumcenter\(a,b,c\)can be verbalized as:

[⬇](data:text/plain;base64,eCBpcyB0aGUgY2lyY3VtY2VudGVyIG9mIGFiYwp4IGlzIHRoZSBjZW50ZXIgb2YgdGhlIGNpcmNsZSBwYXNzaW5nIHRocm91Z2ggYSwgYiwgYW5kIGMKdGhlIGNlbnRlciBvZiB0aGUgY2lyY2xlIHRocm91Z2ggcG9pbnRzIGEsIGIsIGFuZCBjIGlzIHgKdGhlIHBvaW50IHggaXMgdGhlIGNpcmN1bWNlbnRlciBvZiB0cmlhbmdsZSBhYmM=)xisthecircumcenterofabcxisthecenterofthecirclepassingthrougha,b,andcthecenterofthecirclethroughpointsa,b,andcisxthepointxisthecircumcenteroftriangleabc

Similarly, each relation can also be expressed through multiple templates\. For example, the relationPerpendicular\(a,b,c,d\)can be instantiated as:

[⬇](data:text/plain;base64,bGluZSBhYiBpcyBwZXJwZW5kaWN1bGFyIHRvIGxpbmUgY2QKbGluZSBhYiDin4IgbGluZSBjZApsaW5lIHRocm91Z2ggYSBhbmQgYiBpcyBwZXJwZW5kaWN1bGFyIHRvIHRoZSBsaW5lIHRocm91Z2ggYyBhbmQgZAp0aGUgbGluZXMgZm9ybWVkIGJ5IChhLCBiKSBhbmQgKGMsIGQpIGFyZSBwZXJwZW5kaWN1bGFy)lineabisperpendiculartolinecdlineab⟂\\perplinecdlinethroughaandbisperpendiculartothelinethroughcanddthelinesformedby\(a,b\)and\(c,d\)areperpendicular

To refine the problem statement with an LLM, we employ a dedicated prompt that converts the template\-based problem and its goal into fluent text\. The prompt is defined as follows:

[⬇](data:text/plain;base64,WW91IGFyZSBnaXZlbiBhIHBsYW5lIGdlb21ldHJ5IHByb2JsZW06CgpQcm9ibGVtOiA8dGVtcGxhdGUtYmFzZWQgcHJvYmxlbT4uIERldGVybWluZSA8dGVtcGxhdGUtYmFzZWQgZ29hbD4uCgpUYXNrOgotIFJld3JpdGUgdGhlIHByb2JsZW0gaW4gY2xlYXIsIGNvbmNpc2UsIGFuZCBmbHVlbnQgbGFuZ3VhZ2UsIHByZXNlcnZpbmcgdGhlIG9yaWdpbmFsIG1lYW5pbmcuCi0gT3V0cHV0IE9OTFkgdGhlIHJld3JpdHRlbiBwcm9ibGVtLCB3aXRoIG5vIGV4cGxhbmF0aW9ucyBvciBleHRyYSB0ZXh0Lg==)Youaregivenaplanegeometryproblem:Problem:<template\-basedproblem\>\.Determine<template\-basedgoal\>\.Task:\-Rewritetheprobleminclear,concise,andfluentlanguage,preservingtheoriginalmeaning\.\-OutputONLYtherewrittenproblem,withnoexplanationsorextratext\.

Once the refined problem is generated, we employ a separate prompt to rewrite the template\-based solution in fluent natural language:

[⬇](data:text/plain;base64,WW91IGFyZSBnaXZlbiBhIHBsYW5lIGdlb21ldHJ5IHByb2JsZW0gYW5kIGl0cyBjb3JyZXNwb25kaW5nIHNvbHV0aW9uOgoKUHJvYmxlbToKPHJlZmluZWQgcHJvYmxlbT4KClNvbHV0aW9uOgo8dGVtcGxhdGUtYmFzZWQgc29sdXRpb24+CgpUYXNrOgotIFJld3JpdGUgdGhlIHNvbHV0aW9uIGluIGNsZWFyLCBjb25jaXNlLCBhbmQgZmx1ZW50IGxhbmd1YWdlLCBzaW1wbGlmeWluZyB0cml2aWFsIG9yIHJlZHVuZGFudCBzdGVwcy4KLSBTdGVwLXdpc2UgZm9ybWF0dGluZyBpcyBvcHRpb25hbC4gVXNlIGl0IG9ubHkgd2hlbiBpdCBpbXByb3ZlcyBjbGFyaXR5OyBvdGhlcndpc2UsIHByZXNlbnRpbmcgdGhlIHNvbHV0aW9uIGFzIGEgY29udGludW91cyBwYXJhZ3JhcGggaXMgYWNjZXB0YWJsZS4KLSBPdXRwdXQgT05MWSB0aGUgcmV3cml0dGVuIHNvbHV0aW9uLCB3aXRoIHRoZSBmaW5hbCBhbnN3ZXIgaW5zaWRlIFxib3hlZHt9IGF0IHRoZSBlbmQuCi0gRG8gTk9UIGluY2x1ZGUgdGhlIHByb2JsZW0gc3RhdGVtZW50LCBleHBsYW5hdGlvbnMsIG9yIGV4dHJhIHRleHQu)Youaregivenaplanegeometryproblemanditscorrespondingsolution:Problem:<refinedproblem\>Solution:<template\-basedsolution\>Task:\-Rewritethesolutioninclear,concise,andfluentlanguage,simplifyingtrivialorredundantsteps\.\-Step\-wiseformattingisoptional\.Useitonlywhenitimprovesclarity;otherwise,presentingthesolutionasacontinuousparagraphisacceptable\.\-OutputONLYtherewrittensolution,withthefinalanswerinside\\boxed\{\}attheend\.\-DoNOTincludetheproblemstatement,explanations,orextratext\.

We also support converting formal problems and their corresponding solutions into multiple\-choice formats, as commonly used in calculation\-style geometry datasets\[[6](https://arxiv.org/html/2608.14585#bib.bib6),[21](https://arxiv.org/html/2608.14585#bib.bib21),[31](https://arxiv.org/html/2608.14585#bib.bib31),[60](https://arxiv.org/html/2608.14585#bib.bib60)\]\. The prompt for this setting is defined as follows:

[⬇](data:text/plain;base64,WW91IGFyZSBnaXZlbiBhIHBsYW5lIGdlb21ldHJ5IHByb2JsZW0gYW5kIGl0cyBjb3JyZXNwb25kaW5nIHNvbHV0aW9uOgoKUHJvYmxlbTogPHRlbXBsYXRlLWJhc2VkIHByb2JsZW0+LiA8dGVtcGxhdGUtYmFzZWQgZ29hbD4gPSAoICkuCgpSZWZlcmVuY2UgQW5zd2VyIChmb3IgY29ycmVjdG5lc3Mgb25seSk6CjxhbnN3ZXI+CgpUYXNrOgotIFJld3JpdGUgdGhlIHByb2JsZW0gaW4gY2xlYXIsIGNvbmNpc2UsIGFuZCBmbHVlbnQgbGFuZ3VhZ2UsIHByZXNlcnZpbmcgdGhlIG9yaWdpbmFsIG1lYW5pbmcuCi0gQ29udmVydCB0aGUgdGFzayBpbnRvIGEgbXVsdGlwbGUtY2hvaWNlIHF1ZXN0aW9uIHdpdGggZXhhY3RseSA0IG9wdGlvbnMgbGFiZWxlZCBBLEIsQyxELgotIFVzZSB0aGUgcmVmZXJlbmNlIHNvbHV0aW9uIE9OTFkgdG8gZGV0ZXJtaW5lIHRoZSBjb3JyZWN0IG51bWVyaWMvY2hvaWNlIGFuc3dlci4KLSBDcmVhdGUgcGxhdXNpYmxlIGRpc3RyYWN0b3JzIG9mIGNvbXBhcmFibGUgc2NhbGUgb3IgbWFnbml0dWRlIHRvIHRoZSBjb3JyZWN0IGFuc3dlci4KLSBFbnN1cmUgRVhBQ1RMWSBPTkUgb3B0aW9uIGlzIGNvcnJlY3QuCi0gT3V0cHV0IE9OTFkgdGhlIHJld3JpdHRlbiBwcm9ibGVtIGZvbGxvd2VkIGJ5IHRoZSBjaG9pY2VzLCB3aXRoIG5vIGV4cGxhbmF0aW9ucyBvciBleHRyYSB0ZXh0LgotIERvIE5PVCBpbmNsdWRlIHRoZSBzb2x1dGlvbiwgcmF0aW9uYWxlcywgb3IgZXh0cmEgdGV4dC4KCk91dHB1dCBmb3JtYXQ6CjxSZXdyaXR0ZW4gcHJvYmxlbSBzdGF0ZW1lbnQ+CgpDaG9pY2VzOgpBOiAuLi4KQjogLi4uCkM6IC4uLgpEOiAuLi4=)Youaregivenaplanegeometryproblemanditscorrespondingsolution:Problem:<template\-basedproblem\>\.<template\-basedgoal\>=\(\)\.ReferenceAnswer\(forcorrectnessonly\):<answer\>Task:\-Rewritetheprobleminclear,concise,andfluentlanguage,preservingtheoriginalmeaning\.\-Convertthetaskintoamultiple\-choicequestionwithexactly4optionslabeledA,B,C,D\.\-UsethereferencesolutionONLYtodeterminethecorrectnumeric/choiceanswer\.\-Createplausibledistractorsofcomparablescaleormagnitudetothecorrectanswer\.\-EnsureEXACTLYONEoptioniscorrect\.\-OutputONLYtherewrittenproblemfollowedbythechoices,withnoexplanationsorextratext\.\-DoNOTincludethesolution,rationales,orextratext\.Outputformat:<Rewrittenproblemstatement\>Choices:A:\.\.\.B:\.\.\.C:\.\.\.D:\.\.\.

Finally, we use a corresponding prompt to refine the solution for the multiple\-choice setting:

[⬇](data:text/plain;base64,WW91IGFyZSBnaXZlbiBhIHBsYW5lIGdlb21ldHJ5IHByb2JsZW0gYW5kIGl0cyBjb3JyZXNwb25kaW5nIHNvbHV0aW9uOgoKUHJvYmxlbToKPHJlZmluZWQgbXVsdGlwbGUtY2hvaWNlIHByb2JsZW0+CgpTb2x1dGlvbjoKPHRlbXBsYXRlLWJhc2VkIHNvbHV0aW9uPgoKVGFzazoKLSBSZXdyaXRlIHRoZSBzb2x1dGlvbiBpbiBjbGVhciwgY29uY2lzZSwgYW5kIGZsdWVudCBsYW5ndWFnZSwgc2ltcGxpZnlpbmcgdHJpdmlhbCBvciByZWR1bmRhbnQgc3RlcHMuCi0gU3RlcC13aXNlIGZvcm1hdHRpbmcgaXMgb3B0aW9uYWwuIFVzZSBpdCBvbmx5IHdoZW4gaXQgaW1wcm92ZXMgY2xhcml0eTsgb3RoZXJ3aXNlLCBwcmVzZW50aW5nIHRoZSBzb2x1dGlvbiBhcyBhIGNvbnRpbnVvdXMgcGFyYWdyYXBoIGlzIGFjY2VwdGFibGUuCi0gRW5zdXJlIHRoZSBmaW5hbCBjaG9pY2UgbGFiZWwgbWF0Y2hlcyB0aGUgcHJvdmlkZWQgc29sdXRpb24ncyBmaW5hbCBhbnN3ZXIuCi0gT3V0cHV0IE9OTFkgdGhlIHJld3JpdHRlbiBzb2x1dGlvbiwgd2l0aCB0aGUgZmluYWwgQ0hPSUNFIExBQkVMIChlLmcuLCBBLCBCLCBDLCBvciBEKSBpbnNpZGUgXGJveGVke30gYXQgdGhlIGVuZC4KLSBEbyBOT1QgaW5jbHVkZSB0aGUgcHJvYmxlbSBzdGF0ZW1lbnQsIGV4cGxhbmF0aW9ucywgb3IgZXh0cmEgdGV4dC4=)Youaregivenaplanegeometryproblemanditscorrespondingsolution:Problem:<refinedmultiple\-choiceproblem\>Solution:<template\-basedsolution\>Task:\-Rewritethesolutioninclear,concise,andfluentlanguage,simplifyingtrivialorredundantsteps\.\-Step\-wiseformattingisoptional\.Useitonlywhenitimprovesclarity;otherwise,presentingthesolutionasacontinuousparagraphisacceptable\.\-Ensurethefinalchoicelabelmatchestheprovidedsolution’sfinalanswer\.\-OutputONLYtherewrittensolution,withthefinalCHOICELABEL\(e\.g\.,A,B,C,orD\)inside\\boxed\{\}attheend\.\-DoNOTincludetheproblemstatement,explanations,orextratext\.

### B\.3Examples of Synthetic Data Instances

We present two examples of our generated instances for calculation problems: one in a final\-answer format and the other in a multiple\-choice format\. The first example is shown below, with its corresponding diagram provided in Figure[7](https://arxiv.org/html/2608.14585#A2.F7)\.

[⬇](data:text/plain;base64,UHJvYmxlbToKQUJDRCBpcyBhIHNxdWFyZSB3aXRoIHNpZGUgbGVuZ3RoIDEwMC4gUG9pbnQgRiBsaWVzIG9uIGEgY2lyY2xlIGNlbnRlcmVkIGF0IEQgd2l0aCBhIHJhZGl1cyBvZiAxNTAuIExpbmUgc2VnbWVudCBGQiBpcyBwZXJwZW5kaWN1bGFyIHRvIERCLCBhbmQgcG9pbnQgRyBpcyB0aGUgZm9vdCBvZiB0aGUgcGVycGVuZGljdWxhciBkcm9wcGVkIGZyb20gcG9pbnQgQiBvbnRvIHRoZSBsaW5lIERGLiBGaW5kIHRoZSBhcmVhIG9mIHRyaWFuZ2xlIEJERy4=)Problem:ABCDisasquarewithsidelength100\.PointFliesonacirclecenteredatDwitharadiusof150\.LinesegmentFBisperpendiculartoDB,andpointGisthefootoftheperpendiculardroppedfrompointBontothelineDF\.FindtheareaoftriangleBDG\.

[⬇](data:text/plain;base64,U29sdXRpb246CkxldCBBQkNEIGJlIGEgc3F1YXJlIHdpdGggYSBzaWRlIGxlbmd0aCBvZiAxMDAuIFBvaW50IEYgbGllcyBvbiBhIGNpcmNsZSBjZW50ZXJlZCBhdCBEIHdpdGggYSByYWRpdXMgb2YgMTUwLCBhbmQgRkIgaXMgcGVycGVuZGljdWxhciB0byBEQi4gUG9pbnQgRyBpcyB0aGUgZm9vdCBvZiB0aGUgcGVycGVuZGljdWxhciBmcm9tIEIgdG8gbGluZSBERi4KClNpbmNlIHRyaWFuZ2xlIEJERiBhbmQgdHJpYW5nbGUgQkRHIHNoYXJlIOKIoEJERiBhbmQgYXJlIGJvdGggcmlnaHQgdHJpYW5nbGVzLCB0aGV5IGFyZSBzaW1pbGFyLiBVc2luZyB0aGUgc2ltaWxhcml0eSByYXRpbywgd2UgaGF2ZToKClxbClxmcmFje0JEfXtERn0gPSBcZnJhY3tER317QkR9ClxdCgpGcm9tIHRoZSBzcXVhcmUsIFwoIEJEID0gMTAwXCkgYW5kIFwoIERGID0gMTUwIFwpLCBzbzoKClxbClxmcmFjezEwMH17MTUwfSA9IFxmcmFje0RHfXsxMDB9IFxpbXBsaWVzIERHID0gXGZyYWN7NDAwfXszfS4KXF0KClNpbmNlIFwoIERGID0gREcgKyBGRyBcKSBhbmQgXCggREYgPSAxNTAgXCksIHN1YnN0aXR1dGluZyBcKCBERyA9IFxmcmFjezQwMH17M30gXCk6CgpcWwpcZnJhY3s0MDB9ezN9ICsgRkcgPSAxNTAgXGltcGxpZXMgRkcgPSBcZnJhY3s1MH17M30uClxdCgpUcmlhbmdsZSBCREcgaGFzIGEgcmlnaHQgYW5nbGUgYXQgRy4gSXRzIGFyZWEgaXMgZ2l2ZW4gYnk6CgpcWwpcdGV4dHtBcmVhfSA9IFxmcmFjezF9ezJ9IFx0aW1lcyBCRyBcdGltZXMgREcuClxdCgpVc2luZyB0aGUgc2ltaWxhcml0eSByYXRpbyBmcm9tIHRyaWFuZ2xlcyBCREcgYW5kIEZCRzoKClxbClxmcmFje0JHfXtER30gPSBcZnJhY3tGR317Qkd9IFxpbXBsaWVzIEJHXjIgPSBERyBcY2RvdCBGRy4KXF0KClN1YnN0aXR1dGluZyBcKCBERyA9IFxmcmFjezQwMH17M30gXCkgYW5kIFwoIEZHID0gXGZyYWN7NTB9ezN9IFwpOgoKXFsKQkdeMiA9IFxmcmFjezQwMH17M30gXGNkb3QgXGZyYWN7NTB9ezN9ID0gXGZyYWN7MjAwMDB9ezl9IFxpbXBsaWVzIEJHID0gXHNxcnR7XGZyYWN7MjAwMDB9ezl9fSA9IFxmcmFjezEwMFxzcXJ0ezJ9fXszfS4KXF0KClRoZSBhcmVhIG9mIHRyaWFuZ2xlIEJERyBpczoKClxbClx0ZXh0e0FyZWF9ID0gXGZyYWN7MX17Mn0gXHRpbWVzIEJHIFx0aW1lcyBERyA9IFxmcmFjezF9ezJ9IFx0aW1lcyBcZnJhY3sxMDBcc3FydHsyfX17M30gXHRpbWVzIFxmcmFjezQwMH17M30gPSBcZnJhY3syMDAwMCBcc3FydHsyfX17OX0uClxdCgpcWwpcYm94ZWR7XGZyYWN7MjAwMDAgXHNxcnR7Mn19ezl9fQpcXQ==)Solution:LetABCDbeasquarewithasidelengthof100\.PointFliesonacirclecenteredatDwitharadiusof150,andFBisperpendiculartoDB\.PointGisthefootoftheperpendicularfromBtolineDF\.SincetriangleBDFandtriangleBDGshare∠\\angleBDFandarebothrighttriangles,theyaresimilar\.Usingthesimilarityratio,wehave:\\\[\\frac\{BD\}\{DF\}=\\frac\{DG\}\{BD\}\\\]Fromthesquare,\\\(BD=100\\\)and\\\(DF=150\\\),so:\\\[\\frac\{100\}\{150\}=\\frac\{DG\}\{100\}\\impliesDG=\\frac\{400\}\{3\}\.\\\]Since\\\(DF=DG\+FG\\\)and\\\(DF=150\\\),substituting\\\(DG=\\frac\{400\}\{3\}\\\):\\\[\\frac\{400\}\{3\}\+FG=150\\impliesFG=\\frac\{50\}\{3\}\.\\\]TriangleBDGhasarightangleatG\.Itsareaisgivenby:\\\[\\text\{Area\}=\\frac\{1\}\{2\}\\timesBG\\timesDG\.\\\]UsingthesimilarityratiofromtrianglesBDGandFBG:\\\[\\frac\{BG\}\{DG\}=\\frac\{FG\}\{BG\}\\impliesBG^2=DG\\cdotFG\.\\\]Substituting\\\(DG=\\frac\{400\}\{3\}\\\)and\\\(FG=\\frac\{50\}\{3\}\\\):\\\[BG^2=\\frac\{400\}\{3\}\\cdot\\frac\{50\}\{3\}=\\frac\{20000\}\{9\}\\impliesBG=\\sqrt\{\\frac\{20000\}\{9\}\}=\\frac\{100\\sqrt\{2\}\}\{3\}\.\\\]TheareaoftriangleBDGis:\\\[\\text\{Area\}=\\frac\{1\}\{2\}\\timesBG\\timesDG=\\frac\{1\}\{2\}\\times\\frac\{100\\sqrt\{2\}\}\{3\}\\times\\frac\{400\}\{3\}=\\frac\{20000\\sqrt\{2\}\}\{9\}\.\\\]\\\[\\boxed\{\\frac\{20000\\sqrt\{2\}\}\{9\}\}\\\]

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/example1.jpg)Figure 7:Diagram of a generated final\-answer calculation problem\.The second example is shown below, with its corresponding diagram provided in Figure[8](https://arxiv.org/html/2608.14585#A2.F8)\.

[⬇](data:text/plain;base64,UHJvYmxlbToKSW4gdHJpYW5nbGUgQUJDLCDiiKBBQkMgaXMgYSByaWdodCBhbmdsZSwgQUIgPSA1MiwgYW5kIEJDID0gMzIuIEQgaXMgYSBwb2ludCBvbiB0aGUgbGluZSBwYXNzaW5nIHRocm91Z2ggQyBhbmQgcGFyYWxsZWwgdG8gQUIsIHN1Y2ggdGhhdCBEQiBpcyBwZXJwZW5kaWN1bGFyIHRvIEFDLiBGaW5kIHRoZSBhcmVhIG9mIHRyaWFuZ2xlIEJDRC4KCkNob2ljZXM6CkE6IDIwNDgvMTMKQjogNDA5Ni8xMwpDOiA1MTIwLzEzCkQ6IDEwMjQvMTM=)Problem:IntriangleABC,∠\\angleABCisarightangle,AB=52,andBC=32\.DisapointonthelinepassingthroughCandparalleltoAB,suchthatDBisperpendiculartoAC\.FindtheareaoftriangleBCD\.Choices:A:2048/13B:4096/13C:5120/13D:1024/13

[⬇](data:text/plain;base64,U29sdXRpb246CkdpdmVuIHRoYXQgXChcYW5nbGUgQUJDXCkgaXMgYSByaWdodCBhbmdsZSwgXChBQlwpIGlzIHBlcnBlbmRpY3VsYXIgdG8gXChCQ1wpLiBTaW5jZSBcKEFCXCkgaXMgcGFyYWxsZWwgdG8gXChDRFwpLCBcKENEXCkgaXMgYWxzbyBwZXJwZW5kaWN1bGFyIHRvIFwoQkNcKSwgbWFraW5nIFwoXGFuZ2xlIEJDRCA9IDkwXlxjaXJjXCkuIFRoZSBhcmVhIG9mIHRyaWFuZ2xlIFwoQkNEXCkgaXMgZ2l2ZW4gYnkgXChcZnJhY3sxfXsyfSBcY2RvdCBCQyBcY2RvdCBDRFwpLgoKVHJpYW5nbGVzIFwoQUJDXCkgYW5kIFwoQkNEXCkgYXJlIHNpbWlsYXIgYmVjYXVzZSBcKFxhbmdsZSBBQkMgPSBcYW5nbGUgQkNEXCkgKGJvdGggXCg5MF5cY2lyY1wpKSwgYW5kIHRoZSBvdGhlciBhbmdsZXMgYXJlIGNvbmdydWVudCBieSB0aGUgZ2VvbWV0cmljIGNvbnN0cmFpbnRzLiBCeSB0aGUgc2ltaWxhcml0eSByYXRpbywgXChcZnJhY3tBQn17QkN9ID0gXGZyYWN7QkN9e0NEfVwpLiBTdWJzdGl0dXRpbmcgdGhlIGdpdmVuIHNpZGUgbGVuZ3RocyBcKEFCID0gNTJcKSBhbmQgXChCQyA9IDMyXCksIHdlIHNvbHZlIGZvciBcKENEXCk6CgpcWwpcZnJhY3s1Mn17MzJ9ID0gXGZyYWN7MzJ9e0NEfSBcaW1wbGllcyBDRCA9IFxmcmFjezMyIFxjZG90IDMyfXs1Mn0gPSBcZnJhY3sxMDI0fXs1Mn0gPSBcZnJhY3syNTZ9ezEzfS4KXF0KClRoZSBhcmVhIG9mIHRyaWFuZ2xlIFwoQkNEXCkgaXM6CgpcWwpcdGV4dHtBcmVhfSA9IFxmcmFjezF9ezJ9IFxjZG90IEJDIFxjZG90IENEID0gXGZyYWN7MX17Mn0gXGNkb3QgMzIgXGNkb3QgXGZyYWN7MjU2fXsxM30gPSBcZnJhY3s0MDk2fXsxM30uClxdCgpcWwpcYm94ZWR7Qn0KXF0=)Solution:Giventhat\\\(\\angleABC\\\)isarightangle,\\\(AB\\\)isperpendicularto\\\(BC\\\)\.Since\\\(AB\\\)isparallelto\\\(CD\\\),\\\(CD\\\)isalsoperpendicularto\\\(BC\\\),making\\\(\\angleBCD=90^\\circ\\\)\.Theareaoftriangle\\\(BCD\\\)isgivenby\\\(\\frac\{1\}\{2\}\\cdotBC\\cdotCD\\\)\.Triangles\\\(ABC\\\)and\\\(BCD\\\)aresimilarbecause\\\(\\angleABC=\\angleBCD\\\)\(both\\\(90^\\circ\\\)\),andtheotheranglesarecongruentbythegeometricconstraints\.Bythesimilarityratio,\\\(\\frac\{AB\}\{BC\}=\\frac\{BC\}\{CD\}\\\)\.Substitutingthegivensidelengths\\\(AB=52\\\)and\\\(BC=32\\\),wesolvefor\\\(CD\\\):\\\[\\frac\{52\}\{32\}=\\frac\{32\}\{CD\}\\impliesCD=\\frac\{32\\cdot32\}\{52\}=\\frac\{1024\}\{52\}=\\frac\{256\}\{13\}\.\\\]Theareaoftriangle\\\(BCD\\\)is:\\\[\\text\{Area\}=\\frac\{1\}\{2\}\\cdotBC\\cdotCD=\\frac\{1\}\{2\}\\cdot32\\cdot\\frac\{256\}\{13\}=\\frac\{4096\}\{13\}\.\\\]\\\[\\boxed\{B\}\\\]

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/example2.jpg)Figure 8:Diagram of a generated multiple\-choice calculation problem\.We also include two examples of synthetic problems that require auxiliary constructions\. The first example is shown below, and its associated diagram is provided in Figure[9](https://arxiv.org/html/2608.14585#A2.F9)\.

[⬇](data:text/plain;base64,UHJvYmxlbToKYSxiID0gY29uc3RydWN0X3NlZ21lbnQoKSwgYyA9IGNvbnN0cnVjdF9vbl9jaXJjbGUoYixhKSwKYyA9IGNvbnN0cnVjdF9vbl9saW5lKGIsYSksIGUgPSBjb25zdHJ1Y3Rfb25fYmxpbmUoYyxhKSwKZiA9IGNvbnN0cnVjdF9hbmdsZV9iaXNlY3RvcihiLGMsZSksIGYgPSBjb25zdHJ1Y3Rfb25fYmxpbmUoZSxhKQpHb2FsOgpDb25jeWNsaWMoYSxjLGUsZik=)Problem:a,b=construct\_segment\(\),c=construct\_on\_circle\(b,a\),c=construct\_on\_line\(b,a\),e=construct\_on\_bline\(c,a\),f=construct\_angle\_bisector\(b,c,e\),f=construct\_on\_bline\(e,a\)Goal:Concyclic\(a,c,e,f\)

[⬇](data:text/plain;base64,QXV4aWxpYXJ5IENvbnN0cnVjdGlvbnM6CmQgPSBjb25zdHJ1Y3RfbWlkcG9pbnQoYixhKSwKaCA9IGNvbnN0cnVjdF9pbnRlcnNlY3Rpb25fdHQoZixhLGUsYixjLGQp)AuxiliaryConstructions:d=construct\_midpoint\(b,a\),h=construct\_intersection\_tt\(f,a,e,b,c,d\)

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/example3.jpg)Figure 9:Diagram of a synthetic problem with its auxiliary constructions\.The second example is presented below, with its corresponding diagram shown in Figure[10](https://arxiv.org/html/2608.14585#A2.F10)\.

[⬇](data:text/plain;base64,UHJvYmxlbToKYSxiID0gY29uc3RydWN0X3NlZ21lbnQoKSwgYyA9IGNvbnN0cnVjdF9vbl9kaWEoYixhKSwKZCA9IGNvbnN0cnVjdF9vbl9ibGluZShjLGEpLCBkID0gY29uc3RydWN0X2FuZ2xlX2Jpc2VjdG9yKGMsYixhKQpHb2FsOgpBbmdsZV9hX2JfYyArIEFuZ2xlX2FfZF9jIC0gMTgw)Problem:a,b=construct\_segment\(\),c=construct\_on\_dia\(b,a\),d=construct\_on\_bline\(c,a\),d=construct\_angle\_bisector\(c,b,a\)Goal:Angle\_a\_b\_c\+Angle\_a\_d\_c\-180

[⬇](data:text/plain;base64,QXV4aWxpYXJ5IENvbnN0cnVjdGlvbnM6CmUgPSBjb25zdHJ1Y3Rfb25fZGlhKGEsYiksIGUgPSBjb25zdHJ1Y3RfYW5nbGVfYmlzZWN0b3IoYyxkLGEp)AuxiliaryConstructions:e=construct\_on\_dia\(a,b\),e=construct\_angle\_bisector\(c,d,a\)

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/example4.jpg)Figure 10:Diagram of a synthetic problem with its auxiliary constructions\.

## Appendix CExperiments

### C\.1Examples of Generated Formal Solutions

We compare the proofs generated by Euclidea against those produced by AlphaGeometry\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\], Newclid\[[43](https://arxiv.org/html/2608.14585#bib.bib43)\], and PyEuclid\[[28](https://arxiv.org/html/2608.14585#bib.bib28)\]\. For this evaluation, we randomly selected two problems: one from JGEX\-AG\-231\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]and another from IMO\-AG\-30\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]\.

The natural language formulation of the first problem is given below, and the corresponding diagram is shown in Figure[11](https://arxiv.org/html/2608.14585#A3.F11)\.

[⬇](data:text/plain;base64,SW4gdHJpYW5nbGUgRUNELCDiiKBFIGlzIGEgcmlnaHQgYW5nbGUuIE8gaXMgdGhlIG1pZHBvaW50IG9mIHNpZGUgREMuIExpbmUgQUMgaXMgcGVycGVuZGljdWxhciB0byBzaWRlIERDLCBhbmQgQUUgaXMgcGVycGVuZGljdWxhciB0byBFTy4gTGluZSBDQSBpbnRlcnNlY3RzIGF0IGEgcG9pbnQgRiwgYW5kIGxpbmUgREUgYWxzbyBwYXNzZXMgdGhyb3VnaCBwb2ludCBGLiBQcm92ZSB0aGF0IEFFIGlzIGVxdWFsIHRvIEFGLg==)IntriangleECD,∠\\angleEisarightangle\.OisthemidpointofsideDC\.LineACisperpendiculartosideDC,andAEisperpendiculartoEO\.LineCAintersectsatapointF,andlineDEalsopassesthroughpointF\.ProvethatAEisequaltoAF\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/jgex.jpg)Figure 11:Diagram of a geometry problem selected from JGEX\-AG\-231\.The proof produced by Euclidea for this problem is shown below:

[⬇](data:text/plain;base64,U29sdXRpb246CjEuIENvbGxpbmVhcihkLGUsZikgPT4gQW5nbGVfZV9kX28gLSBBbmdsZV9mX2RfbyAmIEFuZ2xlX2FfZl9kIC0gQW5nbGVfYV9mX2UgJiBBbmdsZV9kX2VfbyArIEFuZ2xlX2ZfZV9vIC0gMTgwCjIuIENvbGxpbmVhcihjLGQsbykgPT4gUGFyYWxsZWwoYyxkLGQsbykKMy4gUGVycGVuZGljdWxhcihhLGMsYyxkKSAmIFBhcmFsbGVsKGMsZCxkLG8pID0+IFBlcnBlbmRpY3VsYXIoYSxjLGQsbykKNC4gQ29sbGluZWFyKGEsYyxmKSA9PiBQYXJhbGxlbChhLGMsYSxmKQo1LiBQZXJwZW5kaWN1bGFyKGEsYyxkLG8pICYgUGFyYWxsZWwoYSxjLGEsZikgPT4gUGVycGVuZGljdWxhcihhLGYsZCxvKQo2LiBQZXJwZW5kaWN1bGFyKGEsZixkLG8pID0+IEFuZ2xlX2FfZl9kICsgQW5nbGVfZl9kX28gLSA5MAo3LiBBbmdsZV9lX2RfbyAtIEFuZ2xlX2ZfZF9vICYgQW5nbGVfYV9mX2QgLSBBbmdsZV9hX2ZfZSAmIEFuZ2xlX2FfZl9kICsgQW5nbGVfZl9kX28gLSA5MCA9PiBBbmdsZV9hX2ZfZSArIEFuZ2xlX2VfZF9vIC0gOTAKOC4gUGVycGVuZGljdWxhcihhLGUsZSxvKSA9PiBBbmdsZV9hX2VfbyAtIDkwCjkuIEFuZ2xlX2FfZV9mICsgQW5nbGVfYV9lX28gLSBBbmdsZV9mX2VfbyAmIEFuZ2xlX2RfZV9vICsgQW5nbGVfZl9lX28gLSAxODAgJiBBbmdsZV9hX2VfbyAtIDkwID0+IEFuZ2xlX2FfZV9mICsgQW5nbGVfZF9lX28gLSA5MAoxMC4gTWlkcG9pbnQobyxjLGQpICYgUGVycGVuZGljdWxhcihjLGUsZCxlKSA9PiBMZW5ndGhfZF9vIC0gTGVuZ3RoX2VfbwoxMS4gTGVuZ3RoX2RfbyAtIExlbmd0aF9lX28gPT4gQW5nbGVfZF9lX28gLSBBbmdsZV9lX2RfbwoxMi4gQW5nbGVfYV9mX2UgKyBBbmdsZV9lX2RfbyAtIDkwICYgQW5nbGVfYV9lX2YgKyBBbmdsZV9kX2VfbyAtIDkwICYgQW5nbGVfZF9lX28gLSBBbmdsZV9lX2RfbyA9PiBBbmdsZV9hX2VfZiAtIEFuZ2xlX2FfZl9lCjEzLiBBbmdsZV9hX2VfZiAtIEFuZ2xlX2FfZl9lID0+IExlbmd0aF9hX2UgLSBMZW5ndGhfYV9mCg==)Solution:1\.Collinear\(d,e,f\)=\>Angle\_e\_d\_o\-Angle\_f\_d\_o&Angle\_a\_f\_d\-Angle\_a\_f\_e&Angle\_d\_e\_o\+Angle\_f\_e\_o\-1802\.Collinear\(c,d,o\)=\>Parallel\(c,d,d,o\)3\.Perpendicular\(a,c,c,d\)&Parallel\(c,d,d,o\)=\>Perpendicular\(a,c,d,o\)4\.Collinear\(a,c,f\)=\>Parallel\(a,c,a,f\)5\.Perpendicular\(a,c,d,o\)&Parallel\(a,c,a,f\)=\>Perpendicular\(a,f,d,o\)6\.Perpendicular\(a,f,d,o\)=\>Angle\_a\_f\_d\+Angle\_f\_d\_o\-907\.Angle\_e\_d\_o\-Angle\_f\_d\_o&Angle\_a\_f\_d\-Angle\_a\_f\_e&Angle\_a\_f\_d\+Angle\_f\_d\_o\-90=\>Angle\_a\_f\_e\+Angle\_e\_d\_o\-908\.Perpendicular\(a,e,e,o\)=\>Angle\_a\_e\_o\-909\.Angle\_a\_e\_f\+Angle\_a\_e\_o\-Angle\_f\_e\_o&Angle\_d\_e\_o\+Angle\_f\_e\_o\-180&Angle\_a\_e\_o\-90=\>Angle\_a\_e\_f\+Angle\_d\_e\_o\-9010\.Midpoint\(o,c,d\)&Perpendicular\(c,e,d,e\)=\>Length\_d\_o\-Length\_e\_o11\.Length\_d\_o\-Length\_e\_o=\>Angle\_d\_e\_o\-Angle\_e\_d\_o12\.Angle\_a\_f\_e\+Angle\_e\_d\_o\-90&Angle\_a\_e\_f\+Angle\_d\_e\_o\-90&Angle\_d\_e\_o\-Angle\_e\_d\_o=\>Angle\_a\_e\_f\-Angle\_a\_f\_e13\.Angle\_a\_e\_f\-Angle\_a\_f\_e=\>Length\_a\_e\-Length\_a\_f

The proof produced by AlphaGeometry for this problem is shown below:

[⬇](data:text/plain;base64,ICogUHJvb2Ygc3RlcHM6CjAwMS4gQyxPLEQgYXJlIGNvbGxpbmVhciBbMDFdICYgQ0Qg4p+CIEFDIFswM10g4oeSICBDTyDin4IgQ0EgWzA3XQowMDIuIENPIOKfgiBDQSBbMDddICYgQUUg4p+CIEVPIFswNF0g4oeSICAoKkBcdGV4dGNvbG9ye3JlZH17JFxhbmdsZSRDT0UgPSAkXGFuZ2xlJENBRX1AKikgWzA4XQowMDMuIEMsQSxGIGFyZSBjb2xsaW5lYXIgWzA1XSAmIEMsTyxEIGFyZSBjb2xsaW5lYXIgWzAxXSAmICgqQFx0ZXh0Y29sb3J7cmVkfXskXGFuZ2xlJENPRSA9ICRcYW5nbGUkQ0FFfUAqKSBbMDhdIOKHkiAg4oigRkFFID0g4oigQ09FIFswOV0KMDA0LiBELEYsRSBhcmUgY29sbGluZWFyIFswNl0gJiBERSDin4IgQ0UgWzAwXSDih5IgIEZEIOKfgiBDRSBbMTBdCjAwNS4gQUUg4p+CIEVPIFswNF0gJiBGRCDin4IgQ0UgWzEwXSDih5IgICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoQUUtRkQpfUAqKSA9IOKIoE9FQyBbMTFdCjAwNi4gRCxGLEUgYXJlIGNvbGxpbmVhciBbMDZdICYgKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChBRS1GRCl9QCopID0g4oigT0VDIFsxMV0g4oeSICDiiKBGRUEgPSDiiKBDRU8gWzEyXQowMDcuIOKIoEZBRSA9IOKIoENPRSBbMDldICYg4oigRkVBID0g4oigQ0VPIFsxMl0gKFNpbWlsYXIgVHJpYW5nbGVzKeKHkiAgT0M6T0UgPSBBRjpBRSBbMTNdCjAwOC4gQyxPLEQgYXJlIGNvbGxpbmVhciBbMDFdICYgT0QgPSBPQyBbMDJdIOKHkiAgTyBpcyBtaWRwb2ludCBvZiBEQyBbMTRdCjAwOS4gQ0Ug4p+CIERFIFswMF0gJiBPIGlzIG1pZHBvaW50IG9mIERDIFsxNF0g4oeSICBDTyA9IEVPIFsxNV0KMDEwLiBPQzpPRSA9IEFGOkFFIFsxM10gJiBDTyA9IEVPIFsxNV0g4oeSICBBRiA9IEFFCg==)\*Proofsteps:001\.C,O,Darecollinear\[01\]&CD⟂\\perpAC\[03\]⇒\\RightarrowCO⟂\\perpCA\[07\]002\.CO⟂\\perpCA\[07\]&AE⟂\\perpEO\[04\]⇒\\Rightarrow∠\\angleCOE =∠\\angleCAE\[08\]003\.C,A,Farecollinear\[05\]&C,O,Darecollinear\[01\]&∠\\angleCOE =∠\\angleCAE\[08\]⇒\\Rightarrow∠\\angleFAE=∠\\angleCOE\[09\]004\.D,F,Earecollinear\[06\]&DE⟂\\perpCE\[00\]⇒\\RightarrowFD⟂\\perpCE\[10\]005\.AE⟂\\perpEO\[04\]&FD⟂\\perpCE\[10\]⇒\\Rightarrow∠\\angle\(AE\-FD\)=∠\\angleOEC\[11\]006\.D,F,Earecollinear\[06\]&∠\\angle\(AE\-FD\)=∠\\angleOEC\[11\]⇒\\Rightarrow∠\\angleFEA=∠\\angleCEO\[12\]007\.∠\\angleFAE=∠\\angleCOE\[09\]&∠\\angleFEA=∠\\angleCEO\[12\]\(SimilarTriangles\)⇒\\RightarrowOC:OE=AF:AE\[13\]008\.C,O,Darecollinear\[01\]&OD=OC\[02\]⇒\\RightarrowOismidpointofDC\[14\]009\.CE⟂\\perpDE\[00\]&OismidpointofDC\[14\]⇒\\RightarrowCO=EO\[15\]010\.OC:OE=AF:AE\[13\]&CO=EO\[15\]⇒\\RightarrowAF=AE

The proof produced by Newclid for this problem is shown below:

[⬇](data:text/plain;base64,IyBQcm9vZjoKMDAwLiB8IE8gaXMgdGhlIG1pZHBvaW50IG9mIENEIFtDMF0sIENFIOKfgiBERSBbQzFdID0ocjE5IEh5cG90ZW51c2UgaXMgZGlhbWV0ZXIpPiBDTyA9IEVPIFswXQowMDEuIHwgQ08gPSBFTyBbMF0gPShyMTMgSXNvc2NlbGVzIHRyaWFuZ2xlIGVxdWFsIGFuZ2xlcyk+IOKIoChDRSxDTykgPSDiiKAoRU8sQ0UpIFsxXQowMDIuIHwgQSwgQywgRiBhcmUgY29sbGluZWFyIFtDMl0sIEEg4omgIEMgW04wXSwgQSDiiaAgRiBbTjFdLCBDIOKJoCBGIFtOMl0gPShyODIgUGFyYWxsZWwgZnJvbSBjb2xsaW5lYXIpPiBBRiDiiKUgQUMgWzJdCjAwMy4gfCBPIGlzIHRoZSBtaWRwb2ludCBvZiBDRCBbQzBdID0ocjU2IFByb3BlcnRpZXMgb2YgbWlkcG9pbnQgKGNvbGwpKT4gQywgRCwgTyBhcmUgY29sbGluZWFyIFszXQowMDQuIHwgQywgRCwgTyBhcmUgY29sbGluZWFyIFszXSwgQyDiiaAgRCBbTjNdLCBDIOKJoCBPIFtONF0sIEQg4omgIE8gW041XSA9KHI4MiBQYXJhbGxlbCBmcm9tIGNvbGxpbmVhcik+IENPIOKIpSBDRCBbNF0KMDA1LiB8IEQsIEUsIEYgYXJlIGNvbGxpbmVhciBbQzNdLCBEIOKJoCBFIFtONl0sIEQg4omgIEYgW043XSwgRSDiiaAgRiBbTjhdID0ocjgyIFBhcmFsbGVsIGZyb20gY29sbGluZWFyKT4gREUg4oilIEVGIFs1XQowMDYuIHwg4oigKENFLENPKSA9IOKIoChFTyxDRSkgWzFdLCBBRiDiiKUgQUMgWzJdLCBDTyDiiKUgQ0QgWzRdLCBERSDiiKUgRUYgWzVdLCBBQyDin4IgQ0QgW0M0XSwgQUUg4p+CIEVPIFtDNV0sIENFIOKfgiBERSBbQzFdID0oQVIgRGVkdWN0aW9uKT4gKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChBRSxFRil9QCopID0gKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChFRixBRil9QCopIFs2XQowMDcuIHwgKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChBRSxFRil9QCopID0gKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChFRixBRil9QCopIFs2XSwgQSwgRSwgRiBhcmUgbm90IGNvbGxpbmVhciBbTjldID0ocjE0IEVxdWFsIGJhc2UgYW5nbGVzIGltcGx5IGlzb3NjZWxlcyk+IEFGID0gQUUgWzdd)\#Proof:000\.\|OisthemidpointofCD\[C0\],CE⟂\\perpDE\[C1\]=\(r19Hypotenuseisdiameter\)\>CO=EO\[0\]001\.\|CO=EO\[0\]=\(r13Isoscelestriangleequalangles\)\>∠\\angle\(CE,CO\)=∠\\angle\(EO,CE\)\[1\]002\.\|A,C,Farecollinear\[C2\],A≠\\neqC\[N0\],A≠\\neqF\[N1\],C≠\\neqF\[N2\]=\(r82Parallelfromcollinear\)\>AF∥\\parallelAC\[2\]003\.\|OisthemidpointofCD\[C0\]=\(r56Propertiesofmidpoint\(coll\)\)\>C,D,Oarecollinear\[3\]004\.\|C,D,Oarecollinear\[3\],C≠\\neqD\[N3\],C≠\\neqO\[N4\],D≠\\neqO\[N5\]=\(r82Parallelfromcollinear\)\>CO∥\\parallelCD\[4\]005\.\|D,E,Farecollinear\[C3\],D≠\\neqE\[N6\],D≠\\neqF\[N7\],E≠\\neqF\[N8\]=\(r82Parallelfromcollinear\)\>DE∥\\parallelEF\[5\]006\.\|∠\\angle\(CE,CO\)=∠\\angle\(EO,CE\)\[1\],AF∥\\parallelAC\[2\],CO∥\\parallelCD\[4\],DE∥\\parallelEF\[5\],AC⟂\\perpCD\[C4\],AE⟂\\perpEO\[C5\],CE⟂\\perpDE\[C1\]=\(ARDeduction\)\>∠\\angle\(AE,EF\)=∠\\angle\(EF,AF\)\[6\]007\.\|∠\\angle\(AE,EF\)=∠\\angle\(EF,AF\)\[6\],A,E,Farenotcollinear\[N9\]=\(r14Equalbaseanglesimplyisosceles\)\>AF=AE\[7\]

The proof produced by PyEuclid for this problem is shown below:

[⬇](data:text/plain;base64,KiBQcm9vZiBzdGVwczoKMDAxLiBMZW5ndGhfY19vIC0gTGVuZ3RoX2RfbyAmCkNvbGxpbmVhcihjLGQsbykgJgpCZXR3ZWVuKG8sYyxkKSDih5IgLUxlbmd0aF9jX2QvMiArIExlbmd0aF9kX28KMDAyLiBBbmdsZV9jX2RfZSAtIEFuZ2xlX2ZfZF9vICYKQW5nbGVfY19kX2YgLSBBbmdsZV9mX2RfbyDih5IgQW5nbGVfY19kX2UgLSBBbmdsZV9jX2RfZgowMDMuIFBlcnBlbmRpY3VsYXIoYSxjLGMsZCkgJgpQYXJhbGxlbChhLGMsYyxmKSDih5IgQW5nbGVfZF9jX2YgLSBwaS8yCjAwNC4gQW5nbGVfZF9jX2YgLSBwaS8yKDMpICYKQW5nbGVfY19lX2QgLSBwaS8yIOKHkiBBbmdsZV9jX2VfZCAtIEFuZ2xlX2RfY19mCjAwNS4gTm90KENvbGxpbmVhcihjLGQsZSkpICYKQW5nbGVfY19kX2UgLSBBbmdsZV9jX2RfZigyKSAmCkFuZ2xlX2NfZV9kIC0gQW5nbGVfZF9jX2YoNCkg4oeSIExlbmd0aF9jX2QvTGVuZ3RoX2RfZiAtIExlbmd0aF9kX2UvTGVuZ3RoX2NfZAowMDYuIFBlcnBlbmRpY3VsYXIoYyxlLGQsZSkgJgpQYXJhbGxlbChkLGUsZSxmKSDih5IgQW5nbGVfY19lX2YgLSBwaS8yCjAwNy4gQW5nbGVfY19lX2QgLSBwaS8yICYKQW5nbGVfY19lX2YgLSBwaS8yKDYpIOKHkiAtQW5nbGVfY19lX2QgKyBBbmdsZV9jX2VfZgowMDguIEFuZ2xlX2NfZV9kIC0gcGkvMiAmCkFuZ2xlX2NfZF9lIC0gQW5nbGVfZl9kX28gJgpBbmdsZV9jX2RfZSArIEFuZ2xlX2NfZV9kICsgQW5nbGVfZF9jX2UgLSBwaSDih5IgQW5nbGVfZF9jX2UgKyBBbmdsZV9mX2RfbyAtIHBpLzIKMDA5LiBBbmdsZV9jX2RfZiAtIEFuZ2xlX2ZfZF9vICYKQW5nbGVfY19mX2QgLSBBbmdsZV9jX2ZfZSAmCkFuZ2xlX2NfZF9mICsgQW5nbGVfY19mX2QgKyBBbmdsZV9kX2NfZiAtIHBpICYKQW5nbGVfZF9jX2YgLSBwaS8yIOKHkiBBbmdsZV9jX2ZfZSArIEFuZ2xlX2ZfZF9vIC0gcGkvMgowMTAuIEFuZ2xlX2RfY19lICsgQW5nbGVfZl9kX28gLSBwaS8yKDgpICYKQW5nbGVfY19mX2UgKyBBbmdsZV9mX2RfbyAtIHBpLzIoOSkg4oeSIEFuZ2xlX2NfZl9lIC0gQW5nbGVfZF9jX2UKMDExLiBOb3QoQ29sbGluZWFyKGMsZSxmKSkgJgotQW5nbGVfY19lX2QgKyBBbmdsZV9jX2VfZig3KSAmCkFuZ2xlX2NfZl9lIC0gQW5nbGVfZF9jX2UoMTApIOKHkiBMZW5ndGhfY19lL0xlbmd0aF9kX2UgLSBMZW5ndGhfZV9mL0xlbmd0aF9jX2UKMDEyLiBBbmdsZV9hX2VfbyAtIHBpLzIgJgpBbmdsZV9hX2ZfZSAtIEFuZ2xlX2NfZl9kICYKLUFuZ2xlX2NfZF9mICsgQW5nbGVfZl9kX28gJgotQW5nbGVfYV9lX2YgLSBBbmdsZV9hX2VfbyArIEFuZ2xlX2ZfZV9vICYKQW5nbGVfYV9lX2YgKyBBbmdsZV9hX2ZfZSArIEFuZ2xlX2VfYV9mIC0gcGkgJgpBbmdsZV9jX2RfZiArIEFuZ2xlX2NfZl9kICsgQW5nbGVfZF9jX2YgLSBwaSAmCkFuZ2xlX2RfY19mIC0gcGkvMiDih5IgQW5nbGVfZV9hX2YgLSBBbmdsZV9mX2RfbyArIEFuZ2xlX2ZfZV9vIC0gcGkKMDEzLiAtQW5nbGVfZV9kX28gKyBBbmdsZV9mX2RfbyAmCkFuZ2xlX2RfZV9vICsgQW5nbGVfZF9vX2UgKyBBbmdsZV9lX2RfbyAtIHBpICYKQW5nbGVfY19vX2UgKyBBbmdsZV9kX29fZSAtIHBpICYKQW5nbGVfZF9lX28gKyBBbmdsZV9mX2VfbyAtIHBpIOKHkiBBbmdsZV9jX29fZSAtIEFuZ2xlX2ZfZF9vICsgQW5nbGVfZl9lX28gLSBwaQowMTQuIEFuZ2xlX2VfYV9mIC0gQW5nbGVfZl9kX28gKyBBbmdsZV9mX2VfbyAtIHBpKDEyKSAmCkFuZ2xlX2Nfb19lIC0gQW5nbGVfZl9kX28gKyBBbmdsZV9mX2VfbyAtIHBpKDEzKSDih5IgLUFuZ2xlX2Nfb19lICsgQW5nbGVfZV9hX2YKMDE1LiAtQW5nbGVfY19lX2YgLSBBbmdsZV9jX2VfbyArIEFuZ2xlX2ZfZV9vICYKQW5nbGVfY19lX2YgLSBwaS8yIOKHkiBBbmdsZV9jX2VfbyAtIEFuZ2xlX2ZfZV9vICsgcGkvMgowMTYuIEFuZ2xlX2FfZV9vIC0gcGkvMiAmCi1BbmdsZV9hX2VfZiAtIEFuZ2xlX2FfZV9vICsgQW5nbGVfZl9lX28g4oeSIEFuZ2xlX2FfZV9mIC0gQW5nbGVfZl9lX28gKyBwaS8yCjAxNy4gQW5nbGVfY19lX28gLSBBbmdsZV9mX2VfbyArIHBpLzIoMTUpICYKQW5nbGVfYV9lX2YgLSBBbmdsZV9mX2VfbyArIHBpLzIoMTYpIOKHkiBBbmdsZV9hX2VfZiAtIEFuZ2xlX2NfZV9vCjAxOC4gTm90KENvbGxpbmVhcihhLGUsZikpICYKLUFuZ2xlX2Nfb19lICsgQW5nbGVfZV9hX2YoMTQpICYKQW5nbGVfYV9lX2YgLSBBbmdsZV9jX2VfbygxNykg4oeSIExlbmd0aF9hX2YvTGVuZ3RoX2NfbyAtIExlbmd0aF9lX2YvTGVuZ3RoX2NfZQowMTkuIC1MZW5ndGhfY19vICsgTGVuZ3RoX2RfbyAmCi1MZW5ndGhfY19kLzIgKyBMZW5ndGhfZF9vKDEpICYKTGVuZ3RoX2NfZC9MZW5ndGhfZF9mIC0gTGVuZ3RoX2RfZS9MZW5ndGhfY19kKDUpICYKTGVuZ3RoX2NfZS9MZW5ndGhfZF9lIC0gTGVuZ3RoX2VfZi9MZW5ndGhfY19lKDExKSAmCkxlbmd0aF9hX2YvTGVuZ3RoX2NfbyAtIExlbmd0aF9lX2YvTGVuZ3RoX2NfZSgxOCkg4oeSIExlbmd0aF9hX2YgLSBzcXJ0KExlbmd0aF9kX2YpKnNxcnQoTGVuZ3RoX2VfZikvMgowMjAuIC1BbmdsZV9hX2ZfZSArIEFuZ2xlX2NfZl9kICYKQW5nbGVfY19kX2YgLSBBbmdsZV9mX2RfbyAmCkFuZ2xlX2NfZF9mICsgQW5nbGVfY19mX2QgKyBBbmdsZV9kX2NfZiAtIHBpICYKQW5nbGVfZF9jX2YgLSBwaS8yIOKHkiBBbmdsZV9hX2ZfZSArIEFuZ2xlX2ZfZF9vIC0gcGkvMgowMjEuIEFuZ2xlX2NfZV9kIC0gcGkvMiAmCkFuZ2xlX2NfZF9lIC0gQW5nbGVfZl9kX28gJgpBbmdsZV9kX2NfZSAtIEFuZ2xlX2VfY19vICYKQW5nbGVfY19kX2UgKyBBbmdsZV9jX2VfZCArIEFuZ2xlX2RfY19lIC0gcGkg4oeSIEFuZ2xlX2VfY19vICsgQW5nbGVfZl9kX28gLSBwaS8yCjAyMi4gQW5nbGVfYV9mX2UgKyBBbmdsZV9mX2RfbyAtIHBpLzIoMjApICYKQW5nbGVfZV9jX28gKyBBbmdsZV9mX2RfbyAtIHBpLzIoMjEpIOKHkiBBbmdsZV9hX2ZfZSAtIEFuZ2xlX2VfY19vCjAyMy4gTm90KENvbGxpbmVhcihhLGUsZikpICYKQW5nbGVfYV9lX2YgLSBBbmdsZV9jX2VfbygxNykgJgpBbmdsZV9hX2ZfZSAtIEFuZ2xlX2VfY19vKDIyKSDih5IgTGVuZ3RoX2FfZS9MZW5ndGhfZV9vIC0gTGVuZ3RoX2VfZi9MZW5ndGhfY19lCjAyNC4gQW5nbGVfZV9kX28gLSBBbmdsZV9mX2RfbyAmCkFuZ2xlX2RfZV9vICsgQW5nbGVfZF9vX2UgKyBBbmdsZV9lX2RfbyAtIHBpICYKQW5nbGVfZF9lX28gKyBBbmdsZV9mX2VfbyAtIHBpIOKHkiBBbmdsZV9kX29fZSArIEFuZ2xlX2ZfZF9vIC0gQW5nbGVfZl9lX28KMDI1LiBBbmdsZV9hX2VfbyAtIHBpLzIgJgotQW5nbGVfYV9mX2UgKyBBbmdsZV9jX2ZfZCAmCkFuZ2xlX2NfZF9mIC0gQW5nbGVfZl9kX28gJgotQW5nbGVfYV9lX2YgLSBBbmdsZV9hX2VfbyArIEFuZ2xlX2ZfZV9vICYKQW5nbGVfYV9lX2YgKyBBbmdsZV9hX2ZfZSArIEFuZ2xlX2VfYV9mIC0gcGkgJgpBbmdsZV9jX2RfZiArIEFuZ2xlX2NfZl9kICsgQW5nbGVfZF9jX2YgLSBwaSAmCkFuZ2xlX2NfYV9lICsgQW5nbGVfZV9hX2YgLSBwaSAmCkFuZ2xlX2RfY19mIC0gcGkvMiDih5IgQW5nbGVfY19hX2UgKyBBbmdsZV9mX2RfbyAtIEFuZ2xlX2ZfZV9vCjAyNi4gQW5nbGVfZF9vX2UgKyBBbmdsZV9mX2RfbyAtIEFuZ2xlX2ZfZV9vKDI0KSAmCkFuZ2xlX2NfYV9lICsgQW5nbGVfZl9kX28gLSBBbmdsZV9mX2VfbygyNSkg4oeSIEFuZ2xlX2NfYV9lIC0gQW5nbGVfZF9vX2UKMDI3LiBBbmdsZV9hX2NfZCAtIHBpLzIgJgpBbmdsZV9jX2VfZCAtIHBpLzIgJgotQW5nbGVfY19kX2UgKyBBbmdsZV9mX2RfbyAmCkFuZ2xlX2FfY19kIC0gQW5nbGVfYV9jX2UgLSBBbmdsZV9kX2NfZSAmCkFuZ2xlX2NfZF9lICsgQW5nbGVfY19lX2QgKyBBbmdsZV9kX2NfZSAtIHBpIOKHkiBBbmdsZV9hX2NfZSAtIEFuZ2xlX2ZfZF9vCjAyOC4gQW5nbGVfYV9jX2UgLSBBbmdsZV9mX2RfbygyNykgJgpBbmdsZV9lX2RfbyAtIEFuZ2xlX2ZfZF9vIOKHkiBBbmdsZV9hX2NfZSAtIEFuZ2xlX2VfZF9vCjAyOS4gTm90KENvbGxpbmVhcihhLGMsZSkpICYKQW5nbGVfY19hX2UgLSBBbmdsZV9kX29fZSgyNikgJgpBbmdsZV9hX2NfZSAtIEFuZ2xlX2VfZF9vKDI4KSDih5IgTGVuZ3RoX2FfZS9MZW5ndGhfZV9vIC0gTGVuZ3RoX2NfZS9MZW5ndGhfZF9lCjAzMC4gTGVuZ3RoX2NfbyAtIExlbmd0aF9kX28gJgpDb2xsaW5lYXIoYyxkLG8pICYKQmV0d2VlbihvLGMsZCkgJgpQZXJwZW5kaWN1bGFyKGMsZSxkLGUpIOKHkiBMZW5ndGhfY19vIC0gTGVuZ3RoX2VfbwowMzEuIC1MZW5ndGhfY19kLzIgKyBMZW5ndGhfZF9vKDEpICYKTGVuZ3RoX2FfZS9MZW5ndGhfZV9vIC0gTGVuZ3RoX2VfZi9MZW5ndGhfY19lKDIzKSAmCkxlbmd0aF9jX2QvTGVuZ3RoX2RfZiAtIExlbmd0aF9kX2UvTGVuZ3RoX2NfZCg1KSAmCkxlbmd0aF9hX2UvTGVuZ3RoX2VfbyAtIExlbmd0aF9jX2UvTGVuZ3RoX2RfZSgyOSkgJgpMZW5ndGhfZF9vL0xlbmd0aF9lX28gLSBMZW5ndGhfZV9vL0xlbmd0aF9kX28g4oeSIExlbmd0aF9hX2UgLSBzcXJ0KExlbmd0aF9kX2YpKnNxcnQoTGVuZ3RoX2VfZikvMgowMzIuIExlbmd0aF9hX2YgLSBzcXJ0KExlbmd0aF9kX2YpKnNxcnQoTGVuZ3RoX2VfZikvMigxOSkgJgpMZW5ndGhfYV9lIC0gc3FydChMZW5ndGhfZF9mKSpzcXJ0KExlbmd0aF9lX2YpLzIoMzEpIOKHkiBMZW5ndGhfYV9lIC0gTGVuZ3RoX2FfZg==)\*Proofsteps:001\.Length\_c\_o\-Length\_d\_o&Collinear\(c,d,o\)&Between\(o,c,d\)⇒\\Rightarrow\-Length\_c\_d/2\+Length\_d\_o002\.Angle\_c\_d\_e\-Angle\_f\_d\_o&Angle\_c\_d\_f\-Angle\_f\_d\_o⇒\\RightarrowAngle\_c\_d\_e\-Angle\_c\_d\_f003\.Perpendicular\(a,c,c,d\)&Parallel\(a,c,c,f\)⇒\\RightarrowAngle\_d\_c\_f\-pi/2004\.Angle\_d\_c\_f\-pi/2\(3\)&Angle\_c\_e\_d\-pi/2⇒\\RightarrowAngle\_c\_e\_d\-Angle\_d\_c\_f005\.Not\(Collinear\(c,d,e\)\)&Angle\_c\_d\_e\-Angle\_c\_d\_f\(2\)&Angle\_c\_e\_d\-Angle\_d\_c\_f\(4\)⇒\\RightarrowLength\_c\_d/Length\_d\_f\-Length\_d\_e/Length\_c\_d006\.Perpendicular\(c,e,d,e\)&Parallel\(d,e,e,f\)⇒\\RightarrowAngle\_c\_e\_f\-pi/2007\.Angle\_c\_e\_d\-pi/2&Angle\_c\_e\_f\-pi/2\(6\)⇒\\Rightarrow\-Angle\_c\_e\_d\+Angle\_c\_e\_f008\.Angle\_c\_e\_d\-pi/2&Angle\_c\_d\_e\-Angle\_f\_d\_o&Angle\_c\_d\_e\+Angle\_c\_e\_d\+Angle\_d\_c\_e\-pi⇒\\RightarrowAngle\_d\_c\_e\+Angle\_f\_d\_o\-pi/2009\.Angle\_c\_d\_f\-Angle\_f\_d\_o&Angle\_c\_f\_d\-Angle\_c\_f\_e&Angle\_c\_d\_f\+Angle\_c\_f\_d\+Angle\_d\_c\_f\-pi&Angle\_d\_c\_f\-pi/2⇒\\RightarrowAngle\_c\_f\_e\+Angle\_f\_d\_o\-pi/2010\.Angle\_d\_c\_e\+Angle\_f\_d\_o\-pi/2\(8\)&Angle\_c\_f\_e\+Angle\_f\_d\_o\-pi/2\(9\)⇒\\RightarrowAngle\_c\_f\_e\-Angle\_d\_c\_e011\.Not\(Collinear\(c,e,f\)\)&\-Angle\_c\_e\_d\+Angle\_c\_e\_f\(7\)&Angle\_c\_f\_e\-Angle\_d\_c\_e\(10\)⇒\\RightarrowLength\_c\_e/Length\_d\_e\-Length\_e\_f/Length\_c\_e012\.Angle\_a\_e\_o\-pi/2&Angle\_a\_f\_e\-Angle\_c\_f\_d&\-Angle\_c\_d\_f\+Angle\_f\_d\_o&\-Angle\_a\_e\_f\-Angle\_a\_e\_o\+Angle\_f\_e\_o&Angle\_a\_e\_f\+Angle\_a\_f\_e\+Angle\_e\_a\_f\-pi&Angle\_c\_d\_f\+Angle\_c\_f\_d\+Angle\_d\_c\_f\-pi&Angle\_d\_c\_f\-pi/2⇒\\RightarrowAngle\_e\_a\_f\-Angle\_f\_d\_o\+Angle\_f\_e\_o\-pi013\.\-Angle\_e\_d\_o\+Angle\_f\_d\_o&Angle\_d\_e\_o\+Angle\_d\_o\_e\+Angle\_e\_d\_o\-pi&Angle\_c\_o\_e\+Angle\_d\_o\_e\-pi&Angle\_d\_e\_o\+Angle\_f\_e\_o\-pi⇒\\RightarrowAngle\_c\_o\_e\-Angle\_f\_d\_o\+Angle\_f\_e\_o\-pi014\.Angle\_e\_a\_f\-Angle\_f\_d\_o\+Angle\_f\_e\_o\-pi\(12\)&Angle\_c\_o\_e\-Angle\_f\_d\_o\+Angle\_f\_e\_o\-pi\(13\)⇒\\Rightarrow\-Angle\_c\_o\_e\+Angle\_e\_a\_f015\.\-Angle\_c\_e\_f\-Angle\_c\_e\_o\+Angle\_f\_e\_o&Angle\_c\_e\_f\-pi/2⇒\\RightarrowAngle\_c\_e\_o\-Angle\_f\_e\_o\+pi/2016\.Angle\_a\_e\_o\-pi/2&\-Angle\_a\_e\_f\-Angle\_a\_e\_o\+Angle\_f\_e\_o⇒\\RightarrowAngle\_a\_e\_f\-Angle\_f\_e\_o\+pi/2017\.Angle\_c\_e\_o\-Angle\_f\_e\_o\+pi/2\(15\)&Angle\_a\_e\_f\-Angle\_f\_e\_o\+pi/2\(16\)⇒\\RightarrowAngle\_a\_e\_f\-Angle\_c\_e\_o018\.Not\(Collinear\(a,e,f\)\)&\-Angle\_c\_o\_e\+Angle\_e\_a\_f\(14\)&Angle\_a\_e\_f\-Angle\_c\_e\_o\(17\)⇒\\RightarrowLength\_a\_f/Length\_c\_o\-Length\_e\_f/Length\_c\_e019\.\-Length\_c\_o\+Length\_d\_o&\-Length\_c\_d/2\+Length\_d\_o\(1\)&Length\_c\_d/Length\_d\_f\-Length\_d\_e/Length\_c\_d\(5\)&Length\_c\_e/Length\_d\_e\-Length\_e\_f/Length\_c\_e\(11\)&Length\_a\_f/Length\_c\_o\-Length\_e\_f/Length\_c\_e\(18\)⇒\\RightarrowLength\_a\_f\-sqrt\(Length\_d\_f\)\*sqrt\(Length\_e\_f\)/2020\.\-Angle\_a\_f\_e\+Angle\_c\_f\_d&Angle\_c\_d\_f\-Angle\_f\_d\_o&Angle\_c\_d\_f\+Angle\_c\_f\_d\+Angle\_d\_c\_f\-pi&Angle\_d\_c\_f\-pi/2⇒\\RightarrowAngle\_a\_f\_e\+Angle\_f\_d\_o\-pi/2021\.Angle\_c\_e\_d\-pi/2&Angle\_c\_d\_e\-Angle\_f\_d\_o&Angle\_d\_c\_e\-Angle\_e\_c\_o&Angle\_c\_d\_e\+Angle\_c\_e\_d\+Angle\_d\_c\_e\-pi⇒\\RightarrowAngle\_e\_c\_o\+Angle\_f\_d\_o\-pi/2022\.Angle\_a\_f\_e\+Angle\_f\_d\_o\-pi/2\(20\)&Angle\_e\_c\_o\+Angle\_f\_d\_o\-pi/2\(21\)⇒\\RightarrowAngle\_a\_f\_e\-Angle\_e\_c\_o023\.Not\(Collinear\(a,e,f\)\)&Angle\_a\_e\_f\-Angle\_c\_e\_o\(17\)&Angle\_a\_f\_e\-Angle\_e\_c\_o\(22\)⇒\\RightarrowLength\_a\_e/Length\_e\_o\-Length\_e\_f/Length\_c\_e024\.Angle\_e\_d\_o\-Angle\_f\_d\_o&Angle\_d\_e\_o\+Angle\_d\_o\_e\+Angle\_e\_d\_o\-pi&Angle\_d\_e\_o\+Angle\_f\_e\_o\-pi⇒\\RightarrowAngle\_d\_o\_e\+Angle\_f\_d\_o\-Angle\_f\_e\_o025\.Angle\_a\_e\_o\-pi/2&\-Angle\_a\_f\_e\+Angle\_c\_f\_d&Angle\_c\_d\_f\-Angle\_f\_d\_o&\-Angle\_a\_e\_f\-Angle\_a\_e\_o\+Angle\_f\_e\_o&Angle\_a\_e\_f\+Angle\_a\_f\_e\+Angle\_e\_a\_f\-pi&Angle\_c\_d\_f\+Angle\_c\_f\_d\+Angle\_d\_c\_f\-pi&Angle\_c\_a\_e\+Angle\_e\_a\_f\-pi&Angle\_d\_c\_f\-pi/2⇒\\RightarrowAngle\_c\_a\_e\+Angle\_f\_d\_o\-Angle\_f\_e\_o026\.Angle\_d\_o\_e\+Angle\_f\_d\_o\-Angle\_f\_e\_o\(24\)&Angle\_c\_a\_e\+Angle\_f\_d\_o\-Angle\_f\_e\_o\(25\)⇒\\RightarrowAngle\_c\_a\_e\-Angle\_d\_o\_e027\.Angle\_a\_c\_d\-pi/2&Angle\_c\_e\_d\-pi/2&\-Angle\_c\_d\_e\+Angle\_f\_d\_o&Angle\_a\_c\_d\-Angle\_a\_c\_e\-Angle\_d\_c\_e&Angle\_c\_d\_e\+Angle\_c\_e\_d\+Angle\_d\_c\_e\-pi⇒\\RightarrowAngle\_a\_c\_e\-Angle\_f\_d\_o028\.Angle\_a\_c\_e\-Angle\_f\_d\_o\(27\)&Angle\_e\_d\_o\-Angle\_f\_d\_o⇒\\RightarrowAngle\_a\_c\_e\-Angle\_e\_d\_o029\.Not\(Collinear\(a,c,e\)\)&Angle\_c\_a\_e\-Angle\_d\_o\_e\(26\)&Angle\_a\_c\_e\-Angle\_e\_d\_o\(28\)⇒\\RightarrowLength\_a\_e/Length\_e\_o\-Length\_c\_e/Length\_d\_e030\.Length\_c\_o\-Length\_d\_o&Collinear\(c,d,o\)&Between\(o,c,d\)&Perpendicular\(c,e,d,e\)⇒\\RightarrowLength\_c\_o\-Length\_e\_o031\.\-Length\_c\_d/2\+Length\_d\_o\(1\)&Length\_a\_e/Length\_e\_o\-Length\_e\_f/Length\_c\_e\(23\)&Length\_c\_d/Length\_d\_f\-Length\_d\_e/Length\_c\_d\(5\)&Length\_a\_e/Length\_e\_o\-Length\_c\_e/Length\_d\_e\(29\)&Length\_d\_o/Length\_e\_o\-Length\_e\_o/Length\_d\_o⇒\\RightarrowLength\_a\_e\-sqrt\(Length\_d\_f\)\*sqrt\(Length\_e\_f\)/2032\.Length\_a\_f\-sqrt\(Length\_d\_f\)\*sqrt\(Length\_e\_f\)/2\(19\)&Length\_a\_e\-sqrt\(Length\_d\_f\)\*sqrt\(Length\_e\_f\)/2\(31\)⇒\\RightarrowLength\_a\_e\-Length\_a\_f

For the second problem, the natural language formulation is provided below, along with its corresponding diagram in Figure[12](https://arxiv.org/html/2608.14585#A3.F12)\.

[⬇](data:text/plain;base64,TGV0IEJDIGJlIGEgbGluZSBzZWdtZW50LCBhbmQgTyBiZSB0aGUgbWlkcG9pbnQgb2YgQkMuIFBvaW50IEEgbGllcyBvbiBhIGNpcmNsZSB3aXRoIGNlbnRlciBPIGFuZCByYWRpdXMgT0IuIFBvaW50IEQgbGllcyBvbiB0aGUgcGVycGVuZGljdWxhciBiaXNlY3RvciBvZiBsaW5lIHNlZ21lbnQgQUIgYW5kIGlzIGxvY2F0ZWQgb24gdGhlIHNhbWUgY2lyY2xlIHdpdGggY2VudGVyIE8gYW5kIHJhZGl1cyBPQi4gUG9pbnQgRSBpcyBsb2NhdGVkIG9uIHRoZSBwZXJwZW5kaWN1bGFyIGJpc2VjdG9yIG9mIGxpbmUgc2VnbWVudCBPQSBhbmQgYWxzbyBsaWVzIG9uIHRoZSBjaXJjbGUgd2l0aCBjZW50ZXIgTyBhbmQgcmFkaXVzIE9CLiBTaW1pbGFybHksIHBvaW50IEYgaXMgbG9jYXRlZCBvbiB0aGUgcGVycGVuZGljdWxhciBiaXNlY3RvciBvZiBsaW5lIHNlZ21lbnQgT0EgYW5kIGxpZXMgb24gdGhlIGNpcmNsZSB3aXRoIGNlbnRlciBPIGFuZCByYWRpdXMgT0IuIExpbmUgSk8gaXMgcGFyYWxsZWwgdG8gQUQsIGFuZCBwb2ludCBKIGxpZXMgb24gbGluZSBBQy4gUHJvdmUgdGhhdCDiiKBFQ0ogPSDiiKBGQ0ou)LetBCbealinesegment,andObethemidpointofBC\.PointAliesonacirclewithcenterOandradiusOB\.PointDliesontheperpendicularbisectoroflinesegmentABandislocatedonthesamecirclewithcenterOandradiusOB\.PointEislocatedontheperpendicularbisectoroflinesegmentOAandalsoliesonthecirclewithcenterOandradiusOB\.Similarly,pointFislocatedontheperpendicularbisectoroflinesegmentOAandliesonthecirclewithcenterOandradiusOB\.LineJOisparalleltoAD,andpointJliesonlineAC\.Provethat∠\\angleECJ=∠\\angleFCJ\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/imo2002.jpg)Figure 12:Diagram of a geometry problem selected from IMO\-AG\-30\.The proof produced by Euclidea for this problem is shown below:

[⬇](data:text/plain;base64,U29sdXRpb246CjEuIExlbmd0aF9iX28gLSBMZW5ndGhfY19vICYgTGVuZ3RoX2FfbyAtIExlbmd0aF9iX28gPT4gTGVuZ3RoX2FfbyAtIExlbmd0aF9jX28KMi4gTGVuZ3RoX2JfbyAtIExlbmd0aF9mX28gJiBMZW5ndGhfYl9vIC0gTGVuZ3RoX2NfbyA9PiBMZW5ndGhfY19vIC0gTGVuZ3RoX2ZfbwozLiAtTGVuZ3RoX2FfbyArIExlbmd0aF9jX28gJiBMZW5ndGhfY19vIC0gTGVuZ3RoX2ZfbyA9PiBBbmdsZV9hX2NfZiAtIEFuZ2xlX2Ffb19mLzIKNC4gQ29sbGluZWFyKGEsYyxqKSA9PiBBbmdsZV9hX2NfZiAtIEFuZ2xlX2ZfY19qICYgQW5nbGVfYV9jX2UgLSBBbmdsZV9lX2Nfago1LiBMZW5ndGhfYl9vIC0gTGVuZ3RoX2ZfbyAmIExlbmd0aF9iX28gLSBMZW5ndGhfZV9vID0+IExlbmd0aF9lX28gLSBMZW5ndGhfZl9vCjYuIExlbmd0aF9hX2UgLSBMZW5ndGhfZV9vICYgTGVuZ3RoX2VfbyAtIExlbmd0aF9mX28gJiAtTGVuZ3RoX2FfZiArIExlbmd0aF9mX28gPT4gUmhvbWJ1cyhhLGUsbyxmKQo3LiBSaG9tYnVzKGEsZSxvLGYpID0+IEFuZ2xlX2Ffb19lIC0gQW5nbGVfYV9vX2YKOC4gTGVuZ3RoX2JfbyAtIExlbmd0aF9jX28gJiBMZW5ndGhfYl9vIC0gTGVuZ3RoX2VfbyA9PiBMZW5ndGhfY19vIC0gTGVuZ3RoX2Vfbwo5LiAtTGVuZ3RoX2FfbyArIExlbmd0aF9jX28gJiBMZW5ndGhfY19vIC0gTGVuZ3RoX2VfbyA9PiBBbmdsZV9hX2NfZSAtIEFuZ2xlX2Ffb19lLzIKMTAuIEFuZ2xlX2FfY19mIC0gQW5nbGVfYV9vX2YvMiAmIEFuZ2xlX2FfY19mIC0gQW5nbGVfZl9jX2ogJiBBbmdsZV9hX29fZSAtIEFuZ2xlX2Ffb19mICYgQW5nbGVfYV9jX2UgLSBBbmdsZV9hX29fZS8yICYgQW5nbGVfYV9jX2UgLSBBbmdsZV9lX2NfaiA9PiBBbmdsZV9lX2NfaiAtIEFuZ2xlX2ZfY19qCg==)Solution:1\.Length\_b\_o\-Length\_c\_o&Length\_a\_o\-Length\_b\_o=\>Length\_a\_o\-Length\_c\_o2\.Length\_b\_o\-Length\_f\_o&Length\_b\_o\-Length\_c\_o=\>Length\_c\_o\-Length\_f\_o3\.\-Length\_a\_o\+Length\_c\_o&Length\_c\_o\-Length\_f\_o=\>Angle\_a\_c\_f\-Angle\_a\_o\_f/24\.Collinear\(a,c,j\)=\>Angle\_a\_c\_f\-Angle\_f\_c\_j&Angle\_a\_c\_e\-Angle\_e\_c\_j5\.Length\_b\_o\-Length\_f\_o&Length\_b\_o\-Length\_e\_o=\>Length\_e\_o\-Length\_f\_o6\.Length\_a\_e\-Length\_e\_o&Length\_e\_o\-Length\_f\_o&\-Length\_a\_f\+Length\_f\_o=\>Rhombus\(a,e,o,f\)7\.Rhombus\(a,e,o,f\)=\>Angle\_a\_o\_e\-Angle\_a\_o\_f8\.Length\_b\_o\-Length\_c\_o&Length\_b\_o\-Length\_e\_o=\>Length\_c\_o\-Length\_e\_o9\.\-Length\_a\_o\+Length\_c\_o&Length\_c\_o\-Length\_e\_o=\>Angle\_a\_c\_e\-Angle\_a\_o\_e/210\.Angle\_a\_c\_f\-Angle\_a\_o\_f/2&Angle\_a\_c\_f\-Angle\_f\_c\_j&Angle\_a\_o\_e\-Angle\_a\_o\_f&Angle\_a\_c\_e\-Angle\_a\_o\_e/2&Angle\_a\_c\_e\-Angle\_e\_c\_j=\>Angle\_e\_c\_j\-Angle\_f\_c\_j

The proof produced by AlphaGeometry for this problem is shown below:

[⬇](data:text/plain;base64,ICogUHJvb2Ygc3RlcHM6CjAwMS4gT0UgPSBPQiBbMDNdICYgT0YgPSBPQiBbMDVdICYgT0EgPSBPQiBbMDFdICYgT0QgPSBPQiBbMDJdICYgT0IgPSBPQyBbMDBdIOKHkiAgRSxBLEYsQyBhcmUgY29uY3ljbGljIFswOF0KMDAyLiBFLEEsRixDIGFyZSBjb25jeWNsaWMgWzA4XSDih5IgIOKIoEFFRiA9IOKIoEFDRiBbMDldCjAwMy4gRSxBLEYsQyBhcmUgY29uY3ljbGljIFswOF0g4oeSICDiiKBFRkEgPSDiiKBFQ0EgWzEwXQowMDQuIEVPID0gRUEgWzA0XSAmIE9FID0gT0IgWzAzXSAmIE9GID0gT0IgWzA1XSAmIEZPID0gRkEgWzA2XSDih5IgIEFGID0gQUUgWzExXQowMDUuIEFGID0gQUUgWzExXSDih5IgIOKIoEVGQSA9IOKIoEFFRiBbMTJdCjAwNi4gSixBLEMgYXJlIGNvbGxpbmVhciBbMDddICYg4oigQUVGID0g4oigQUNGIFswOV0gJiDiiKBFRkEgPSDiiKBBRUYgWzEyXSAmIOKIoEVGQSA9IOKIoEVDQSBbMTBdIOKHkiAg4oigRUNKID0g4oigSkNG)\*Proofsteps:001\.OE=OB\[03\]&OF=OB\[05\]&OA=OB\[01\]&OD=OB\[02\]&OB=OC\[00\]⇒\\RightarrowE,A,F,Careconcyclic\[08\]002\.E,A,F,Careconcyclic\[08\]⇒\\Rightarrow∠\\angleAEF=∠\\angleACF\[09\]003\.E,A,F,Careconcyclic\[08\]⇒\\Rightarrow∠\\angleEFA=∠\\angleECA\[10\]004\.EO=EA\[04\]&OE=OB\[03\]&OF=OB\[05\]&FO=FA\[06\]⇒\\RightarrowAF=AE\[11\]005\.AF=AE\[11\]⇒\\Rightarrow∠\\angleEFA=∠\\angleAEF\[12\]006\.J,A,Carecollinear\[07\]&∠\\angleAEF=∠\\angleACF\[09\]&∠\\angleEFA=∠\\angleAEF\[12\]&∠\\angleEFA=∠\\angleECA\[10\]⇒\\Rightarrow∠\\angleECJ=∠\\angleJCF

The proof produced by Newclid for this problem is shown below:

[⬇](data:text/plain;base64,IyBQcm9vZjoKMDAwLiB8IE8gaXMgdGhlIG1pZHBvaW50IG9mIEJDIFtDMV0gPShyNTEgTWlkcG9pbnQgc3BsaXRzIGluIHR3byk+IEJDOkJPID0gMi8xIFswXQowMDEuIHwgTyBpcyB0aGUgbWlkcG9pbnQgb2YgQkMgW0MxXSA9KHI1MSBNaWRwb2ludCBzcGxpdHMgaW4gdHdvKT4gQkM6Q08gPSAyLzEgWzFdCjAwMi4gfCBBTyA9IEJPIFtDMF0sIEJDOkJPID0gMi8xIFswXSwgQkM6Q08gPSAyLzEgWzFdID0oQVIgRGVkdWN0aW9uKT4gQ08gPSBBTyBbMl0KMDAzLiB8IENPID0gQU8gWzJdID0ocjEzIElzb3NjZWxlcyB0cmlhbmdsZSBlcXVhbCBhbmdsZXMpPiAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEFDLEFPKX1AKikgPSAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKENPLEFDKX1AKikgWzNdCjAwNC4gfCAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEFFLEFPKX1AKikgPSAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEFPLEVPKX1AKikgW0MzXSwgKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChBRixBTyl9QCopID0gKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChBTyxGTyl9QCopIFtDMl0gPShBUiBEZWR1Y3Rpb24pPiAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEFFLEFGKX1AKikgPSAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEZPLEVPKX1AKikgWzRdCjAwNS4gfCBBRSA9IEVPIFtDNF0sIEVPID0gQk8gW0M1XSwgRk8gPSBBRiBbQzZdLCBGTyA9IEJPIFtDN10gPShBUiBEZWR1Y3Rpb24pPiBBRTpBRiA9IEZPOkVPIFs1XQowMDYuIHwgKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChBRSxBRil9QCopID0gKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChGTyxFTyl9QCopIFs0XSwgQUU6QUYgPSBGTzpFTyBbNV0sIOKWskFFRiBoYXMgdGhlIHNhbWUgb3JpZW50YXRpb24gYXMg4payRU9GIFtOMF0gPShyNjIgU0FTIFNpbWlsYXJpdHkgb2YgdHJpYW5nbGVzIChEaXJlY3QpKT4g4payQUVGIOKJhSDilrJPRkUgWzZdCjAwNy4gfCDilrJBRUYgaGFzIHRoZSBzYW1lIG9yaWVudGF0aW9uIGFzIOKWskVPRiBbTjBdLCDilrJBRUYg4omFIOKWsk9GRSBbNl0gPShyNTIgUHJvcGVydGllcyBvZiBzaW1pbGFyIHRyaWFuZ2xlcyAoRGlyZWN0KSk+ICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoQUYsRUYpfUAqKSA9ICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoRU8sRUYpfUAqKSBbN10KMDA4LiB8IEVPID0gQk8gW0M1XSwgQkM6Qk8gPSAyLzEgWzBdLCBCQzpDTyA9IDIvMSBbMV0gPShBUiBEZWR1Y3Rpb24pPiBFTyA9IENPIFs4XQowMDkuIHwgRU8gPSBDTyBbOF0gPShyMTMgSXNvc2NlbGVzIHRyaWFuZ2xlIGVxdWFsIGFuZ2xlcyk+ICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoQ0UsQ08pfUAqKSA9ICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoRU8sQ0UpfUAqKSBbOV0KMDEwLiB8IEZPID0gQk8gW0M3XSwgQkM6Qk8gPSAyLzEgWzBdLCBCQzpDTyA9IDIvMSBbMV0gPShBUiBEZWR1Y3Rpb24pPiBDTyA9IEZPIFsxMF0KMDExLiB8IENPID0gRk8gWzEwXSA9KHIxMyBJc29zY2VsZXMgdHJpYW5nbGUgZXF1YWwgYW5nbGVzKT4gKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChDRixDTyl9QCopID0gKCpAXHRleHRjb2xvcntibHVlfXskXGFuZ2xlJChGTyxDRil9QCopIFsxMV0KMDEyLiB8IEEsIEMsIEogYXJlIGNvbGxpbmVhciBbQzhdLCBBIOKJoCBDIFtOMV0sIEEg4omgIEogW04yXSwgQyDiiaAgSiBbTjNdID0ocjgyIFBhcmFsbGVsIGZyb20gY29sbGluZWFyKT4gQ0og4oilIEFDIFsxMl0KMDEzLiB8ICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoQUMsQU8pfUAqKSA9ICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoQ08sQUMpfUAqKSBbM10sICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoQUYsQU8pfUAqKSA9ICgqQFx0ZXh0Y29sb3J7Ymx1ZX17JFxhbmdsZSQoQU8sRk8pfUAqKSBbQzJdLCAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEFGLEVGKX1AKikgPSAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEVPLEVGKX1AKikgWzddLCAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKENFLENPKX1AKikgPSAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEVPLENFKX1AKikgWzldLCAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKENGLENPKX1AKikgPSAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKEZPLENGKX1AKikgWzExXSwgQ0og4oilIEFDIFsxMl0gPShBUiBEZWR1Y3Rpb24pPiAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKENFLENKKX1AKikgPSAoKkBcdGV4dGNvbG9ye2JsdWV9eyRcYW5nbGUkKENKLENGKX1AKikgWzEzXQ==)\#Proof:000\.\|OisthemidpointofBC\[C1\]=\(r51Midpointsplitsintwo\)\>BC:BO=2/1\[0\]001\.\|OisthemidpointofBC\[C1\]=\(r51Midpointsplitsintwo\)\>BC:CO=2/1\[1\]002\.\|AO=BO\[C0\],BC:BO=2/1\[0\],BC:CO=2/1\[1\]=\(ARDeduction\)\>CO=AO\[2\]003\.\|CO=AO\[2\]=\(r13Isoscelestriangleequalangles\)\>∠\\angle\(AC,AO\)=∠\\angle\(CO,AC\)\[3\]004\.\|∠\\angle\(AE,AO\)=∠\\angle\(AO,EO\)\[C3\],∠\\angle\(AF,AO\)=∠\\angle\(AO,FO\)\[C2\]=\(ARDeduction\)\>∠\\angle\(AE,AF\)=∠\\angle\(FO,EO\)\[4\]005\.\|AE=EO\[C4\],EO=BO\[C5\],FO=AF\[C6\],FO=BO\[C7\]=\(ARDeduction\)\>AE:AF=FO:EO\[5\]006\.\|∠\\angle\(AE,AF\)=∠\\angle\(FO,EO\)\[4\],AE:AF=FO:EO\[5\],△\\triangleAEFhasthesameorientationas△\\triangleEOF\[N0\]=\(r62SASSimilarityoftriangles\(Direct\)\)\>△\\triangleAEF≅\\cong△\\triangleOFE\[6\]007\.\|△\\triangleAEFhasthesameorientationas△\\triangleEOF\[N0\],△\\triangleAEF≅\\cong△\\triangleOFE\[6\]=\(r52Propertiesofsimilartriangles\(Direct\)\)\>∠\\angle\(AF,EF\)=∠\\angle\(EO,EF\)\[7\]008\.\|EO=BO\[C5\],BC:BO=2/1\[0\],BC:CO=2/1\[1\]=\(ARDeduction\)\>EO=CO\[8\]009\.\|EO=CO\[8\]=\(r13Isoscelestriangleequalangles\)\>∠\\angle\(CE,CO\)=∠\\angle\(EO,CE\)\[9\]010\.\|FO=BO\[C7\],BC:BO=2/1\[0\],BC:CO=2/1\[1\]=\(ARDeduction\)\>CO=FO\[10\]011\.\|CO=FO\[10\]=\(r13Isoscelestriangleequalangles\)\>∠\\angle\(CF,CO\)=∠\\angle\(FO,CF\)\[11\]012\.\|A,C,Jarecollinear\[C8\],A≠\\neqC\[N1\],A≠\\neqJ\[N2\],C≠\\neqJ\[N3\]=\(r82Parallelfromcollinear\)\>CJ∥\\parallelAC\[12\]013\.\|∠\\angle\(AC,AO\)=∠\\angle\(CO,AC\)\[3\],∠\\angle\(AF,AO\)=∠\\angle\(AO,FO\)\[C2\],∠\\angle\(AF,EF\)=∠\\angle\(EO,EF\)\[7\],∠\\angle\(CE,CO\)=∠\\angle\(EO,CE\)\[9\],∠\\angle\(CF,CO\)=∠\\angle\(FO,CF\)\[11\],CJ∥\\parallelAC\[12\]=\(ARDeduction\)\>∠\\angle\(CE,CJ\)=∠\\angle\(CJ,CF\)\[13\]

The proof produced by PyEuclid for this problem is shown below:

[⬇](data:text/plain;base64,KiBQcm9vZiBzdGVwczoKMDAxLiBMZW5ndGhfYV9vIC0gTGVuZ3RoX2JfbyAmCi1MZW5ndGhfYl9vICsgTGVuZ3RoX2ZfbyDih5IgTGVuZ3RoX2FfbyAtIExlbmd0aF9mX28KMDAyLiAtTGVuZ3RoX2FfZSArIExlbmd0aF9lX28gJgotTGVuZ3RoX2JfbyArIExlbmd0aF9lX28gJgotTGVuZ3RoX2JfbyArIExlbmd0aF9mX28g4oeSIExlbmd0aF9hX2UgLSBMZW5ndGhfZl9vCjAwMy4gTGVuZ3RoX2FfbyAtIExlbmd0aF9mX28oMSkgJgpMZW5ndGhfYV9lIC0gTGVuZ3RoX2ZfbygyKSDih5IgTGVuZ3RoX2FfZSAtIExlbmd0aF9hX28KMDA0LiBOb3QoQ29sbGluZWFyKGEsZSxvKSkgJgpMZW5ndGhfYV9lIC0gTGVuZ3RoX2FfbygzKSDih5IgQW5nbGVfYV9lX28gLSBBbmdsZV9hX29fZQowMDUuIC1MZW5ndGhfYl9vICsgTGVuZ3RoX2VfbyAmCi1MZW5ndGhfYl9vICsgTGVuZ3RoX2ZfbyDih5IgTGVuZ3RoX2VfbyAtIExlbmd0aF9mX28KMDA2LiBOb3QoQ29sbGluZWFyKGEsZSxvKSkgJgpMZW5ndGhfYV9lIC0gTGVuZ3RoX2VfbyDih5IgLUFuZ2xlX2Ffb19lICsgQW5nbGVfZV9hX28KMDA3LiBMZW5ndGhfYl9vIC0gTGVuZ3RoX2NfbyAmCi1MZW5ndGhfYl9vICsgTGVuZ3RoX2ZfbyDih5IgTGVuZ3RoX2NfbyAtIExlbmd0aF9mX28KMDA4LiBMZW5ndGhfYV9vIC0gTGVuZ3RoX2ZfbygxKSAmCkxlbmd0aF9jX28gLSBMZW5ndGhfZl9vKDcpIOKHkiBMZW5ndGhfYV9vIC0gTGVuZ3RoX2NfbwowMDkuIExlbmd0aF9lX28gLSBMZW5ndGhfZl9vKDUpICYKTGVuZ3RoX2NfbyAtIExlbmd0aF9mX28oNykg4oeSIExlbmd0aF9jX28gLSBMZW5ndGhfZV9vCjAxMC4gU2FtZVNpZGUoYyxvLGEsZSkgJgpMZW5ndGhfYV9vIC0gTGVuZ3RoX2Nfbyg4KSAmCkxlbmd0aF9jX28gLSBMZW5ndGhfZV9vKDkpIOKHkiBBbmdsZV9hX2NfZSAtIEFuZ2xlX2Ffb19lLzIKMDExLiBBbmdsZV9hX2NfZSAtIEFuZ2xlX2VfY19qICYKQW5nbGVfYV9lX28gKyBBbmdsZV9hX29fZSArIEFuZ2xlX2VfYV9vIC0gcGkgJgpBbmdsZV9hX2VfbyAtIEFuZ2xlX2Ffb19lKDQpICYKLUFuZ2xlX2Ffb19lICsgQW5nbGVfZV9hX28oNikgJgpBbmdsZV9hX2NfZSAtIEFuZ2xlX2Ffb19lLzIoMTApIOKHkiBBbmdsZV9lX2NfaiAtIHBpLzYKMDEyLiBMZW5ndGhfYV9vIC0gTGVuZ3RoX2ZfbygxKSAmCkxlbmd0aF9hX2YgLSBMZW5ndGhfZl9vIOKHkiBMZW5ndGhfYV9mIC0gTGVuZ3RoX2FfbwowMTMuIE5vdChDb2xsaW5lYXIoYSxmLG8pKSAmCkxlbmd0aF9hX2YgLSBMZW5ndGhfYV9vKDEyKSDih5IgQW5nbGVfYV9mX28gLSBBbmdsZV9hX29fZgowMTQuIE5vdChDb2xsaW5lYXIoYSxmLG8pKSAmCkxlbmd0aF9hX2YgLSBMZW5ndGhfZl9vIOKHkiAtQW5nbGVfYV9vX2YgKyBBbmdsZV9mX2FfbwowMTUuIFNhbWVTaWRlKGMsbyxhLGYpICYKTGVuZ3RoX2FfbyAtIExlbmd0aF9jX28oOCkgJgpMZW5ndGhfY19vIC0gTGVuZ3RoX2ZfbyDih5IgQW5nbGVfYV9jX2YgLSBBbmdsZV9hX29fZi8yCjAxNi4gQW5nbGVfYV9jX2YgLSBBbmdsZV9mX2NfaiAmCkFuZ2xlX2FfZl9vICsgQW5nbGVfYV9vX2YgKyBBbmdsZV9mX2FfbyAtIHBpICYKQW5nbGVfYV9mX28gLSBBbmdsZV9hX29fZigxMykgJgotQW5nbGVfYV9vX2YgKyBBbmdsZV9mX2FfbygxNCkgJgpBbmdsZV9hX2NfZiAtIEFuZ2xlX2Ffb19mLzIoMTUpIOKHkiBBbmdsZV9mX2NfaiAtIHBpLzYKMDE3LiBBbmdsZV9lX2NfaiAtIHBpLzYoMTEpICYKQW5nbGVfZl9jX2ogLSBwaS82KDE2KSDih5IgQW5nbGVfZV9jX2ogLSBBbmdsZV9mX2Nfag==)\*Proofsteps:001\.Length\_a\_o\-Length\_b\_o&\-Length\_b\_o\+Length\_f\_o⇒\\RightarrowLength\_a\_o\-Length\_f\_o002\.\-Length\_a\_e\+Length\_e\_o&\-Length\_b\_o\+Length\_e\_o&\-Length\_b\_o\+Length\_f\_o⇒\\RightarrowLength\_a\_e\-Length\_f\_o003\.Length\_a\_o\-Length\_f\_o\(1\)&Length\_a\_e\-Length\_f\_o\(2\)⇒\\RightarrowLength\_a\_e\-Length\_a\_o004\.Not\(Collinear\(a,e,o\)\)&Length\_a\_e\-Length\_a\_o\(3\)⇒\\RightarrowAngle\_a\_e\_o\-Angle\_a\_o\_e005\.\-Length\_b\_o\+Length\_e\_o&\-Length\_b\_o\+Length\_f\_o⇒\\RightarrowLength\_e\_o\-Length\_f\_o006\.Not\(Collinear\(a,e,o\)\)&Length\_a\_e\-Length\_e\_o⇒\\Rightarrow\-Angle\_a\_o\_e\+Angle\_e\_a\_o007\.Length\_b\_o\-Length\_c\_o&\-Length\_b\_o\+Length\_f\_o⇒\\RightarrowLength\_c\_o\-Length\_f\_o008\.Length\_a\_o\-Length\_f\_o\(1\)&Length\_c\_o\-Length\_f\_o\(7\)⇒\\RightarrowLength\_a\_o\-Length\_c\_o009\.Length\_e\_o\-Length\_f\_o\(5\)&Length\_c\_o\-Length\_f\_o\(7\)⇒\\RightarrowLength\_c\_o\-Length\_e\_o010\.SameSide\(c,o,a,e\)&Length\_a\_o\-Length\_c\_o\(8\)&Length\_c\_o\-Length\_e\_o\(9\)⇒\\RightarrowAngle\_a\_c\_e\-Angle\_a\_o\_e/2011\.Angle\_a\_c\_e\-Angle\_e\_c\_j&Angle\_a\_e\_o\+Angle\_a\_o\_e\+Angle\_e\_a\_o\-pi&Angle\_a\_e\_o\-Angle\_a\_o\_e\(4\)&\-Angle\_a\_o\_e\+Angle\_e\_a\_o\(6\)&Angle\_a\_c\_e\-Angle\_a\_o\_e/2\(10\)⇒\\RightarrowAngle\_e\_c\_j\-pi/6012\.Length\_a\_o\-Length\_f\_o\(1\)&Length\_a\_f\-Length\_f\_o⇒\\RightarrowLength\_a\_f\-Length\_a\_o013\.Not\(Collinear\(a,f,o\)\)&Length\_a\_f\-Length\_a\_o\(12\)⇒\\RightarrowAngle\_a\_f\_o\-Angle\_a\_o\_f014\.Not\(Collinear\(a,f,o\)\)&Length\_a\_f\-Length\_f\_o⇒\\Rightarrow\-Angle\_a\_o\_f\+Angle\_f\_a\_o015\.SameSide\(c,o,a,f\)&Length\_a\_o\-Length\_c\_o\(8\)&Length\_c\_o\-Length\_f\_o⇒\\RightarrowAngle\_a\_c\_f\-Angle\_a\_o\_f/2016\.Angle\_a\_c\_f\-Angle\_f\_c\_j&Angle\_a\_f\_o\+Angle\_a\_o\_f\+Angle\_f\_a\_o\-pi&Angle\_a\_f\_o\-Angle\_a\_o\_f\(13\)&\-Angle\_a\_o\_f\+Angle\_f\_a\_o\(14\)&Angle\_a\_c\_f\-Angle\_a\_o\_f/2\(15\)⇒\\RightarrowAngle\_f\_c\_j\-pi/6017\.Angle\_e\_c\_j\-pi/6\(11\)&Angle\_f\_c\_j\-pi/6\(16\)⇒\\RightarrowAngle\_e\_c\_j\-Angle\_f\_c\_j

It is important to note that proofs generated by different systems can vary substantially in both style and strategy\. In contrast to Euclidea, AlphaGeometry and Newclid rely on full\-angle formalization\[[14](https://arxiv.org/html/2608.14585#bib.bib14)\], which often fails to distinguish an angle from its supplement and may therefore yield “incorrect” angle relations compared to human reasoning \(highlighted in red\)\. Furthermore, these systems represent angles as pairs of lines \(shown in blue\), which introduces additional ambiguity\. By comparison, the proofs generated by Euclidea faithfully capture the angle relations shown in the diagram, yielding a more human\-like representation\. Compared to PyEuclid, Euclidea produces proofs that are about twice as compact and avoid redundant equations, making them significantly clearer and easier for humans to read\.

### C\.2Ablation Study over Training Datasets

To perform a controlled ablation, we fine\-tune Qwen2\.5\-VL\-7B\[[2](https://arxiv.org/html/2608.14585#bib.bib2)\]on several open\-source datasets under matched training settings\. We consider Geo170K\[[21](https://arxiv.org/html/2608.14585#bib.bib21)\], GeoGen\[[39](https://arxiv.org/html/2608.14585#bib.bib39)\], and TR\-CoT\[[17](https://arxiv.org/html/2608.14585#bib.bib17)\]\. Concretely, we train models on 20K subsets of Geo170K, GeoGen, and TR\-CoT, as well as two 20K mixtures \(10K Geo170K \+ 10K GeoGen and 10K Geo170K \+ 10K TR\-CoT\)\. We additionally fine\-tune on Ours 10K as an ablation\.

Table 5:Accuracy \(%\) on four benchmarks under different training data choices\.Training DataGeoQAGeometry3KMathVistaMathVerseQwen2\.5\-VL\-7B \(no fine\-tuning\)69\.456\.472\.244\.1Geo170K 20K75\.057\.870\.150\.4GeoGen 20K73\.145\.163\.640\.2TR\-CoT 20K75\.057\.372\.147\.8Geo170K 10K \+ GeoGen 10K75\.359\.862\.944\.9Geo170K 10K \+ TR\-CoT 10K72\.855\.274\.044\.5Ours 10K74\.763\.672\.150\.4Geo170K 10K \+ Ours 10K76\.661\.074\.751\.0Table[5](https://arxiv.org/html/2608.14585#A3.T5)show that, under comparable compute, Euclid\-Omni data consistently yields competitive or superior performance, especially on the Geometry3K dataset\. This demonstrates that high\-fidelity, symbolically verified constructions, rather than simply increasing dataset size, are essential for improving VLM performance on geometry reasoning benchmarks\.

### C\.3Examples of Generated Natural Language Solutions

We provide two examples from the GeoQA\[[5](https://arxiv.org/html/2608.14585#bib.bib5)\]and Geometry3K\[[30](https://arxiv.org/html/2608.14585#bib.bib30)\]datasets and compare the solutions generated by our finetuned model with those produced by the base model Qwen2\.5\-VL\[[2](https://arxiv.org/html/2608.14585#bib.bib2)\]\. The results illustrate that training on our synthetic dataset improves the model’s ability to understand and solve informal geometry problems\.

The natural language description of the problem from the GeoQA dataset is presented below, with the corresponding diagram shown in Figure[13](https://arxiv.org/html/2608.14585#A3.F13)\. This example demonstrates that our model correctly interprets diagrammatic relationships through finetuning\.

[⬇](data:text/plain;base64,QXMgc2hvd24gaW4gdGhlIGZpZ3VyZSwgaXQgaXMga25vd24gdGhhdCBCQSBpcyB0aGUgdGFuZ2VudCBvZiBjaXJjbGUgTywgYW5kIGNvbm5lY3QgT0IgdG8gaW50ZXJzZWN0IGNpcmNsZSBPIGF0IHBvaW50IEMuIElmIGFuZ2xlIEIgPSA0NS4wIGFuZCB0aGUgbGVuZ3RoIG9mIEFCIGlzIDIuMCwgdGhlbiB0aGUgbGVuZ3RoIG9mIEJDIGlzICgpCkNob2ljZXM6CkE6MlxzcXJ0ezJ9LTEKQjpcc3FydHsyfQpDOjJcc3FydHsyfS0yCkQ6Mi1cc3FydHsyfQ==)Asshowninthefigure,itisknownthatBAisthetangentofcircleO,andconnectOBtointersectcircleOatpointC\.IfangleB=45\.0andthelengthofABis2\.0,thenthelengthofBCis\(\)Choices:A:2\\sqrt\{2\}\-1B:\\sqrt\{2\}C:2\\sqrt\{2\}\-2D:2\-\\sqrt\{2\}

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/geoqa_272.png)Figure 13:Diagram of a problem selected from GeoQA\.The solution produced by our model for this problem is shown below:

[⬇](data:text/plain;base64,U2luY2UgQkEgaXMgYSB0YW5nZW50IGxpbmUgdG8gY2lyY2xlIE8sIHdlIGhhdmUgT0EgcGVycGVuZGljdWxhciB0byBBQi4gR2l2ZW4gdGhhdCBhbmdsZSBCIGlzIDQ1IGRlZ3JlZXMsIHdlIGNhbiBmaW5kIHRoYXQgT0EgZXF1YWxzIEFCLCB3aGljaCBpcyAyLiBJbiByaWdodCB0cmlhbmdsZSBBT0IsIHVzaW5nIHRoZSBQeXRoYWdvcmVhbiB0aGVvcmVtLCB3ZSBjYW4gZmluZCBPQiBhcyBcc3FydHtPQV4yK0FCXjJ9LCB3aGljaCBlcXVhbHMgMlxzcXJ0ezJ9LiBUaGVyZWZvcmUsIEJDIGVxdWFscyBPQiBtaW51cyBPQywgd2hpY2ggaXMgMlxzcXJ0ezJ9LTIuIEhlbmNlLCB0aGUgYW5zd2VyIGlzIFxib3hlZHtDfQ==)SinceBAisatangentlinetocircleO,wehaveOAperpendiculartoAB\.GiventhatangleBis45degrees,wecanfindthatOAequalsAB,whichis2\.InrighttriangleAOB,usingthePythagoreantheorem,wecanfindOBas\\sqrt\{OA^2\+AB^2\},whichequals2\\sqrt\{2\}\.Therefore,BCequalsOBminusOC,whichis2\\sqrt\{2\}\-2\.Hence,theansweris\\boxed\{C\}

The solution produced by the base model for this problem is shown below:

[⬇](data:text/plain;base64,U2luY2UgQUIgaXMgYSB0YW5nZW50IGxpbmUgdG8gY2lyY2xlIE8sIHdlIGhhdmUgT0EgcGVycGVuZGljdWxhciAgQUIuIEluIHJpZ2h0IHRyaWFuZ2xlIEFPQiwgd2Uga25vdyB0aGF0IGFuZ2xlIEIgaXMgNDXCsCBhbmQgQUIgaXMgMi4gVGhlcmVmb3JlLCBPQSA9IE9CID0gQUIgKiBzaW4oNDXCsCkgPSBcc3FydHsyfS4gSGVuY2UsIE9DID0gT0EgPSBcc3FydHsyfS4gVGh1cywgQkMgPSBPQiAtIE9DID0gKFxzcXJ0ezJ9KSAtIChcc3FydHsyfSkvMiA9IChcc3FydHsyfSkvMi4gVGhlcmVmb3JlLCB0aGUgYW5zd2VyIGlzIG9wdGlvbiBELgpBbnN3ZXI6RA==)SinceABisatangentlinetocircleO,wehaveOAperpendicularAB\.InrighttriangleAOB,weknowthatangleBis45∘andABis2\.Therefore,OA=OB=AB\*sin\(45∘\)=\\sqrt\{2\}\.Hence,OC=OA=\\sqrt\{2\}\.Thus,BC=OB\-OC=\(\\sqrt\{2\}\)\-\(\\sqrt\{2\}\)/2=\(\\sqrt\{2\}\)/2\.Therefore,theanswerisoptionD\.Answer:D

The natural language version of the problem from the Geometry3K dataset is given below, and its corresponding diagram is shown in Figure[14](https://arxiv.org/html/2608.14585#A3.F14)\. This example shows that our model can perform algebraic computation robustly after training on the synthetic dataset\.

[⬇](data:text/plain;base64,RmluZCAkbVxhbmdsZSBSJC4=)Find$m\\angleR$\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/geo3k_2489.png)Figure 14:Diagram of a problem selected from Geometry3K\.The solution produced by our model for this problem is shown below:

[⬇](data:text/plain;base64,VG8gZmluZCB0aGUgbWVhc3VyZSBvZiBhbmdsZSBcKCBcYW5nbGUgUiBcKSwgd2UgbmVlZCB0byB1c2UgdGhlIGZhY3QgdGhhdCB0aGUgc3VtIG9mIHRoZSBpbnRlcmlvciBhbmdsZXMgb2YgYSBxdWFkcmlsYXRlcmFsIGlzIGFsd2F5cyAzNjAgZGVncmVlcy4KCkdpdmVuIHRoZSBhbmdsZXMgaW4gdGhlIHF1YWRyaWxhdGVyYWw6Ci0gXCggXGFuZ2xlIFEgPSAoMnggKyA1KV5cY2lyYyBcKQotIFwoIFxhbmdsZSBSID0geF5cY2lyYyBcKQotIFwoIFxhbmdsZSBTID0gKDJ4ICsgNyleXGNpcmMgXCkKLSBcKCBcYW5nbGUgVCA9IHheXGNpcmMgXCkKCldlIGNhbiBzZXQgdXAgdGhlIGVxdWF0aW9uIGZvciB0aGUgc3VtIG9mIHRoZSBpbnRlcmlvciBhbmdsZXM6ClxbCigyeCArIDUpICsgeCArICgyeCArIDcpICsgeCA9IDM2MApcXQoKQ29tYmluZSBsaWtlIHRlcm1zOgpcWwoyeCArIDUgKyB4ICsgMnggKyA3ICsgeCA9IDM2MApcXQpcWwo2eCArIDEyID0gMzYwClxdCgpTdWJ0cmFjdCAxMiBmcm9tIGJvdGggc2lkZXM6ClxbCjZ4ID0gMzQ4ClxdCgpEaXZpZGUgYnkgNjoKXFsKeCA9IDU4ClxdCgpOb3csIHN1YnN0aXR1dGUgXCggeCA9IDU4IFwpIGJhY2sgaW50byB0aGUgZXhwcmVzc2lvbiBmb3IgXCggXGFuZ2xlIFIgXCk6ClxbClxhbmdsZSBSID0geF5cY2lyYyA9IDU4XlxjaXJjClxdCgpUaHVzLCB0aGUgbWVhc3VyZSBvZiBcKCBcYW5nbGUgUiBcKSBpczoKXFsKXGJveGVkezU4fQpcXQ==)Tofindthemeasureofangle\\\(\\angleR\\\),weneedtousethefactthatthesumoftheinterioranglesofaquadrilateralisalways360degrees\.Giventheanglesinthequadrilateral:\-\\\(\\angleQ=\(2x\+5\)^\\circ\\\)\-\\\(\\angleR=x^\\circ\\\)\-\\\(\\angleS=\(2x\+7\)^\\circ\\\)\-\\\(\\angleT=x^\\circ\\\)Wecansetuptheequationforthesumoftheinteriorangles:\\\[\(2x\+5\)\+x\+\(2x\+7\)\+x=360\\\]Combineliketerms:\\\[2x\+5\+x\+2x\+7\+x=360\\\]\\\[6x\+12=360\\\]Subtract12frombothsides:\\\[6x=348\\\]Divideby6:\\\[x=58\\\]Now,substitute\\\(x=58\\\)backintotheexpressionfor\\\(\\angleR\\\):\\\[\\angleR=x^\\circ=58^\\circ\\\]Thus,themeasureof\\\(\\angleR\\\)is:\\\[\\boxed\{58\}\\\]

The solution produced by the base model for this problem is shown below:

[⬇](data:text/plain;base64,VG8gZmluZCB0aGUgbWVhc3VyZSBvZiBhbmdsZSBcKCBcYW5nbGUgUiBcKSBpbiB0aGUgZ2l2ZW4gcXVhZHJpbGF0ZXJhbCwgd2UgbmVlZCB0byB1c2UgdGhlIGZhY3QgdGhhdCB0aGUgc3VtIG9mIHRoZSBpbnRlcmlvciBhbmdsZXMgb2YgYSBxdWFkcmlsYXRlcmFsIGlzIGFsd2F5cyBcKCAzNjBeXGNpcmMgXCkuCgpUaGUgZ2l2ZW4gYW5nbGVzIGFyZToKLSBcKCBcYW5nbGUgUSA9ICgyeCArIDUpXlxjaXJjIFwpCi0gXCggXGFuZ2xlIFMgPSAoMnggKyA3KV5cY2lyYyBcKQotIFwoIFxhbmdsZSBUID0geF5cY2lyYyBcKQotIFwoIFxhbmdsZSBSID0geF5cY2lyYyBcKQoKV2UgY2FuIHNldCB1cCB0aGUgZXF1YXRpb24gZm9yIHRoZSBzdW0gb2YgdGhlIGludGVyaW9yIGFuZ2xlczoKClxbCigyeCArIDUpICsgKDJ4ICsgNykgKyB4ICsgeCA9IDM2MApcXQoKQ29tYmluZSBsaWtlIHRlcm1zOgoKXFsKMnggKyA1ICsgMnggKyA3ICsgeCArIHggPSAzNjAKXF0KClxbCjR4ICsgMTIgPSAzNjAKXF0KClN1YnRyYWN0IDEyIGZyb20gYm90aCBzaWRlczoKClxbCjR4ID0gMzQ4ClxdCgpEaXZpZGUgYnkgNDoKClxbCnggPSA4NwpcXQoKTm93LCBzdWJzdGl0dXRlIFwoIHggPSA4NyBcKSBiYWNrIGludG8gdGhlIGV4cHJlc3Npb24gZm9yIFwoIFxhbmdsZSBSIFwpOgoKXFsKXGFuZ2xlIFIgPSB4XlxjaXJjID0gODdeXGNpcmMKXF0KClRodXMsIHRoZSBtZWFzdXJlIG9mIFwoIFxhbmdsZSBSIFwpIGlzOgoKXFsKXGJveGVkezg3fQpcXQ==)Tofindthemeasureofangle\\\(\\angleR\\\)inthegivenquadrilateral,weneedtousethefactthatthesumoftheinterioranglesofaquadrilateralisalways\\\(360^\\circ\\\)\.Thegivenanglesare:\-\\\(\\angleQ=\(2x\+5\)^\\circ\\\)\-\\\(\\angleS=\(2x\+7\)^\\circ\\\)\-\\\(\\angleT=x^\\circ\\\)\-\\\(\\angleR=x^\\circ\\\)Wecansetuptheequationforthesumoftheinteriorangles:\\\[\(2x\+5\)\+\(2x\+7\)\+x\+x=360\\\]Combineliketerms:\\\[2x\+5\+2x\+7\+x\+x=360\\\]\\\[4x\+12=360\\\]Subtract12frombothsides:\\\[4x=348\\\]Divideby4:\\\[x=87\\\]Now,substitute\\\(x=87\\\)backintotheexpressionfor\\\(\\angleR\\\):\\\[\\angleR=x^\\circ=87^\\circ\\\]Thus,themeasureof\\\(\\angleR\\\)is:\\\[\\boxed\{87\}\\\]

### C\.4Examples of Generated Formal Auxiliary Constructions

We compared the auxiliary constructions identified by AlphaGeometry\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]with those generated by our approach\. Notably, our predicted constructions often differ from those of AlphaGeometry, highlighting that multiple valid auxiliary strategies can achieve the same goal\. Moreover, our method sometimes requires fewer auxiliary constructions than AlphaGeometry\. To illustrate these differences, we present two examples from the IMO\-AG\-30 dataset\[[45](https://arxiv.org/html/2608.14585#bib.bib45)\]\.

The natural language formulation of the first problem is given below, and the corresponding diagram is shown in Figure[15](https://arxiv.org/html/2608.14585#A3.F15)\.

[⬇](data:text/plain;base64,SW4gdHJpYW5nbGUgQUJDLCBwb2ludCBPIGlzIHRoZSBtaWRwb2ludCBvZiBzaWRlIEJDLiBQb2ludCBNIGxpZXMgb24gdGhlIGNpcmNsZSBjZW50ZXJlZCBhdCBPIHdpdGggcmFkaXVzIE9CLCBhbmQgTSBpcyBsb2NhdGVkIG9uIGxpbmUgQUIuIFBvaW50IE4gbGllcyBvbiB0aGUgY2lyY2xlIGNlbnRlcmVkIGF0IE8gd2l0aCByYWRpdXMgT0IsIGFuZCBOIGlzIGxvY2F0ZWQgb24gbGluZSBBQy4gUG9pbnQgUiBsaWVzIG9uIHRoZSBhbmdsZSBiaXNlY3RvciBvZiDiiKBCQUMsIHN1Y2ggdGhhdCDiiKBNT1IgPSDiiKBST04uIExldCBPXzEgYmUgdGhlIGNlbnRlciBvZiB0aGUgY2lyY2xlIHBhc3NpbmcgdGhyb3VnaCBwb2ludHMgQiwgTSwgYW5kIFIsIGFuZCBPXzIgYmUgdGhlIGNpcmN1bWNlbnRlciBvZiB0cmlhbmdsZSBDTlIuIFBvaW50IFAgbGllcyBvbiB0aGUgY2lyY2xlIGNlbnRlcmVkIGF0IE9fMSB3aXRoIHJhZGl1cyBPXzFSLCBhbmQgUCBhbHNvIGxpZXMgb24gdGhlIGNpcmNsZSBjZW50ZXJlZCBhdCBPXzIgd2l0aCByYWRpdXMgT18yUi4gUHJvdmUgdGhhdCB0aGUgcG9pbnRzIEIsIEMsIGFuZCBQIGFyZSBjb2xsaW5lYXIu)IntriangleABC,pointOisthemidpointofsideBC\.PointMliesonthecirclecenteredatOwithradiusOB,andMislocatedonlineAB\.PointNliesonthecirclecenteredatOwithradiusOB,andNislocatedonlineAC\.PointRliesontheanglebisectorof∠\\angleBAC,suchthat∠\\angleMOR=∠\\angleRON\.LetO\_1bethecenterofthecirclepassingthroughpointsB,M,andR,andO\_2bethecircumcenteroftriangleCNR\.PointPliesonthecirclecenteredatO\_1withradiusO\_1R,andPalsoliesonthecirclecenteredatO\_2withradiusO\_2R\.ProvethatthepointsB,C,andParecollinear\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/imo2004.jpg)Figure 15:Diagram of a geometry problem selected from IMO\-AG\-30\.The auxiliary constructions predicted by our LLM for this problem are shown below\.

[⬇](data:text/plain;base64,Q29uc3RydWN0IHBvaW50IEsgYXMgdGhlIGNpcmN1bWNlbnRlciBvZiB0cmlhbmdsZSBBTU4u)ConstructpointKasthecircumcenteroftriangleAMN\.

The auxiliary constructions predicted by AlphaGeometry for this problem are shown below\.

[⬇](data:text/plain;base64,Q29uc3RydWN0IHBvaW50IEsgc3VjaCB0aGF0IEtNID0gS04uCkNvbnN0cnVjdCBwb2ludCBMIGFzIHRoZSBpbnRlcnNlY3Rpb24gb2YgY2lyY2xlcyAoSywgQSkgYW5kIChPLCBBKS4=)ConstructpointKsuchthatKM=KN\.ConstructpointLastheintersectionofcircles\(K,A\)and\(O,A\)\.

The natural language formulation of the second problem is given below, and the corresponding diagram is shown in Figure[16](https://arxiv.org/html/2608.14585#A3.F16)\.

[⬇](data:text/plain;base64,SW4gdHJpYW5nbGUgQUJDLCBsZXQgSCBiZSB0aGUgb3J0aG9jZW50ZXIuIFBvaW50IEYgbGllcyBvbiB0aGUgbGluZSBIQSBhbmQgYWxzbyBvbiB0aGUgbGluZSBCQy4gTGV0IE0gYmUgdGhlIG1pZHBvaW50IG9mIHNlZ21lbnQgQkMuIExldCBPIGJlIHRoZSBjaXJjdW1jZW50ZXIgb2YgdHJpYW5nbGUgQUJDLCB3aGljaCBpcyB0aGUgY2VudGVyIG9mIHRoZSBjaXJjbGUgcGFzc2luZyB0aHJvdWdoIHBvaW50cyBBLCBCLCBhbmQgQy4gVHJpYW5nbGUgUUFIIGlzIGEgcmlnaHQgdHJpYW5nbGUgd2l0aCBhIDkwLWRlZ3JlZSBhbmdsZSBhdCBRLCB3aGVyZSBRIGxpZXMgb24gdGhlIGNpcmNsZSBjZW50ZXJlZCBhdCBPIHdpdGggcmFkaXVzIE9BLiBTaW1pbGFybHksIHRyaWFuZ2xlIEtIUSBpcyBhIHJpZ2h0IHRyaWFuZ2xlIHdpdGggYSA5MC1kZWdyZWUgYW5nbGUgYXQgSywgd2hlcmUgSyBhbHNvIGxpZXMgb24gdGhlIGNpcmNsZSBjZW50ZXJlZCBhdCBPIHdpdGggcmFkaXVzIE9BLiBMZXQgT18xIGJlIHRoZSBjaXJjdW1jZW50ZXIgb2YgdHJpYW5nbGUgS1FILCBhbmQgbGV0IE9fMiBiZSB0aGUgY2lyY3VtY2VudGVyIG9mIHRyaWFuZ2xlIEZLTS4gUHJvdmUgdGhhdCBwb2ludHMgSywgT18xLCBhbmQgT18yIGFyZSBjb2xsaW5lYXIu)IntriangleABC,letHbetheorthocenter\.PointFliesonthelineHAandalsoonthelineBC\.LetMbethemidpointofsegmentBC\.LetObethecircumcenteroftriangleABC,whichisthecenterofthecirclepassingthroughpointsA,B,andC\.TriangleQAHisarighttrianglewitha90\-degreeangleatQ,whereQliesonthecirclecenteredatOwithradiusOA\.Similarly,triangleKHQisarighttrianglewitha90\-degreeangleatK,whereKalsoliesonthecirclecenteredatOwithradiusOA\.LetO\_1bethecircumcenteroftriangleKQH,andletO\_2bethecircumcenteroftriangleFKM\.ProvethatpointsK,O\_1,andO\_2arecollinear\.

![Refer to caption](https://arxiv.org/html/2608.14585v1/figures/imo2015.jpg)Figure 16:Diagram of a geometry problem selected from IMO\-AG\-30\.The auxiliary constructions predicted by our LLM for this problem are shown below:

[⬇](data:text/plain;base64,Q29uc3RydWN0IHBvaW50IHAgYXMgdGhlIGludGVyc2VjdGlvbiBvZiBjaWNsZSAoTywgQSkgYW5kIExpbmUgKEgsIFEpLg==)Constructpointpastheintersectionofcicle\(O,A\)andLine\(H,Q\)\.

The auxiliary constructions predicted by AlphaGeometry for this problem are shown below:

[⬇](data:text/plain;base64,Q29uc3RydWN0IHBvaW50IFggYXMgdGhlIG1pZHBvaW50IG9mIENILgpDb25zdHJ1Y3QgcG9pbnQgWSBhcyB0aGUgbWlkcG9pbnQgb2YgS00uCkNvbnN0cnVjdCBwb2ludCBaIGFzIHRoZSBtaWRwb2ludCBvZiBCSC4=)ConstructpointXasthemidpointofCH\.ConstructpointYasthemidpointofKM\.ConstructpointZasthemidpointofBH\.