Autoformalizing Euclidean Geometry

Motivation

• Euclidean geometry offers a controllable autoformalization domain because its logical gaps are understood and it combines textual with diagrammatic reasoning.The setting also supports automatic evaluation and multimodal reasoning research.Source: §1 · p. 1

Evaluation challenge

• Semantic evaluation is difficult because exact matching is too rigid, logical equivalence is generally intractable, and proxy metrics or human judgment are inadequate.These limitations motivate domain-specific automatic evaluation.Source: §1 · p. 1

Automatic evaluation

• The symbolic engine combines Euclidean domain knowledge with SMT solvers to check equivalence between ground-truth and predicted formal theorems, while also supporting partial analysis.The protocol was validated by its correlation with human evaluation.Source: §1 · pp. 1–2

LeanEuclid

• LeanEuclid is a benchmark for testing machine learning on autoformalizing Euclidean geometry, with each example containing informal and formal theorems and proofs, plus a diagram.Source: §1 · p. 2

Diagrammatic reasoning

• The formal system E models diagrammatic reasoning as logical deductions, allowing the symbolic engine to fill proof gaps while the LLM formalizes explicit textual steps.This design lets formalized Elements proofs remain close to Euclid’s originals.Source: §1 · p. 2, Figure 1 · p. 2

LLM experiments

• GPT-4 correctly autoformalizes 18.9% of theorems, while GPT-4V reaches 21.0% and correctly autoformalizes 23.1% of proofs with 5-shot prompting.Imperfect proofs can often be manually repaired through a few simple modifications.Source: §1 · p. 3

Contributions

• The paper contributes automatic theorem-semantic evaluation, implicit handling of diagrammatic proof reasoning, and evidence about current LLM capabilities and limitations.It positions Euclidean geometry as a promising target for moving evaluation toward automatic methods.Source: §1 · p. 3

Autoformalization

• Existing autoformalization work uses synthetic data or few-shot LLMs because informal-formal training pairs are expensive, and LeanEuclid is intended for testing only.The benchmark follows the few-shot evaluation approach rather than targeting finetuning.Source: §2 · p. 3

Evaluation

• Prior evaluation relies on human judgment, compilation rates, or BLEU, whereas this work claims reliable automatic semantic evaluation of formalized statements.The paper identifies proxy metrics as insufficiently accurate.Source: §2 · p. 3

Formalizing Euclidean geometry

• Earlier formalizations of Euclid’s Elements require explicit treatment of diagrammatic gaps, making their proofs more verbose and less suitable for autoformalization.LeanEuclid instead builds on formal system E to automate diagrammatic reasoning.Source: §2 · p. 3
• The paper implements formal system E as a practical automated procedure for diagrammatic reasoning, extending a conceptual framework inspired by Euclid’s Elements.E defines geometric objects, relations, and procedures for stating and proving theorems.Source: §2 · p. 3

Geometric problem solving

• Geometry solvers such as AlphaGeometry find structured solutions, whereas this work translates human-written informal theorems and proofs into Lean using a general-purpose proof assistant.Both approaches combine neural and symbolic components, but their tasks and representations differ.Source: §2 · p. 3

Multimodal geometry benchmarks

• LeanEuclid extends multimodal geometry benchmarks by formalizing both problems and solutions, including 125 random UniGeo examples from a dataset of 9,543 informal theorems and proofs.This demonstrates formalization beyond Euclid’s Elements.Source: §2 · p. 4

3. Formalizing Euclidean Geometry in Lean

• LeanEuclid implements a variant of system E in Lean, supporting implicit diagrammatic reasoning and logical equivalence checking between theorems.System E defines geometric objects, relations, and formal theorem-proving rules inspired by Euclid’s Elements.Source: §3 · p. 4, §3.2 · p. 4

3.1. The Lean Proof Assistant

• Lean checks theorem well-formedness and proof correctness, but well-formedness alone does not ensure that a predicted theorem has the ground-truth meaning.The symbolic engine’s SMT results also cannot currently be fully certified by Lean.Source: §3.1 · p. 4

3.2. The Formal System E

