Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions

1 Introduction

• The introduction situates the work within long-running AI research on automated theorem proving and the enduring role of Euclidean geometry in the IMO.The authors cite foundational studies by Gelernter (1959), Gelernter et al. (1960), and Reiter (1972).Source: §1 · p. 1
• Neural-based geometry provers rely on models, particularly LLMs, that require additional GPU resources for inference.The introduction notes AlphaGeometry2’s use of multiple LLMs and shared knowledge, and TongGeometry’s guided tree search; it says TongGeometry’s technical details remain unreported.Source: §1 · p. 1
• A CPU-only random strategy for adding auxiliary points solves 25 of 30 IMO-30 problems, matching AlphaGeometry’s reported performance and motivating the question of whether a heuristic could reach gold-medal level.The introduction reports one of AlphaGeometry’s 25 announced proofs as wrong in Appendix A.Source: §1 · pp. 1–2
• HAGeo uses heuristic auxiliary constructions without a neural network, achieves gold-medal performance on IMO-30, and its optimized DDAR engine is approximately 20× faster than AlphaGeometry’s.The heuristic favors geometrically useful points, including intersections of circles and lines discoverable through numerical calculations; the deduction engine assumes numerical information is available.Source: §1 · p. 2
• HAGeo-409 contains 409 Olympiad-level geometry problems with human-assessed difficulty labels and is generally more challenging than IMO-30.The authors describe IMO-30 as small and predominantly relatively easy, and say that this may produce high evaluation variance.Source: §1 · p. 2

2.1 Automated Theorem Proving for Euclidean Geometry

• Algebraic provers transform geometry problems into polynomial systems, while synthetic work includes area-method proofs for more than 400 problems and deductive databases built from geometric rules.The cited algebraic approaches include Wu’s method and Gröbner bases; the synthetic examples are Chou et al. (1993) and Chou et al. (2000).Source: §2.1 · p. 2
• Recent systems extend deductive databases with algebraic reasoning and add auxiliary points using neural models or tree search; the cited work reports results ranging from silver-medal IMO-30 performance to 30/30.AlphaGeometry combined with Wu’s method is reported to solve 27/30, while TongGeometry is reported to solve 30/30; its technical details remain unavailable.Source: §2.1 · p. 2
• AlphaGeometry2 adds geometric-language and DDAR-engine improvements, double-point support, an ensemble of language models, and shareable knowledge across searches.Its synthetic training data is also described as having more complex problems and a better-balanced distribution.Source: §2.1 · pp. 2–3

2.2 Geometry Problem Dataset

• Olympiad-level datasets have largely focused on algebra and number theory, and several large synthetic geometry datasets have been generated from configurations or DDAR-derived facts.The cited work includes AlphaGeometry’s 100-million-problem dataset, GeoGen’s more than 100 turnaround problems, and TongGeometry’s reported 6 billion extracted problems; further TongGeometry details are unavailable.Source: §2.2 · p. 3

3 HAGeo-409 Benchmark Construction

• The authors collected more than 2,000 geometry problems, converted them into a geometry-specific language, and numerically verified more than 1,000 successfully converted problems.They retain a subset with human-annotated difficulty scores and add around 50 problems from ShuZhiMi.Source: §3 · p. 3
• Difficulty ranges from 1 to 7 and is defined as the average rating provided by ShuZhiMi users; the final benchmark contains over 400 annotated problems grouped into five difficulty ranges.The ranges are [1, 3), [3, 4), [4, 5), [5, 6), and [6, 7].Source: §3 · p. 4
• HAGeo-409 has an average difficulty of 3.47, compared with 2.85 for IMO-30, which the authors characterize as relatively easy.Difficulty is reported on a scale from 1 to 7, with higher values corresponding to harder problems.Source: §3 · p. 4
• Automatic conversion was difficult: around 50% of problems could be converted into construction-based definitions, and fewer than 20% could be automatically converted and numerically verified.The remaining problems expressible in the geometry language were manually revised.Source: §3 · p. 4
• For comparison with AlphaGeometry, the authors converted problems to its format, manually corrected errors, and aligned the benchmark format as closely as possible.Their example adds the circumcenter point when AlphaGeometry’s format defines it in the circumcircle construction.Source: §3 · p. 4