• E models six geometric object types and their relations, including points, lines, segments, circles, angles, and triangles.Relations such as point-on-line are used to state Euclidean theorems formally.Source: §3.2 · p. 4
• System E represents theorems as preconditions, constructed objects, and postconditions, with axioms divided into construction and non-construction rules.Construction rules create new objects, while non-construction rules deduce properties of existing objects.Source: §3.2 · pp. 4–5
• When an explicit rule lacks a precondition, Lean can trigger diagrammatic reasoning to prove that precondition and then continue the construction if successful.For circle intersection, the system can infer the intersection fact and introduce a new point with its circle-membership relations.Source: §3.2 · p. 5
• Figure 2 separates explicit rule applications from implicit SMT-backed steps, restricting implicit reasoning to non-construction rules while explicit steps may use any rules.This division treats construction as the less mechanical part of geometric reasoning.Source: Figure 2 · p. 5, §3.3 · p. 5

3.3. Symbolic Reasoning Engine Based on SMT

• The symbolic reasoning engine uses SMT solvers to deduce obvious geometric facts and to check theorem equivalence.It encodes non-construction rules, existing objects and relations, and the negated target; an UNSAT result proves the target.Source: §3.3 · pp. 5–6

3.4. LeanEuclid: Overview and Dataset Statistics

• LeanEuclid contains 173 manually formalized theorems and proofs: 48 from Euclid’s Elements Book I and 125 adapted from UniGeo.The Elements formalizations follow Euclid’s texts closely while leaving diagrammatic reasoning implicit; UniGeo contributes 25 problems from each of five categories.Source: §3.4 · p. 6

4. Autoformalizing Euclidean Geometry with Large Language Models

• LLMs generate Lean theorem statements from natural-language problems using prompts containing syntax guidance, well-formed examples, and few-shot demonstrations.The complete prompting template is provided in the appendix.Source: §4.1 · p. 6

4.1. Autoformalizing and Evaluating Theorems

• E3 evaluates predicted theorem statements through logical equivalence checks and approximate clause-level semantic comparisons against ground truth.Logical checking tests both implication directions and contradictions; approximate checking uses selected variable unifications and compares provable preconditions and postconditions.Source: §4.1 · p. 6

4.2. Autoformalizing Proofs

• For proof autoformalization, the LLM receives natural-language and Lean proposition descriptions and generates tactic sequences, whose correctness is checked in Lean.The symbolic engine then attempts to fill diagrammatic gaps; available helper theorems depend on the proposition.Source: §4.2 · pp. 6–7
• Approximate equivalence checking is currently limited when the predicted formula does not have the same number of bound variables as the ground truth.The proof-autoformalization setup also allows a handful of construction rules in one configuration.Source: §4.2 · p. 6

5.1. Autoformalizing Theorem Statements

• Under 5-shot prompting, autoformalized theorem statements were correct at a rate of 21% across the Elements and UniGeo parts of LeanEuclid, with a small improvement from visual inputs.Correctness was measured using E3 to check logical equivalence.Source: §5.1 · p. 7, Table 1 · p. 7
• E3 automatically measured semantic equivalence and partitioned failed predictions by proving one, both, or neither implication direction.In two GPT-4 1-shot rounds, 31 of 67 rejected predictions supported only Tgt ⇒ Tpred, 15 only Tpred ⇒ Tgt, and 21 neither.Source: §5.1 · p. 7
• Among GPT-4’s 36 rejected Elements predictions, 5 resolved more than 90% of proof obligations through approximate equivalence analysis, beyond 7 provably equivalent propositions.Source: §5.1 · p. 7, Figure 3 · p. 7
• Manual comparison estimated E3’s false-negative rate at 15.8%, while the study found no soundness-bug indications and only one possible false positive.Source: §5.1 · p. 7

5.2. Autoformalizing Proofs

• GPT-4V correctly formalized 23.1% of LeanEuclid proofs versus 18.8% for GPT-4, although both completely formalized only Elements Propositions 1 and 17.The remaining 41 Elements proofs required some repair to be accepted by Lean.Source: §5.2 · p. 8, Table 2 · p. 8
• Repaired proofs retained median Levenshtein similarity of 61.7% for GPT-4 and 64.0% for GPT-4V, with many fixes involving tactic rearrangement or slight theorem strengthening.The authors attribute shorter, easier-to-repair proofs to tactic language and proof automation that handle implicit diagrammatic reasoning.Source: §5.2 · pp. 8–9

• SMT-based symbolic reasoning makes automatic theorem-statement evaluation and implicit diagrammatic reasoning feasible.Source: §6 · p. 9

• LeanEuclid contains 173 examples, a reasonable testing size but too small for finetuning-based approaches.The authors suggest automatically translating existing geometry datasets into the formalism to collect more examples.Source: §7 · p. 9
• Data contamination is considered unlikely because LeanEuclid was not publicly available during the experiments.Other online formalizations of Elements may have been seen by GPT-4, but they are described as fundamentally different from LeanEuclid.Source: §7 · p. 9
• The findings focus on Euclidean geometry, although domains with similar characteristics may also benefit from the methodology.Euclidean geometry is selected because its domain knowledge supports theorem equivalence checking and filling implicit reasoning gaps.Source: §7 · p. 9
• The work constructs a benchmark rather than introducing a novel model.The benchmark is intended to support future modeling efforts, including LLMs that use Lean feedback.Source: §7 · p. 9

Impact Statement

• The work advances autoformalization through the controlled domain of Euclidean geometry, whose applications include formal mathematics, verification, and autonomous systems.The authors note potential societal consequences of these downstream applications but do not specifically highlight any.Source: Impact Statement · p. 9

A. The Formal System E

• The Lean-like formal system E mostly follows E’s original specification, with a few minor deviations and a complete list of axioms.Its axioms are organized into construction, diagrammatic, metric, transfer, and superposition rules.Source: A. The Formal System E · p. 12, §A.3 · p. 13

A.1. Geometry Objects

• E represents six geometric object types: points, lines, circles, segments, angles, and triangles, with the latter three parameterized by points.For example, points can form segments, angles, and triangles.Source: §A.1 · p. 12

A.2. Functions, Constants, and Relations

• The system associates segments, angles, and triangles with length, degree, and size, and defines basic geometric predicates plus syntactic-sugar relations such as opposingSides.The basic predicates express relations including incidence, sidedness, betweenness, containment, centers, and intersections.Source: §A.2 · p. 12

A.3. Axioms

• E includes 32 construction rules and 36 diagrammatic rules, including several additions or strengthened variants introduced to facilitate formalizing proofs.The specification also notes that E’s axioms may be redundant because their number was not minimized.Source: §A.3 · pp. 13–14
• The axiom system contains 11 metric rules for lengths, angles, and areas, with SMT theories over real numbers included implicitly.Metric rules include segment equality, angle symmetry and range, area symmetry, and area congruence.Source: §A.3 · p. 16
• The framework provides 23 transfer rules bridging diagrammatic and metric facts, including five additions absent from E’s paper.The added rules are flat angle if, flat angle onlyif, parallelogram area, sum parallelograms area, and rectangle area.Source: §A.3 · p. 16
• A superposition rule supports Euclid’s method for proving Propositions 4 and 8 in Book I by constructing a triangle with matching angles, lengths, and placement constraints.The rule follows Avigad’s approach and guarantees corresponding geometric equalities and side-position relations.Source: §A.3 · p. 18
• The SMT-based symbolic engine accesses real-number theories and, for diagrammatic reasoning, all diagrammatic, metric, and transfer rules.For equivalence checking, it additionally uses nine construction rules, including point, line, circle, and line-intersection constructions.Source: §A.3 · p. 18

B. An Example of Logical Gaps in Euclid’s Proofs Found by Formalization

• Euclid’s proof of Proposition 24 omits the case where D and G lie on opposite sides of EF, revealing a logical gap.The authors construct a substantially more complicated proof for this case.Source: B. An Example of Logical Gaps in… · p. 19
• The omitted case is reduced to proving x > y from angle decompositions and triangle-angle inequalities.Here x = ∠EFG and y = ∠EGF, while α denotes equal base angles in the constructed triangle.Source: B. An Example of Logical Gaps in… · p. 19
• The formal Lean proof explicitly handles the missing case through geometric constructions, side-of-line case splits, and theorem applications.Its statement encodes two formed triangles, corresponding equal sides, and a larger included angle implying a larger base.Source: B. An Example of Logical Gaps in… · pp. 19–20