4.1 General Pipeline

• HAGeo processes problems through a geometry-specific language and DDAR, then retries with up to K heuristic auxiliary constructions if initial deduction fails.Each construction can contain up to N rounds, selecting one valid algebraically determined candidate per round.Source: §4.1 · p. 4, Figure 3 · p. 5, §4.5 · p. 7

4.2 Geometry-Specific Languages

• HAGeo’s language represents diverse geometric objects and construction actions, better matching problem statements and its deduction rules than AlphaGeometry’s point-based language.It can define points as intersections of curves, such as a curve for an angle condition with a line.Source: §4.2 · pp. 4–5

4.3 Deduction

• 24× speed improvement over AlphaGeometry’s DDAR on IMO-30 corresponds to average solving times of 1.75 seconds versus 42.77 seconds.The engine’s rule and implementation optimizations reduce time complexity while preserving deductive capacity.Source: §4.3 · p. 5

4.4 Algebraic Reasoning

• The algebraic reasoning engine converts length, ratio, and angle relations into linear equations, then uses Gaussian elimination to derive equivalent variable relations.Its alternative implementation uses sums instead of differences, halving computation through symmetry.Source: §4.4 · pp. 5–6

4.5 Heuristic for Auxiliary Points

• Because valid auxiliary constructions are numerous but only a few are useful, HAGeo favors basic constructions whose points lie non-trivially on lines or circles.Its numerically driven heuristic includes midpoints, reflections, perpendicular feet, and intersections; numerical checks add no assumptions beyond those already used by deduction.Source: §4.5 · p. 6
• Heuristic candidates include intersections of multiple lines, line-and-circle or circle pairs, and existing points shared by multiple lines or circles.Random auxiliary points are also included to enhance generalization.Source: §4.5 · pp. 6–7
• For up to K attempts, HAGeo randomly selects candidate constructions, generates points for N rounds, and reruns DDAR on CPUs.The resulting constructions are integrated into new DDAR runs without neural inference.Source: Figure 3 · p. 5, §4.5 · p. 7

5.1 Settings

• Settings used N=6 rounds, K=4096 on IMO-30 and K=2048 or 8192 on HAGeo-409; AlphaGeometry used beam, batch, and depth settings of 16, 64, and 8.Experiments ran on a 64-core CPU, with 60 seconds per DDAR run per problem.Source: §5.1 · pp. 7–8, Table 1 · p. 8

5.2 Results

• 28 of 30 IMO-30 problems were solved by HAGeo, compared with 24 credited to AlphaGeometry after its incorrect proof was excluded.The random auxiliary-point strategy solved 25 problems; HAGeo’s proofs were manually verified by an IMO gold medalist.Source: §5.2 · p. 8, Table 2 · p. 8
• At K=8192, HAGeo’s solve rates were 92.5% and 83.0% on [1,3) and [3,4), surpassing AlphaGeometry by 19.2% and 43.7%, respectively.All methods solved fewer problems as difficulty increased, while HAGeo solved two problems in the [6,7] range.Source: §5.2 · pp. 8–9

5.3 Ablation Study

• As K increases, both strategies improve on HAGeo-409, while HAGeo consistently outperforms the random baseline and solves [6,7] problems when K is sufficiently large.Figure 6 shows Pass@K across difficulty ranges and the full benchmark; its red double arrow marks the gap between the strategies’ best results.Source: §5.3 · p. 9, Figure 6 · p. 9

6 Conclusion

• HAGeo solves 28 of 30 IMO-30 problems, achieving gold-medal performance while being 20 times faster than AlphaGeometry.The method uses numerical computation on CPUs to add auxiliary points in DDAR.Source: §6 · p. 9
• HAGeo-409 contains human-evaluated difficulty annotations and problems generally more difficult than those in IMO-30.Experiments on HAGeo-409 demonstrate the method’s scalability and effectiveness.Source: §6 · p. 9

A Fallacious Proof in AlphaGeometry