C. Comparison to Existing Formalization of Elements

• LeanEuclid’s formalization of Proposition 1 is concise, follows Euclid’s proof closely, and makes tactic-to-sentence correspondence straightforward.The formal statement concludes that an equilateral triangle can be constructed on a given segment.Source: C. Comparison to Existing… · p. 20
• Unlike LeanEuclid, Hernandez-Espiet (2023) requires diagrammatic inferences such as circle intersection to be supplied explicitly by the proof author.LeanEuclid uses a symbolic engine to establish such inferences automatically and implicitly.Source: C. Comparison to Existing… · p. 21
• Beeson et al. (2019) also formalize diagrammatic reasoning manually, producing longer proofs whose correspondence with Euclid’s proofs is harder to discern.Their Coq formalization of the equilateral-triangle construction expands many geometric and congruence facts explicitly.Source: C. Comparison to Existing… · p. 22

D.1. Theorem Statement Formalization

• The theorem-statement prompt constrains Lean propositions to a single implication over conjunctions, primitive geometric variables, permitted axioms, and a prescribed output format.It also restricts numeric notation, forbids intermediate variables, and requires all bound variables to occur in the formula.Source: §D.1 · pp. 23–24
• Because Euclid’s propositions may begin imperatively and reveal their logical meaning only at the proof’s end, the authors abbreviate proofs before prompting theorem-statement formalization.They found that giving the model entire natural-language proofs often produced poor theorem statements, and they provide the abbreviated versions in LeanEuclid.Source: §D.1 · p. 23, D. Autoformalization Prompts · p. 23

D.2. Proof Formalization (Elements)

• Elements formalization supplies all manually used inference rules, preceding theorem variants, and five hardcoded examples spanning proof formats and tactic invocations.For Proposition n, the model may use Propositions 1 through n−1 and their variations.Source: §D.2 · p. 25
• The formal language defines geometric sorts for points, lines, and circles, together with notation for lengths, angles, triangles, areas, incidence, sidedness, collinearity, and intersections.Additional abbreviations encode configurations such as triangles, rectilinear angles, and parallelograms.Source: §D.2 · p. 25
• Construction axioms generate distinct or between points, extend segments, establish lines and circles, and produce line-circle or circle-circle intersections under stated geometric conditions.The rules also encode same-side and opposite-side intersection constructions.Source: §D.2 · p. 26
• Inference axioms capture line uniqueness, superposition, segment and circle equalities, angle and area decomposition, perpendicularity, and rectangle area relations.These rules provide the theorem-level geometric consequences used after construction steps.Source: §D.2 · p. 26
• The proof DSL uses euclid_intros, euclid_apply, euclid_finish, and euclid_assert, with SMT solvers checking rule premises and resolving goals from the proof context.Existential rules introduce witnesses through the `as` form, while standard structural tactics are allowed and imperative tactics such as `rw` and `simp` are prohibited.Source: §D.2 · p. 27
• Generated responses must be bare Lean tactic scripts, provide all non-propositional rule arguments, and use `use` only when supplying witnesses for existential goals.The required output is a sequence of declarative tactics that can be inserted directly into a proof.Source: §D.2 · p. 27
• Worked formalizations translate constructions for laying off an equal segment and drawing a perpendicular into sequences of `euclid_apply`, witness selection, and `euclid_finish`.The examples instantiate geometric constructions, intersections, and propositions to produce the required witnesses.Source: §D.2 · pp. 28–29
• Elements formalizations encode triangle-angle, parallelogram-construction, and isosceles-triangle theorems as Lean statements proved through Euclid-specific rule applications.Examples formalize Proposition 32, construction of a parallelogram equal to a triangle, and Proposition 6 using `euclid_apply`, contradiction, and case analysis.Source: §D.2 · pp. 29–31
• The parallelogram construction formalization introduces midpoint, parallel-line, intersection, and area-equality steps before supplying witnesses for every existentially quantified variable.The implementation explicitly uses one argument for each existential variable in the theorem statement.Source: §D.2 · p. 30

D.3. Proof Formalization (UniGeo)

• The UniGeo formalization reuses manually selected inference rules and relevant Elements theorems, with randomly selected shots drawn from a separate UniGeo proof test set.Its guidelines are adjusted to accommodate UniGeo’s different input style.Source: §D.3 · p. 31
• UniGeo’s formal language defines geometric entities, relations, constructions, and macros for points, lines, circles, angles, triangles, lengths, areas, and configurations such as parallelograms.The definitions include relations such as collinearity, same-side, intersection, betweenness, and triangle similarity or congruence.Source: §D.3 · pp. 31–32
• The UniGeo rule library includes congruence and similarity consequences plus Elements propositions covering isosceles triangles, straight-line angles, vertical angles, and parallel-line angle relations.The encoded rules also formalize triangle exterior-angle and interior-angle sums and parallelogram side, angle, and area properties.Source: §D.3 · pp. 32–33
• Parallel-line inference rules encode both directions of standard angle criteria, including alternate-angle, exterior-angle, same-side-angle, and vertical-angle relationships under explicit betweenness and side conditions.The library contains propositions 15, 27–29 and their variants, with conclusions expressed as line nonintersection or angle equalities and sums.Source: §D.3 · p. 33
• Additional UniGeo axioms and propositions formalize triangle exterior-angle sums and parallelogram equalities for opposite sides, angles, and corresponding triangle areas.These rules include Proposition 32 and Proposition 34 with variants that differ in their assumptions about auxiliary lines.Source: §D.3 · pp. 33–34
• The DSL requires each key proof step or lemma to be formalized as a tactic proof in LeanEuclid’s restricted proof language.Proofs must be enclosed in three angle brackets and contain no annotations or markdown.Source: §D.3 · p. 34
• euclid_intros introduces universally quantified variables and premises into the current proof context.It requires no names for the introduced items.Source: §D.3 · p. 34
• euclid_apply instantiates rules, proves their premises from the context and axioms, and adds either conclusions or existential witnesses with properties.It can, for example, create a point on a line with a specified betweenness relation.Source: §D.3 · p. 34
• euclid_assert attempts to prove a proposition from the current context and the available axioms.This supports directly asserting claims whose proofs require no additional construction.Source: §D.3 · p. 34
• euclid_finish resolves the main proof goal using the accumulated context and axioms.It is also required at the end of proofs supplied to have.Source: §D.3 · p. 34
• The use tactic supplies witnesses for existential goals, while have proves named or unnamed intermediate lemmas.A lemma proof must terminate with euclid_finish, and a premise already in context can be used directly.Source: §D.3 · p. 34

Evaluation examples

• GPT-4 and GPT-4V examples compare generated formalizations with ground-truth propositions for Euclid’s Elements statements, including triangle congruence and triangle inequalities.The examples include both formalized theorem statements and their corresponding informal propositions.Source: §E.1 · pp. 35–36

Semantic equivalence

• E3 proves propositions equivalent despite four syntactic substitutions that swap line sets and points in triangle conditions and the postcondition.These perturbations may be difficult for human graders to validate directly.Source: §E.1 · p. 35

Alternative formulations

• E3 fills the gap between two valid midpoint formulations, one using betweenness and equal lengths and another adding a segment-addition condition.The example concerns formalizing that a point lies exactly halfway between two endpoints.Source: §E.1 · pp. 35–36

Concise versus expanded statements

• E3 identifies a concise triangle-inequality formalization as equivalent to an expanded formulation that explicitly enumerates all three side combinations.A syntactic metric could penalize the expanded prediction because it nearly doubles the ground-truth character length.Source: §E.1 · p. 36

E.2. False Negatives

• E3 also fails when its construction rules cannot form required geometric objects, such as lines AC and BC.Source: §E.2 · p. 37
• E3 occasionally rejects reasonable formalizations because equivalent theorem statements can differ in structure or omit diagram-specific conditions.One example reflects a diagram where C lies between A and B, although the formalization only requires constructing a right angle against AB.Source: §E.2 · p. 37