• AlphaGeometry’s released IMO-2020-P1 proof contains an error at Step 9.The paper illustrates the proof and identifies the faulty inference.Source: A Fallacious Proof in AlphaGeometry · p. 13
• Step 9 infers an angle relation from collinearity and angle-equality statements.The displayed inference concludes that ∠(PO, AM) = ∠(DO, AZ).Source: A Fallacious Proof in AlphaGeometry · p. 13
• The inference implicitly assumes that M, N, and E are collinear, but the proof does not establish this.The authors identify this unsupported premise as the reason the statement is incorrect.Source: A Fallacious Proof in AlphaGeometry · p. 13

B Preliminary for DDAR

• DDAR combines deductive database inference and algebraic reasoning to explore geometric and numerical dependencies.The engine is used as the symbolic core in existing generative geometry theorem-proving frameworks.Source: B Preliminary for DDAR · p. 13
• The deductive database engine applies logically valid geometric rules to incrementally expand the set of provable statements.Rules infer properties such as collinearity, parallelism, or equality of segments and angles.Source: B Preliminary for DDAR · p. 13
• Algebraic reasoning represents equalities in canonical linear form and uses Gaussian elimination to uncover dependencies among angles, distances, or ratios.It also derives new quantitative relationships among existing angles or edges.Source: B Preliminary for DDAR · p. 13
• DDAR alternates deduction and algebraic inference, feeding each stage’s results into the other until the process converges.The paper says this interaction reasons across geometric and numerical domains while maintaining logical soundness.Source: B Preliminary for DDAR · p. 13

• The example starts from an IMO 2010 problem stated as a triangle configuration with an incenter, circumcircle, and constrained points.The target is that the intersection of EI and DG lies on the circumcircle.Source: C Example of our Geometry-Specific… · p. 14
• The translated goal is expressed as congruence of OA and OK, corresponding to K lying on the circle centered at O through A.The passage identifies that circle as the circumcircle of ABC.Source: C Example of our Geometry-Specific… · p. 14
• The geometry-specific form encodes the configuration through named constructions such as a triangle, circumcenter, incenter, line, intersection, and midpoint.It represents the angle condition with an angle-equality construction and names K as the intersection of DG and EI.Source: C Example of our Geometry-Specific… · p. 14

• The benchmark example begins with positively similar triangles A1A3A5 and A4A6A2 and defines six intersection points Xi.Each Xi is formed from specified lines through the indexed vertices.Source: D Example in our HAGeo-409 · p. 14
• For each index i, the problem defines Oi as the circumcenter of triangle AiXiAi+1, with A7 identified as A1.These circumcenters supply the points used in the theorem’s three lines.Source: D Example in our HAGeo-409 · p. 14
• The theorem asks whether O1O4, O2O5, and O3O6 are concurrent, while the translated form encodes the first two lines’ intersection K and proves K, O3, and O6 collinear.The geometry-specific form expresses the concurrency target as collinearity.Source: D Example in our HAGeo-409 · p. 14
• The translated construction encodes the initial similarity through angle-equality constraints and builds the Xi and Oi using line intersections and circumcenters.It then defines K as the intersection of O1O4 and O2O5.Source: D Example in our HAGeo-409 · p. 14

• The formalized IMO 2008 problem defines a circumcircle, four tangents, two incenters, and circles centered at those incenters before asking to prove IX = IT1.The original problem statement is represented as a sequence of geometric definitions and a congruence target.Source: E Example Proof of a Problem in IMO-30 · p. 15
• The auxiliary construction adds E as the foot of I on BI2 and F as the foot of B on IC, then introduces lines l5 and l6.The modified construction retains the original target IX = IT1.Source: E Example Proof of a Problem in IMO-30 · p. 15
• The deduction chain establishes intermediary circle, angle, and parallel-line relations before deriving IX = IT1.The listed proof concludes with IT1 = IT2 and IT2 = IX.Source: E Example Proof of a Problem in IMO-30 · pp. 16–18
• The authors manually convert and improve the HAGeometry proof for readability, including a concise similarity step and a congruence step in the rewritten proof.The displayed steps state △ET3F ∼ △I2DB and △ET3I ≃ △EXI.Source: E Example Proof of a Problem in IMO-30 · p. 18

F Prompt to Convert Natural Language into AlphaGeometry’s Geometric Language