E.3. False Positive

• A false positive occurred when E3 proved equivalence for a statement using a quadrilateral and different parallel lines, despite not faithfully matching the proposition’s two-triangle formulation.Source: §E.3 · p. 38

E.4. Unsatisfiable Statements

• E3 correctly identifies unsatisfiable predictions, including contradictory line-intersection conditions and invalid repeated inputs to formQuadrilateral.The latter fails because formQuadrilateral requires all input objects to be distinct.Source: §E.4 · p. 38

E.5. The Approximate Logical Equivalence Procedure

• Approximate equivalence compares corresponding preconditions and postconditions after selecting bounded candidate unifications of bound variables.E3 records proved obligations across four implication steps and aggregates clause-level results into metrics such as the ratio of clauses solved.Source: §E.5 · p. 39

F.1. Quantitative Results

• Most repairs involved rearranging tactic arguments or switching between theorem variants rather than correcting major conceptual errors.The comparison uses Levenshtein ratio for incomplete GPT-4 and GPT-4V proof formalizations.Source: §F.1 · p. 39, Figure C · p. 39

F.2. Correctly Formalized Proofs from Elements

• The same two proofs, Propositions 1 and 17, were correctly formalized out of the box by both GPT-4 and GPT-4V.Source: §F.2 · p. 39
• These examples demonstrate that LeanEuclid’s proof language can support simple, elegant, and faithful formalizations of natural-language proofs.Source: §F.2 · p. 39
• Proposition 1 formalizes construction of an equilateral triangle by drawing two circles, selecting their intersection, joining it to A and B, and applying equal-radius facts.Source: §F.2 · p. 40
• For any triangle, the sum of any two angles is less than two right-angles: producing BC to D and using [Prop. 1.16] and [Prop. 1.13] establishes this.Source: §F.2 · pp. 40–41

Partial repairs

• Minor repairs can make several incorrect Elements proofs go through, and the required changes often do not require creative insight.The paper suggests this repair process is amenable to automation.Source: §F.3 · p. 41

Proposition 3

• Proposition 3 is repaired by replacing an insufficient intersection theorem with a stronger version that proves the needed between relation.The repaired proof constructs an intersection point and finishes using the between condition.Source: §F.3 · pp. 41–42

Proposition 5

• Proposition 5 requires a stronger between-points theorem, argument rearrangements, and removal of an inapplicable use tactic.The repaired proof uses point_between_points_shorter_than and reordered invocations of propositions 3 and 4.Source: §F.3 · pp. 42–43

Proposition 7

• Proposition 7 is repaired by switching to proposition 5′, trimming excess arguments, and relying on euclid_finish where intermediate tactics are redundant.The original rule and variant accept different point and line argument structures.Source: §F.3 · pp. 43–44

Proposition 18

• Proposition 18 is repaired by using proposition 3′ and proposition 5′, permuting arguments, and dropping the invalid as binding.After these changes, the proof goes through.Source: §F.3 · p. 44

Proposition 34

• Proposition 34 needs variant proposition 29 invocations, inferred arguments for proposition 26, and removal or permutation of an unnecessary proposition 4 tactic.The proof can already be completed by euclid_finish before the final tactic is repaired.Source: §F.3 · p. 45

Congruent/Thm07

• GPT-4V correctly translates the UniGeo/Congruent/Thm07 semiformal proof into LeanEuclid.The formal theorem asserts triangle congruence from equal sides and a parallel-line condition.Source: §F.4 · pp. 45–46
• The Congruent/Thm07 formalization derives an angle equality with proposition 29′′′ and closes the congruence proof with euclid_finish.The theorem concludes that triangle WYZ is congruent to triangle YWX.Source: §F.4 · p. 46

Parallel/Thm06

• GPT-4V also correctly translates the UniGeo/Parallel/Thm06 example, whose conclusion is that SU is parallel to VX when two angles are supplementary.The example is presented with a diagrammatic input in Fig. F.Source: §F.4 · pp. 46–47