• The encoding uses lowercase point names, semicolon-separated definitions, and a `?` separator before the conclusion.Its two parts are the problem definition and the conclusion to be proved.Source: F Prompt to Convert Natural Language… · pp. 19–20
• Initial free structures establish the geometry, and each subsequently constructed point is defined using one or two constraints.Examples include defining a midpoint, a foot, or a reflection with dedicated predicates.Source: F Prompt to Convert Natural Language… · p. 19
• Conclusions use predicates for geometric goals such as cyclicity, collinearity, perpendicularity, parallelism, ratios, and triangle similarity.For example, cyclicity is encoded as `? cyclic a b c d`, while similarity is encoded as `? simtri a b c d e f`.Source: F Prompt to Convert Natural Language… · p. 20
• Some conclusions require defining an auxiliary point first, and some implicit constructions are expanded into explicit point constraints.Examples encode a bisected segment by defining its midpoint and an incircle contact as the foot of the incenter on a side.Source: F Prompt to Convert Natural Language… · pp. 20–21
• A parallelogram problem is encoded with triangle and parallelogram declarations, line and circle constraints, and a final concurrence query.The natural-language example specifies a point on CD with OB = OD and asks whether AT, BO, and a circle are concurrent.Source: F Prompt to Convert Natural Language… · p. 22
• An incenter and circumcenter angle-equality problem is encoded using incenter, foot, and circumcenter constructions followed by an eqangle query.The statement concerns the in-circle tangent points on AB and AC and asks to prove angle ODB equals angle OEC.Source: F Prompt to Convert Natural Language… · p. 22
• An acute-triangle length problem is encoded using a circumcenter, midpoint, and circle intersections, followed by a congruence query.The natural-language example asks to prove DM = EC for the specified intersections of (AOM) with AB and AC.Source: F Prompt to Convert Natural Language… · p. 22
• The prompt instructs the model to convert {INPUT_PROBLEM} by following the examples.The listing is identified as an illustration of a natural-language-to-AlphaGeometry-language prompt.Source: F Prompt to Convert Natural Language… · p. 22

G Prompt to Convert Natural Language into our Geometric language

• Points, lines, and circles follow prescribed naming conventions, with nonconforming names converted to the allowed forms.Points use uppercase letters, optionally with subscripts; lines may use lowercase names or two defining points, and circles may be named by a center, diameter, or points on the circle.Source: G Prompt to Convert Natural Language… · p. 23
• The format separates a problem definition from its conclusion and builds the definition by adding geometry objects to an initial structure.Initial structures include triangles and other polygons, as well as points, lines, and circles.Source: F Prompt to Convert Natural Language… · p. 19, G Prompt to Convert Natural Language… · p. 23
• Each newly constructed point, line, or circle is defined using one or two constraints, with two conditions separated by a comma.For example, an intersection can be written as “X = AB, CD.”Source: G Prompt to Convert Natural Language… · pp. 23–24
• The target conclusion is written as a geometric predicate after “Prove:”, while new points are separated by semicolons and must have unused names.Examples of conclusion predicates include concyclicity, collinearity, concurrency, perpendicularity, and parallelism.Source: F Prompt to Convert Natural Language… · p. 20, G Prompt to Convert Natural Language… · p. 24
• Some conversions require adjustments, such as treating an angle at a triangle vertex as the corresponding three-letter angle and encoding a circle’s tangency point as a foot.A line or segment named by two points is written without a space, as in “foot X AB.”Source: G Prompt to Convert Natural Language… · pp. 24–25
• One example represents an acute triangle, its incenter and contact feet, then encodes intersections and a perpendicularity goal.The construction introduces points using named geometric operations, including a perpendicular line, circle intersections, and intersection of lines.Source: G Prompt to Convert Natural Language… · p. 26
• Other examples encode circumcircle and reflected-tangent constructions, and a problem using angle bisectors, intersections, length equality, and parallelism or congruence goals.The displayed encodings name geometric objects and operations and express the requested conclusion with predicates such as parallel or congruent.Source: G Prompt to Convert Natural Language… · p. 26
• The prompt asks the model to follow the examples and convert an input problem into the geometry-specific language.Listing 3 presents the prompt as an illustration of converting a natural-language problem.Source: G Prompt to Convert Natural Language… · p. 26