MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4 Hao Shen*1 , Junyu Guo*2 , Tian Cui3 , Yuxuan Xiao1 , and Lihong Zhi†1

arXiv:2608.02295v1 [cs.AI] 3 Aug 2026

1

SKLMS, Academy of Mathematics and Systems Science, Chinese Academy of Sciences, University of Chinese Academy of Sciences, Beijing 100190, China 2 Institute of Logic and Cognition, Department of Philosophy, Sun Yat-sen University, Guangdong 510275, China 3 School of Mathematics, Shandong University, Shandong 250100, China * Equal contribution. † Corresponding author. shenhao24@amss.ac.cn; guojy228@mail2.sysu.edu.cn; ct@mail.sdu.edu.cn yuxuanxiao@mail.sdu.edu.cn; lzhi@mmrc.iss.ac.cn

Abstract We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean’s kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP’s Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.

1

Introduction

Large language models now solve difficult competition problems and are beginning to contribute to mathematical research, while formal reasoning systems increasingly construct machine checked proofs [Kung et al., 2026, Soltani Moakhar et al., 2026]. Lean 4 [de Moura and Ullrich, 2021] provides a rigorous foundation by representing mathematical claims precisely and checking proof terms with a small trusted kernel, supported by Mathlib [The mathlib community, 2020], a large library of formalized mathematics. Recent systems span specialized provers and agentic frameworks: AlphaProof, Seed-Prover, and Aristotle have demonstrated Olympiad level formal reasoning, 1

Evaluator Constructor LLM

LLM

Linter

Statement

GeoIR

Formal

Theorem

Reasoning

synthetic

Mathlib lemmas

Planner

Verifier

LLM Theorem

F-score

Computation

Subgoals algebraic

Agent

Proof

CAS

Figure 1: Overview of MechGeo. GeoFormalizer (top, yellow) translates an informal statement through GeoIR into a linted, compiled, and semantically evaluated Lean theorem. GeoProver (bottom, green) plans a proof, decomposes it into subgoals, discharges synthetic subgoals with Mathlib lemmas and algebraic ones through Lean-checked CAS certificates, and an independent verifier audits the final proof or counterexample artifact. Blue and red icons denote informal and formal artifacts, respectively. while DeepSeek-Prover-V2, Goedel-Prover-V2, and Hilbert have advanced Lean theorem proving [Hubert et al., 2026, Chen et al., 2025, Achim et al., 2025, Ren et al., 2025, Lin et al., 2026, Varambally et al., 2026]. AxiomProver1 , Numina-Lean-Agent, and LEAP have each reported verified Lean solutions to all twelve Putnam 2025 problems [Xin et al., 2026, Liu et al., 2026, Kung et al., 2026]. Most evaluations, however, begin with already formalized statements, leaving open a prior challenge: faithfully translating the intended configuration into a formal statement. Faithful formalization is challenging in Euclidean geometry. Informal problems derive their meaning jointly from text, diagrams, and geometric conventions, often leaving necessary order and nondegeneracy conditions implicit. Human readers naturally interpret the statement through the intended diagram and may therefore overlook unintended configurations admitted by the formal assumptions. Because many Mathlib definitions remain meaningful on degenerate inputs, such omissions need not cause a compilation error. For example, “D lies on BC” may mean that D lies on the supporting line, on the closed segment, or strictly between B and C, with B ̸= C often left implicit. These interpretations yield different Lean statements, all of which may elaborate, and some may even admit valid proofs. Thus, neither compiler feedback nor human inspection alone reliably determines whether a formal statement captures the intended configuration [Murphy et al., 2024, Tang et al., 2026]. Proving a formalized theorem poses a second challenge: exposing enough geometric structure for effective proof search. Specialized systems such as AlphaGeometry and TongGeometry achieve strong performance through specialized languages and symbolic deduction, but their success depends on proposing the required auxiliary constructions and expressing the relevant relations [Trinh et al., 2024, Zhang et al., 2026]. AlphaGeometry2 expands this language to express 88% of IMO geometry problems from 2000 to 2024; the remaining cases involve inequalities, nonlinear relations, three dimensional configurations, or constructions with arbitrarily many points [Chervonyi et al., 1

https://github.com/AxiomMath/Putnam2025

2

2025]. Mathlib native formalization is complementary, embedding geometry in a general mathematical library and producing reusable proofs checked by the Lean kernel. Algebraic reasoning is a central tool for geometry theorem proving. Coordinate algebraization translates geometric hypotheses and goals into polynomial equations and inequalities, which can then be handled systematically by Wu’s method, Gröbner basis computation, and related symbolic procedures [Wu, 1986, Buchberger, 1970]. Although algebraic methods reduce dependence on auxiliary constructions, algebraizing an entire configuration may produce large polynomial systems and substantial expression growth, with efficiency sensitive to coordinate choice, formulation, and variable ordering. Geometric reasoning and algebraic computation are therefore complementary: the former preserves geometric structure and decomposes the theorem into manageable subgoals, while the latter systematically discharges the resulting polynomial consequences. We present MechGeo, a Mathlib native agentic framework for autoformalization and certified Euclidean geometry proving. Its central principle is that geometric reasoning and algebraic computation should work together: geometric reasoning exposes the structure of a configuration and decomposes difficult proofs into manageable subgoals, while our formally verified algebraization library translates selected obligations into polynomial form for systematic symbolic computation. Our contributions are threefold: • Mathlib native autoformalization. GeoFormalizer introduces GeoIR, a deterministic Lean translation, and repair guided by compiler and semantic feedback. Across seven LLM backbones, it substantially improves the success rates of elaboration, especially for models with weaker direct-translation performance. • Certified proving through geometric and algebraic reasoning. GeoProver combines proof planning, intermediate lemmas, and selective algebraization. External CAS may generate certificates, but Lean verifies every certificate and final proof. • Verified IMO geometry results. We construct the faithful formalizations and kernelchecked proofs for 44 IMO geometry problems from 2000 to 2026. MechGeo also proves 12 statements in LEAP’s Lean-IMO-Bench [Kung et al., 2026] for the first time, formally refutes the remaining two, and proves both after repair. The results are publicly available in the MechGeoBench repository.2

2

Related Work

Symbolic and Neuro-Symbolic Geometry Reasoning. Classical approaches include Wu’s method, Gröbner basis computation, area and full angle methods, and deductive databases [Wu, 1986, Buchberger, 1970, Chou et al., 1994, 2000]. Recent systems such as AlphaGeometry, AlphaGeometry2, and TongGeometry combine symbolic deduction with learned guidance for auxiliary construction and search [Trinh et al., 2024, Chervonyi et al., 2025, Sinha et al., 2024, Zhang et al., 2026]. Unlike these systems, which use specialized geometric languages, MechGeo works with Mathlib statements and produces proofs checked by the Lean kernel. Euclidean Geometry in Proof Assistants. Earlier work formalized the area method, a simple version of Wu’s method, the connection between synthetic and Cartesian geometry in GeoCoq, and Euclid’s Book I in Coq and HOL Light [Narboux, 2004, Génevaux et al., 2011, Boutry et al., 2019, Beeson et al., 2019]. In Lean, LeanEuclid translates informal problems into System E and uses 2

https://github.com/MechMath/MechGeoBench

3

IMO 2026

GeoIR

GeoFormalizer

Triangle ABC; M, N midpoints of AB, AC. K lies in △ BMC and in ∠LBA, L in △ BNC and in ∠ACK, with

∠KBA=∠ACL, ∠LBK=∠LNC, ∠LCK=∠BMK. For O the circumcentre of △ AKL, prove OM = ON.

Lean Statement

point A; point B; point C; assume (nondegenerate_of_triangle A B C); let M = midpoint A B; let N = midpoint A C; point K; point L; assume (nondegenerate_of_triangle B M C); ×2 assume (nondegenerate_of_triangle A B L); ×2 assume (is K in_convex_hull B M C); ×4 assume (nondegenerate_of_angle K B A); ×6

A

assume ((angle K B A) = (angle A C L)); ×3 assume (nondegenerate_of_triangle A K L);

M K B

O

assume ((dist O A) = (dist O K)); ×2

let M := midpoint ℝ A B; let N := midpoint ℝ A C; ∀ K L : EuclideanSpace ℝ (Fin 2), AffineIndependent ℝ ![B, M, C] → ×2 AffineIndependent ℝ ![A, B, L] → ×2 K ∈ convexHull ℝ {B, M, C} → ×4 (K ≠ B ∧ B ≠ A) → ×6

∀ O : EuclideanSpace ℝ (Fin 2), dist O A = dist O K → ×2

prove ((dist O M) = (dist O N))

L

AffineIndependent ℝ ![A, B, C] →

∠ K B A = ∠ A C L → ×3 AffineIndependent ℝ ![A, K, L] →

point O;

N

dist O M = dist O N := by

C

GeoProver Proof Outline

Lean Proof excerpts

a Geometric reasoning: orientations from convexity three_angle_cross_signs

theorem imo_2026_p2 … := by obtain ⟨sg1, sg2, sg3⟩ := three_angle_cross_signs …

X ∈ conv{P,Q,R} ⇒ [Q−P, R−P]·[Q−P, X−P] ≥ 0 (sg₁, sg₂, sg₃) b Selective algebraization of angle constraints angle_tangent_of_same_sign

GeoProver

theorem imo_2026_p2 : ∀ A B C : EuclideanSpace ℝ (Fin 2),

[u,v]·(w·z) − (u·v)·[w,z] = 0 (t₁, t₂, t₃) c Selective algebraization of circumcentre constraints coordinate_sq Frame at A: B=(b,0), C=(u,v), K=(x,y), L=(p,q), O=(ox,oy); squaring OA=OK, OA=OL. e_K : 2ox·x + 2oy·y = x²+y² e_L : 2ox·p + 2oy·q = p²+q²

(a)

have t1 := angle_tangent_of_same_sign …; t2, t3 …

(b)

have hF := coordinate_core b u v x y p q …

(d₁)

have eK : 2*ox*x + 2*oy*y - (x^2+y^2) = 0 := …

(c)

have eL : 2*ox*p + 2*oy*q - (p^2+q^2) = 0 := …

(c)

have eW : … = 0 := by linear_combination (x*(-v)-y*(b-u))*eL - (p*(-v)-q*(b-u))*eK - hF

(d₂)

… nlinarith ✓

d Certified algebraic discharge coordinate_core t₁, t₂, t₃ (in coordinates) ⊢ F = 0; e_K, e_L, F ⊢ e_W goal OM = ON ⇔ e_W = 0 ✓

Figure 2: Case study on IMO 2026 P2: GeoIR to Lean 4 statement, then GeoProver’s plan (a)–(d) and the Lean proof lines it maps to. Repeated hypothesis families are folded as ×n. SMT reasoning to recover implicit diagrammatic facts; LeanGeo provides a library, automation, and a benchmark for competition geometry, and Euclean targets Mathlib-native geometry statement formalization through constraint explication, configuration anchoring, formalization mapping, and iterative repair [Murphy et al., 2024, Song et al., 2025, Tang et al., 2026]. MechGeo unifies Mathlib native autoformalization, semantic repair, and certified proof construction through a Lean verified algebraization layer.

3

Methodology

In this section, we present MechGeo, a framework that translates informal Euclidean geometry problems into Mathlib native Lean 4 statements and constructs complete proofs without sorry. As shown in Figure 1, GeoFormalizer generates a checked GeoIR representation, translates it deterministically into Lean, and repairs it using static, compiler, and semantic feedback. GeoProver first constructs a geometric proof plan that identifies auxiliary constructions and intermediate facts. Guided by this plan, it keeps structural arguments at the Mathlib level and selectively translates suitable hypotheses and goals into polynomial constraints. This selective algebraization preserves geometric structure, keeps the resulting polynomial systems tractable, and allows symbolic methods to discharge exact algebraic consequences. All generated certificates and the final proof are checked in Lean. Figure 2 illustrates this workflow on IMO 2026 Problem 2.

4

3.1

GeoFormalizer: Autoformalization via GeoIR

GeoFormalizer comprises four stages: GeoIR generation, Lean 4 statement translation, formal and semantic evaluation, and iterative repair. 3.1.1

GeoIR Generation

Directly generating Mathlib native geometry statements requires substantial knowledge of Lean syntax, its type system, and Mathlib interfaces, beyond what is needed to express standard Euclidean geometry problems. GeoIR reduces this burden by providing a simple, compact, and typed language in which models can state geometric content with a limited set of notations without directly manipulating statements in Lean. 3.1.2

Formal Statement Translation

There are four categories of GeoIR constructs: declarations, constructions, geometric relations, and values. Each construct has a fixed translation in Lean. Most of these constructs are translated into corresponding Mathlib expressions, and a small number are translated into predicates from our library. Translation is performed by a rule-based translator without an LLM. The translator parses a geometry proposition written in GeoIR into a typed abstract syntax tree, recursively traverses the tree, and reconstructs the corresponding Lean statement using a fixed mapping table. Lean’s parser, elaborator, and kernel then check well-formedness and well-typedness of the generated statement. The syntax and symbols used in the statement are confined to the translator mappings. When an interface in Mathlib changes, the affected mappings can be updated, and existing GeoIR statements can be re-translated into Lean statements that fit the new interface. 3.1.3

Evaluation

A challenge in automated geometry formalization is detecting and repairing semantic mismatches between a natural language problem and its formal statement. A statement may type check in Lean yet fail to capture the intended theorem because its assumptions are inconsistent, its conclusion is trivial, or it expresses a different theorem. We therefore combine semantic and structural signals into a single score: F = 0.7Sjudge + 0.3Sstruct . The judge score Sjudge evaluates the correspondence between the informal problem and the generated Lean statement. It assigns one of three labels: semantically consistent, partially consistent, or inconsistent, which are mapped to scores of 1, 0.5, and 0, respectively. The structural score Sstruct is the point coverage ratio, defined as the fraction of points declared in the GeoIR specification that are mentioned in the informal problem. This scoring design motivates our choice of τ = 0.6, so Sstruct is decisive only in the ambiguous case Sjudge = 0.5. 3.1.4

Iterative Repair

The generated GeoIR specification is first parsed and statically checked for undeclared objects, arity errors, type mismatches, and malformed structures. Diagnostics from parsing and static checking are returned to the constructor for repair. Candidates that pass these checks receive a score F and are accepted if F ≥ 0.6. Otherwise, the evaluator provides semantic and structural feedback, and the constructor revises the GeoIR specification.

5

3.2

GeoProver: Integrating Geometric and Algebraic Reasoning

GeoProver combines geometric and algebraic reasoning in a four stage agentic workflow: (1) Proof Planning, (2) Selective Algebraization, (3) Certified Algebraic Discharge, and (4) Independent Verification. 3.2.1

Proof Planning

For each theorem, GeoProver gives the proof agent only the formal Lean statement. The agent reconstructs the geometry and organizes key lemmas, auxiliary constructions, angle chases, and algebraic identities into an ordered informal proof plan. This decomposition precedes algebraization, so each CAS call typically handles a smaller, lower degree polynomial subsystem, reducing the burden on symbolic elimination. 3.2.2

Selective Algebraization

Algebraization is implemented by a collection of verified lemmas and the simplification tactic to poly, which applies some of these lemmas to the goal or selected hypotheses. It rewrites geometric notions, including predicates (e.g., collinearity and concyclicity), geometric objects (e.g., points and circles), and real number quantities (e.g., distances and arithmetic expressions), into polynomial expressions, equations, and inequalities in point coordinates. Logically, it proceeds in two steps. First, derived geometric predicates and objects are expressed with basic notations, including vectors, norms, and inner products, as handled by the tactic to basic. Then, these expressions are expanded coordinatewise into polynomials, as done by tactic basic to poly. The agent may apply selected lemmas or tactics at specialized locations. This selective control allows algebraization on specialized hypotheses and goals, such as subgoals proved with algebraic computation while keeping the remaining part in geometric form, on which existing lemmas in Mathlib for geometry can be applied. Rewrite rules applied by to poly are lemmas of equivalence between the geometric expressions and their algebraic expressions, so they never silently strengthen or weaken the statement. Typical proofs alternate between the two levels: synthetic lemmas establish geometric facts that are subsequently used for algebraization. 3.2.3

Certified Algebraic Discharge

For polynomial equality goals with hypotheses p1 = 0, . . . , pn = 0 and target q = 0, when Lean’s internal tactics are insufficient, GeoProver calls Singular [Decker P et al., 2019] or SymPy [Meurer et al., 2017] to compute cofactors c1 , . . . , cn that satisfy q = ni=1 ci pi . The agent translates this identity into a Lean proof, which is checked by the kernel. Inequalities and nonzero constraints are handled using Lean tactics, explicit sign lemmas, and case analysis. A CAS may assist with factorization or algebraic decomposition, but all sign arguments are verified in Lean. Independent Verification. For each input statement, GeoProver attempts either to prove it or to refute it with a counterexample. In the latter case, explicit coordinates are usually used to construct a counterexample and prove that the conclusion can fail when hypotheses hold. An independent verifier checks whether the statement has been correctly proved or refuted: a proof must match the input statement exactly, whereas a counterexample must formally establish its negation. In either case, the complete file must compile without sorry and use only the permitted Lean axioms.

6

4

Experiments

We evaluate GeoFormalizer and GeoProver both separately and within the complete MechGeo pipeline. End-to-end accuracy alone conflates three distinct failure modes: the generated statement may fail to elaborate, may elaborate but misrepresent the source problem, or may not yield a kernel-verified proof. We therefore report elaboration, semantic consistency, and proof success separately, organized around three research questions: RQ1. Autoformalization. How accurately does GeoFormalizer generate Lean statements that elaborate, and how much do iterative repairs improve performance? RQ2. Theorem proving and refutation. Given a fixed Lean statement, how often does GeoProver either construct a kernel-checked proof or formally refute it with a Lean-verified counterexample, and how much do selective algebraization and external computer algebra contribute? RQ3. Olympiad-level reasoning. How broadly can MechGeo prove or refute Olympiadlevel geometry statements? We evaluate MechGeo on 44 human audited IMO formalizations, repaired where necessary, as well as all 14 geometry problems in Lean-IMO-Bench [Kung et al., 2026].

4.1 4.1.1

Experimental Settings Dataset

Our evaluation set, MG200, contains four subsets totaling 200 informal geometry problems: 43 historical IMO geometry problems, 77 non-IMO problems from LeanGeo-Bench [Song et al., 2025], 22 classical geometry theorems, denoted CertiGeo, used to evaluate algebraic proving [Grégoire et al., 2011], and 58 plane geometry problems sampled by difficulty from Euclidean’s OMNI-Geometry dataset [Tang et al., 2026]. Together, these subsets are used to evaluate GeoFormalizer. To isolate proof generation from statement formalization, we evaluate GeoProver on the Lean statements produced by GeoFormalizer for all 200 MG200 problems. We further test GeoProver on 31 plane Euclidean geometry statements based on EuclideanSpace R (Fin 2) in Lean selected from PutnamBench [Tsoukalas et al., 2024] and on all 14 geometry problems in Lean-IMO-Bench, introduced by LEAP [Kung et al., 2026], to assess transfer beyond the main benchmark and performance on IMO-level geometry. 4.1.2

Models and Tools

We evaluate autoformalization with seven strong LLM backbones from diverse providers: GPT5.6-Sol [OpenAI, 2026], Claude Opus 4.8 [Anthropic, 2026], DeepSeek-V4-Pro and DeepSeek-V4Flash [DeepSeek-AI, 2026], Qwen3.7-Max [Qwen Team, 2026], MiniMax-M3 [Lai et al., 2026], and GLM-5.2 [Z.ai, 2026]. The selection includes both proprietary and open-weight model families, allowing us to assess whether the benefits of GeoFormalizer generalize beyond any single model or provider. All experiments use Lean 4.27.0. External symbolic computation uses Singular 4.4.1 and SymPy 1.13.2.

4.2

RQ1: Automatic Formalization

In all RQ1 experiments, the automatic semantic judge used for semantic-guided repair is fixed to GPT-5.6-Sol across all constructor backbones. Table 1 shows that the structured formalization pipeline substantially improves elaboration rate across model families. Across all 1,400

7

Method

GPT-5.6 Sol

Claude Opus 4.8

DeepSeek V4-Pro

DeepSeek V4-Flash

Qwen 3.7-Max

MiniMax M3

GLM 5.2

Direct Euclean Ours Direct CertiGeo (22) Euclean Ours Direct LeanGeo Non-IMO (77) Euclean Ours Direct OMNI Geometry (58) Euclean Ours

21 (48.8) 43 (100) 43 (100) 16 (72.7) 22 (100) 22 (100) 33 (42.9) 77 (100) 77 (100) 40 (69.0) 58 (100) 58 (100)

23 (53.5) 43 (100) 43 (100) 15 (68.2) 22 (100) 22 (100) 25 (32.5) 77 (100) 77 (100) 35 (60.3) 58 (100) 58 (100)

1 (2.3) 43 (100) 39 (90.7) 4 (18.2) 22 (100) 22 (100) 5 (6.5) 75 (97.4) 76 (98.7) 6 (10.3) 57 (98.3) 48 (82.8)

0 (0.0) 43 (100) 42 (97.7) 4 (18.2) 22 (100) 22 (100) 7 (9.1) 77 (100) 77 (100) 15 (25.9) 54 (93.1) 53 (91.4)

30 (69.8) 31 (72.1) 39 (90.7) 17 (77.3) 16 (72.7) 22 (100) 59 (76.6) 65 (84.4) 72 (93.5) 37 (63.8) 28 (48.3) 53 (91.4)

0 (0.0) 20 (46.5) 41 (95.3) 3 (13.6) 10 (45.5) 21 (95.5) 9 (11.7) 37 (48.1) 74 (96.1) 5 (8.6) 24 (41.4) 53 (91.4)

16 (37.2) 29 (67.4) 43 (100) 12 (54.5) 13 (59.1) 22 (100) 42 (54.5) 66 (85.7) 77 (100) 33 (56.9) 27 (46.6) 58 (100)

Dataset IMO (43)

Table 1: RQ1 results on the four autoformalization datasets. Ours denotes GeoFormalizer. Each entry reports the number (percentage) of successfully elaborated Lean statements. Direct uses a single translation attempt. Although the evaluation settings differ, Euclean receives a 10-minute timeout and, in our runs, makes 14–116 model calls per problem, whereas GeoFormalizer uses at most five calls. Best results within each dataset–model column are bolded. model–problem pairs, GeoFormalizer produces 1,354 statements that elaborate successfully (96.7%), compared with 1,159 (82.8%) for Euclean and 513 (36.6%) for direct translation. The gains over Euclean are particularly large for backbones with weaker baseline performance: the overall elaboration rate rises from 70.0% to 93.0% for Qwen3.7-Max, from 45.5% to 94.5% for MiniMax-M3, and from 67.5% to 100% for GLM-5.2. GeoFormalizer also preserves near-ceiling performance for the strongest backbones, achieving 100% with GPT-5.6-Sol and Claude Opus 4.8. The improvements are consistent across datasets. Even on IMO and OMNI-Geometry, where several baselines degrade most sharply, GeoFormalizer maintains strong performance across backbones, with most results exceeding 90%. Although the evaluation settings differ, Euclean uses a substantially larger model call budget: in our runs, it makes 14–116 model calls per problem, whereas GeoFormalizer uses at most five. Table 2 further examines the contributions of compiler guided and semantic-guided repair in GeoFormalizer. We compare four settings by independently enabling or disabling the two repair components. Without repair, the mean elaboration rate is 83.1%. Two rounds of compiler guided repair increase it to 96.9%, whereas semantic-guided repair alone raises it to 88.7%. Thus, compiler guided repair contributes most of the gain in elaboration rate. Semantic guided repair has a smaller effect on elaboration because it primarily targets semantic mismatches. Because Lean acceptance guarantees only syntactic and type correctness, three experts independently evaluate the semantic consistency of the 200 statements generated by Claude Opus 4.8. A statement is accepted by majority vote only if it preserves the intended objects, constructions, hypotheses, admissible configurations, and conclusion, allowing equivalent reformulations. Initially, 157 statements are judged faithful, giving a rate of 78.5%. However, Table 4 shows that formal counterexample search refutes 22 of these statements, revealing degeneracy and order errors missed by human inspection.

8

Model

Setting (r, f )

∆

(0, 0)

(0, 2)

(2, 0)

(2, 2)

Claude Opus 4.8 GLM-5.2 GPT-5.6 DeepSeek V4-Flash DeepSeek V4-Pro Qwen3.7 Max MiniMax M3

98.5 97.5 97.5 85.0 81.0 64.5 57.5

99.0 98.0 96.0 87.0 85.0 63.0 93.0

97.5 100.0 100.0 97.0 96.5 90.5 96.5

100.0 100.0 100.0 97.0 92.5 93.0 94.5

+1.5 +2.5 +2.5 +12.0 +11.5 +28.5 +37.0

Mean

83.1

88.7

96.9

96.7

+13.6

Table 2: RQ1 ablation of repair rounds on the 200-problem benchmark. Each cell reports the percentage of problems whose generated Lean statement elaborates successfully under setting (r, f ), where r and f denote the numbers of compiler-guided and semantic-guided repair rounds, respectively. ∆ is the absolute improvement of the full setting (2, 2) over the baseline (0, 0).

4.3

RQ2: Automated Theorem Proving and Refutation

For RQ2, we evaluate all provers on the 200 statements generated by GeoFormalizer with Claude Opus 4.8, including statements later judged semantically unfaithful, along with 31 Euclidean geometry statements in Lean from PutnamBench. Each prover receives a two hour budget per problem and runs in a sandbox with read only access to the Lean project and toolchain, a private writable workspace, and no web access. Numina-Lean-Agent and Hilbert use the same DeepSeek-V4Pro backend, input statements, and budget as GeoProver. For both agents, we retain the default prompts from their official releases and replace only the LLM backend. Goedel-Prover-V2-8B uses its released 8B model with pass@32 sampling, following its original evaluation protocol. As shown in Table 3, GeoProver proves 67 of the 200 MG200 statements and 6 of the 31 PutnamBench statements in Lean, for a total of 73 out of 231, compared with 44 for Numina-Lean-Agent, 13 for Hilbert, and none for Goedel-Prover-V2-8B. To evaluate both proof construction and formal refutation, Table 4 presents the cross-tabulation between the results on MG200 and human semantic annotations. Replacing the backbone with GPT-5.6-Sol while keeping all other settings unchanged substantially improves performance on both datasets. On MG200, GeoProver proves 145 of the 200 statements and formally refutes 45. On the Putnam subset, it proves 30 of the 31 statements in Lean, with only one timeout. The results further illustrate that successfully proving a formal statement does not necessarily imply semantic consistency with the original informal problem. Moreover, because Euclidean geometry problems often rely on implicit nondegeneracy conditions that are difficult for human annotators to verify exhaustively, establishing statement faithfulness remains a challenging problem. We investigate this issue in detail in RQ3. 4.3.1

Contributions of CAS

To quantify the contribution of symbolic computations, we perform an ablation study by progressively removing the external computer algebra systems and the Lean-side algebraization toolkit. All other components, including the DeepSeek-V4-Pro backbone, remain unchanged. As shown in Table 3, the full GeoProver achieves 73 verified proofs out of 231 problems. Removing CAS causes a substantial performance degradation, reducing the number of solved problems to 29. This demonstrates that external symbolic computation plays a central role in discharging algebraically 9

Method / Setting

MG200 (200)

Putnam (31)

Total (231)

Goedel Hilbert Numina

0 (0.0%) 13 (6.5%) 43 (21.5%)

0 (0.0%) 0 (0.0%) 1 (3.2%)

0 (0.0%) 13 (5.6%) 44 (19.0%)

GeoProver (full) w/o CAS w/o CAS + algebra

67 (33.5%) 29 (14.5%) 19 (9.5%)

6 (19.4%) 0 (0.0%) 0 (0.0%)

73 (31.6%) 29 (12.6%) 19 (8.2%)

Table 3: RQ2 main comparison and cumulative ablation results. Hilbert, Numina-Lean-Agent, GeoProver, and the GeoProver ablations use DeepSeek-V4-Pro under the same two-hour perproblem budget. Goedel-Prover-V2-8B is evaluated with its native model using pass@32. Each entry reports the number and percentage of statements for which a kernel-checked proof is obtained. Proved

Refuted

Timeout

Total

Faithful (Human) Not Faithful (Human)

128 17

22 23

7 3

157 43

Total

145

45

10

200

Table 4: Cross-tabulation of initial human semantic judgments and GeoProver outcomes on MG200 using GPT-5.6-Sol. The statements are generated by GeoFormalizer with Claude Opus 4.8. structured geometric goals. Removing both CAS and the algebraization toolkit further decreases performance to only 19 solved problems. The additional drop indicates that the algebraization interface is also essential: even without external symbolic solvers, exposing geometric relations as polynomial constraints provides useful intermediate representations for Lean-based reasoning. These results confirm that GeoProver’s effectiveness does not come solely from LLM-based proof search. Instead, the combination of geometric reasoning, Lean-verified algebraization, and symbolic computation provides complementary capabilities. 4.3.2

Qualitative analysis of proof decomposition.

The ablation results quantify the aggregate contribution of the algebraization and CAS components. We further examine how the agent’s planning and decomposition reduce the complexity of individual algebraic goals. For IMO 2008 P1, one of the 73 solved problems, decomposition replaces a global system of 16 quadratic equations in 22 scalar coordinate variables with six local systems, each comprising three quadratic equations and one quadratic nonvanishing constraint in 10 variables, followed by two symmetry systems with three and two quadratic equations, respectively, in at most 10 variables.

4.4

RQ3: IMO-Level Geometry Formalization and Proving

We evaluate the complete system on three sets of Olympiad level geometry problems: 43 historical IMO problems, IMO 2026 Problem 2, and the 14 geometry statements in LEAP’s Lean-IMO-Bench. Throughout this section, statements are formalized by GeoFormalizer with Claude Opus 4.8 and proofs are constructed by GeoProver with GPT-5.6-Sol. Table 5 reports whether GeoProver

10

IMO (43)

IMO 2026

LEAP

Proved Refuted Human repaired Repaired proved

29 14 14 14

1 0 0 0

12 2 2 2

Final faithful proofs

43

1

14

Table 5: Proof and repair outcomes across three geometry evaluation sets. A statement is refuted when GeoProver finds a counterexample; final faithful proofs include both original and human repaired statements. proves the original formal statement, refutes it with a Lean verified counterexample, or proves a human repaired version. GeoProver proves 28 of the 43 statements generated by GeoFormalizer within two hours, and one additional statement in 2 hours and 6 minutes. Manual inspection confirms that all 29 are semantically faithful formalizations of their corresponding informal problems. For each of the remaining 14 statements, GeoProver constructs a formally verified counterexample, typically exposing missing nondegeneracy or point order assumptions. After expert repair, GeoProver proves all 14 corrected statements, yielding faithful verified proofs for all 43 historical IMO problems. MechGeo also formalizes and proves IMO 2026 Problem 2 directly from its informal statement, as illustrated in Figure 2. On Lean-IMO-Bench, GeoProver proves 12 of the 14 original statements for the first time and refutes the remaining two with counterexamples revealing missing nondegeneracy assumptions. After these two statements are repaired, GeoProver proves both corrected versions. 4.4.1

Example (IMO 2007 P2, missing nondegeneracy)

ABCD is a parallelogram and BCED is a cyclic quadrilateral. Let l be a line passing through A. Suppose that l intersects the interior of the segment DC at F and intersects line BC at G. Suppose also that EF = EG = EC. Prove that l is the bisector of ∠DAB. Figure 3a shows the intended configuration, while Figure 3b presents a degenerate counterexample with D = (0, 0), A = (1/5, 0), F = G = (1/2, 0), B = C = (1, 0), E = (3/4, 1), for which ∠DAF = π and ∠F AB = 0. The formalization omits the noncollinearity implicit in “ABCD is a parallelogram.” After adding that A, B, and C are noncollinear, GeoProver proves the repaired statement.

(a) Correct diagram

(b) A counterexample to formalization

Figure 3: IMO 2007 P2

11

4.4.2

Example (Lean-IMO-Bench Basic 028, missing order relation)

In △ABC the altitudes BE and CF intersect at H. A circle (W ) is externally tangent to the Euler circle (E) of △ABC and also tangent to the sides AB and AC at X and Y , respectively, with (W ) being closer to A than the Euler circle. Let I ′ be the incenter of △AEF . Prove that AXI ′ Y is a rhombus. A

W H

Y

X

W

Y

X I' F E A

I' F

E H

B

C

C B

(a) Correct diagram

(b) A counterexample to formalization

Figure 4: Lean-IMO-Bench Basic 028 Figure 4 shows both the intended configuration and an unintended case admitted by the original formalization, in which X and Y lie outside the segments AB and AC. After requiring X and Y to lie in the interiors of AB and AC, respectively, GeoProver proves the repaired statement.

5

Conclusion

Our results show that trustworthy geometry theorem formalization requires statement validation and proof construction within a unified verification loop. MechGeo proves challenging geometry theorems, detects incorrect formalizations through Lean verified counterexamples, and demonstrates the value of selective algebraization and symbolic computation. Future work will automate semantic and nondegeneracy checks and scale proof planning and certificate generation to broader and more challenging classes of geometry theorems.

Acknowledgment Hao Shen and Lihong Zhi are supported by the National Key R&D Program of China (Grant No. 2023YFA1009401) and the Strategic Priority Research Program of the Chinese Academy of Sciences under Grant XDA0480501. Junyu Guo is encouraged and supported by his supervisor, Xishun Zhao, to work on this project. We sincerely thank Yunfei Li for helping to review the formalizations of the geometry problems and Ruichen Qiu for assisting with the preparation of Figure 1.

12

References Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathı̈s Fédérico, Sergei Gukov, Daniel HalpernLeistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, and Lawrence Wu. Aristotle: Imo-level automated theorem proving, 2025. URL https://arxiv.org/abs/2510. 01346. Anthropic. Introducing Claude Opus 4.8. https://www.anthropic.com/news/claude-opus-4-8, May 2026. Accessed: 2026-07-27. Michael Beeson, Julien Narboux, and Freek Wiedijk. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, 85(2–4):213–257, 2019. doi: 10.1007/s10472-018-9606-x. Pierre Boutry, Gabriel Braun, and Julien Narboux. Formalization of the arithmetization of Euclidean plane geometry and applications. Journal of Symbolic Computation, 90:149–168, 2019. doi: 10.1016/j.jsc.2018.04.007. Bruno Buchberger. Ein algorithmisches kriterium für die lösbarkeit eines algebraischen gleichungssystems. Aequationes Mathematicae, 4(3):374–383, 1970. doi: 10.1007/BF01844169. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-Prover: Deep and broad reasoning for automated theorem proving, 2025. URL https://arxiv.org/abs/2507.23726. Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang H. Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le, and Thang Luong. Goldmedalist performance in solving olympiad geometry with AlphaGeometry2. Journal of Machine Learning Research, 26(241):1–39, 2025. URL https://www.jmlr.org/papers/v26/25-1654.html. Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry Theorems, volume 6 of Series on Applied Mathematics. World Scientific, Singapore, 1994. ISBN 978-981-02-1584-2. doi: 10.1142/2196. Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25(3): 219–246, 2000. doi: 10.1023/A:1006171315513. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28, volume 12699 of Lecture Notes in Computer Science, pages 625–635, Cham, 2021. Springer. doi: 10.1007/978-3-030-79876-5 37. Wolfram Decker, Gert-Martin Greuel, Gerhard Pfister, and Hans Schönemann. Singular 4-1-2—a computer algebra system for polynomial computations. https://www.singular.uni-kl.de/, 2019. DeepSeek-AI. Deepseek-v4: Towards highly efficient million-token context intelligence, 2026. URL https://arxiv.org/abs/2606.19348. Jean-David Génevaux, Julien Narboux, and Pascal Schreck. Formalization of Wu’s simple method in Coq. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, volume 7086 of Lecture Notes in Computer Science, pages 71–86, Berlin, Heidelberg, 2011. Springer. doi: 10.1007/978-3-642-25379-9 8. 13

Benjamin Grégoire, Loı̈c Pottier, and Laurent Théry. Proof certificates for algebra and their application to automatic geometry theorem proving. In Automated Deduction in Geometry, volume 6301 of Lecture Notes in Computer Science, pages 42–59. Springer, 2011. doi: 10.1007/978-3-642-21046-4 3. Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 651:607–613, 2026. doi: 10.1038/s41586-025-09833-y. Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun-Liang Li, Simone Severini, Mirek Olšák, Edward Lockhart, Quoc V. Le, Burak Gokturk, Thang Luong, Tomas Pfister, and Nanyun Peng. LEAP: Supercharging LLMs for formal mathematics with agentic frameworks, 2026. URL https://arxiv.org/abs/2606.03303. Xunhao Lai, Weiqi Xu, Yufeng Yang, Qiaorui Chen, Yang Xu, Lunbin Zeng, Xiaolong Li, Haohai Sun, Haichao Zhu, Vito Zhang, Jinkai Hu, Jiayao Li, Rui Gao, Zekun Li, Songquan Zhu, Jingkai Zhou, and Pengyu Zhao. Minimax sparse attention, 2026. URL https://arxiv.org/abs/2606. 13392. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-Prover-V2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. In The Fourteenth International Conference on Learning Representations, 2026. URL https://openreview.net/forum? id=j4C0nALrgK. Junqi Liu, Zihao Zhou, Zekai Zhu, Marco dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, Lihong Zhi, Jia Li, and Wenda Li. Numina-Lean-Agent: An open and general agentic reasoning system for formal mathematics. In Proceedings of the 43rd International Conference on Machine Learning, 2026. URL https://arxiv.org/abs/2601.14027. Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ondřej Čertı́k, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. SymPy: symbolic computing in Python. PeerJ Computer Science, 3:e103, 2017. Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing Euclidean geometry. In Proceedings of the 41st International Conference on Machine Learning, volume 235 of Proceedings of Machine Learning Research, pages 36847–36893. PMLR, 2024. URL https://proceedings.mlr.press/v235/murphy24a.html. Julien Narboux. A decision procedure for geometry in Coq. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, Theorem Proving in Higher Order Logics, volume 3223 of Lecture Notes in Computer Science, pages 225–240, Berlin, Heidelberg, 2004. Springer. doi: 10.1007/978-3-540-30142-4 17. OpenAI. GPT-5.6: Frontier intelligence that scales with your ambition. https://openai.com/index/ gpt-5-6/, July 2026. Accessed: 2026-07-27. Qwen Team. Qwen3.7: The agent frontier. https://qwen.ai/blog?id=qwen3.7, May 2026. Accessed: 2026-07-27. 14

Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition, 2025. URL https://arxiv.org/abs/2504.21801. Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat, and Matthias Bethge. Wu’s method can boost symbolic AI to rival silver medalists and AlphaGeometry to outperform gold medalists at IMO geometry, 2024. URL https://arxiv.org/abs/2404.06405. Arshia Soltani Moakhar, Iman Gholami, Max Springer, Mahdi JafariRaviz, and MohammadTaghi Hajiaghayi. Beyond the library: An agentic framework for autoformalizing research mathematics, 2026. URL https://arxiv.org/abs/2606.31134. Chendong Song, Zihan Wang, Frederick Pu, Haiming Wang, Xiaohan Lin, Junqi Liu, Jia Li, and Zhengying Liu. LeanGeo: Formalizing competitional geometry problems in Lean, 2025. URL https://arxiv.org/abs/2508.14644. Linbin Tang, Jingyan You, Zilin Kang, Hanzhang Liu, Sophia Zhang, Zenan Li, Chenrui Cao, Liangcheng Song, Jiaao Wu, Xian Zhang, and Fan Yang. Euclean: Automated geometry problem formalization with unified verification in Lean. In Proceedings of the 43rd International Conference on Machine Learning, 2026. URL https://arxiv.org/abs/2607.19374. The mathlib community. The Lean mathematical library. In CPP 2020, page 367–381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450370974. doi: 10.1145/ 3372885.3373824. Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476–482, 2024. doi: 10.1038/s41586-02306747-5. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. PutnamBench: Evaluating neural theorem-provers on the putnam mathematical competition. In Advances in Neural Information Processing Systems, volume 37, pages 11545–11569. Curran Associates, Inc., 2024. doi: 10.52202/079017-0368. Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, and Ke Ye. Hilbert: Recursively building formal proofs with informal reasoning. In The Fourteenth International Conference on Learning Representations, 2026. Wen-Tsun Wu. Basic principles of mechanical theorem proving in elementary geometries. Journal of Automated Reasoning, 2(3):221–252, 1986. doi: 10.1007/BF02328447. Jimmy Xin, Alex Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh, and Jannis Limperg. AXLE: A cloud infrastructure for Lean 4 theorem proving utilities. In 3rd AI for Math Workshop at ICML 2026, 2026. URL https://arxiv.org/abs/2606.26442. Z.ai. GLM-5.2: Built for long-horizon tasks. https://z.ai/blog/glm-5.2, June 2026. Accessed: 2026-07-27. Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu, and Song-Chun Zhu. Proposing and solving olympiad geometry with guided tree search. Nature Machine Intelligence, 8(1):84–95, 2026. doi: 10.1038/s42256-025-01164-x. 15

A

Overview of the Appendix

This appendix provides additional technical details and supporting material for MechGeo. We first describe the autoformalization pipeline, including a detailed specification of GeoIR. Next, we present further details of the automated theorem proving process. We then provide several case studies illustrating the effect of proof decomposition on GeoProver’s performance and its ability to discover counterexamples. Finally, we report additional experimental settings.

B

Autoformalization Details

B.1

GeoIR Specification

Table 3 presents the specification of GeoIR and its deterministic translation into Mathlib-native Lean. GeoIR represents each problem as a sequence of object declarations, explicit constructions, geometric hypotheses, and a single goal.

B.2

Predicates for Polygon Convexity

We also introduce two predicates for the formalization of polygon convexity. def IsConvexQuad (A B C D : EuclideanSpace R (Fin 2)) := letI oangle := (PiLp.basisFun 2 R (Fin 2)).orientation.oangle; ((oangle (A -v B) (C -v B)).sign = -1 ∧ (oangle (B -v C) (D -v C)).sign = -1 ∧ (oangle (C -v D) (A -v D)).sign = -1 ∧ (oangle (D -v A) (B -v A)).sign = -1) ∨ ((oangle (A -v B) (C -v B)).sign = 1 ∧ (oangle (B -v C) (D -v C)).sign = 1 ∧ (oangle (C -v D) (A -v D)).sign = 1 ∧ (oangle (D -v A) (B -v A)).sign = 1) def IsConvex {n} (f : Fin n → EuclideanSpace R (Fin 2)) : Prop := letI oangle := (PiLp.basisFun 2 R (Fin 2)).orientation.oangle; (∀ i j : Fin n, j ̸= i → j ̸= finRotate n i → (oangle (f (finRotate n i) -v f i) (f j -v f i)).sign = 1) ∨ (∀ i j : Fin n, j ̸= i → j ̸= finRotate n i → (oangle (f (finRotate n i) -v f i) (f j -v f i)).sign = -1)

C

Automated Theorem Proving Details

C.1

Algebraization Lemmas

The conversion of geometric objects and expressions into algebraic form, primarily polynomial equalities and inequalities, proceeds in two steps. Each step can be performed either by applying the lemmas listed in the docstring of MechGeoBench/GeoTheorem/ToPolyMacros.lean or by using the following tactics: 1. convert derived expressions to basic expressions: the “Derived” part, the to_basic tactic;

16

2. convert basic expressions to algebraic expressions: the “Basic” part, the basic_to_poly tactic. The two steps can also be done in a single tactic to_poly. These three tactics can be called with an extra argument at POSITION(s) like simp, such as to_poly at h, which is for selective algebraization. Step 1 and its reverse can also serve as a bridge between different derived expressions.

C.2

Proof Efficiency

To investigate the additional proof coverage obtainable under an extended budget by GeoProver, we subsequently conduct a separate run using GPT-5.6-Sol, with a timeout of 24 hours per problem. The dashed vertical line marks the two-hour reference point corresponding to the budget used in the main comparison experiments. Figure 5 covers the 29 formalizations generated by GeoFormalizer using Claude Opus 4.8 proved directly by GeoProver without human repair. Figure 6 reports the corresponding results for the 14 expert-repaired formalizations.

Figure 5: Cumulative distribution of wall-clock time for the 29 proofs of the original formalizations. The dashed vertical line marks the two-hour reference point corresponding to the budget used in the main comparison experiments.

C.3

Detailed Results on Lean-IMO-Bench

Table 6 compares proof success on the 14 original geometry statements in LEAP’s Lean-IMO-Bench. MechGeo obtains kernel-checked proofs for 12 of the 14 original statements in total. For the remaining two statements, GeoProver constructs Lean-verified counterexamples that expose missing assumptions. After experts repair these two statements, MechGeo proves both corrected versions, yielding faithful verified proofs for all 14 problems. Because the repaired statements differ from the original benchmark inputs, we retain 12/14 as the directly comparable leaderboard result and report 14/14 separately as the final coverage after validation and repair. (See MechGeoBench/LEAP/ in the supplementary material for Lean source code.)

17

Figure 6: Cumulative distribution of wall-clock time for the 14 proofs of the expert-repaired formalizations. The dashed vertical line marks the two-hour reference point corresponding to the budget used in the main comparison experiments. Method Hilbert Gemini 3.1 Pro Goedel-V2-32B Aristotle LEAP MechGeo

Basic (6)

Advanced (8)

Total (14)

0 0 0 1 1 5

0 0 0 0 1 7

0 (0.0%) 0 (0.0%) 0 (0.0%) 1 (7.1%) 2 (14.3%) 12 (85.7%)

Table 6: Verified proofs on the 14 original geometry statements in LEAP’s Lean-IMO-Bench. Baseline results are taken from the official leaderboard.

D

Case Studies

D.1

IMO 2008 P1

An acute-angled triangle ABC has orthocentre H. The circle passing through H with centre the midpoint of BC intersects the line BC at A1 and A2 . Similarly, the circle passing through H with centre the midpoint of CA intersects the line CA at B1 and B2 , and the circle passing through H with centre the midpoint of AB intersects the line AB at C1 and C2 . Show that A1 , A2 , B1 , B2 , C1 , and C2 lie on a circle.

Why global algebraization is difficult. As shown in Figure 7, if there is such a circle, one can show that it has the same center as the circumcircle of △ABC. Denote this center by O, then it suffices to prove OA1 = OA2 = OB1 = OB2 = OC1 = OC2 . A direct coordinate encoding introduces two scalar coordinates for each of A, B, C, H, A1 , A2 , B1 , B2 , C1 , C2 , O, and therefore contains 22 scalar variables. Its 16 quadratic equations consist of two altitude constraints, six collinearity constraints, six midpoint-circle constraints, and two circumcentre con18

Figure 7: IMO 2008 P1 straints. Algebraizing these constraints and the conclusion as a single system creates an unnecessarily large elimination problem. Proof Decomposition. Instead of translating the entire theorem into one large polynomial system, GeoProver first constructs a proof plan. Let Ma , Mb , and Mc denote the midpoints of BC, CA, and AB, respectively. The proof is decomposed into the following obligations: OA21 = OA22 = OMa2 + HMa2 , OB12 = OB22 = OMb2 + HMb2 , OC12 = OC22 = OMc2 + HMc2 , together with OMa2 + HMa2 = OMb2 + HMb2 = OMc2 + HMc2 . These identities immediately imply OA1 = OA2 = OB1 = OB2 = OC1 = OC2 , and therefore the six points lie on a common circle centered at O. Rather than solving one monolithic elimination problem containing all 22 scalar variables and 16 quadratic constraints, GeoProver reduces the proof to several independent polynomial obligations, each involving at most ten scalar variables. The remainder of this section uses the first obligation, OA21 = OMa2 + HMa2 , as a representative example. For the point A1 , the local system only involves the coordinates of A1 , B, C, H, and O. Since Ma is uniquely determined by B and C, the system contains at most ten scalar coordinate variables. Its constraints are simply OB = OC, B, C, A1 are collinear, and Ma A1 = HMa , together with the nondegeneracy condition B ̸= C. Because O is the circumcenter, OMa ⊥ BC. Since A1 , B, and C are collinear, A1 Ma ∥ BC, and therefore A1 Ma ⊥ OMa . Hence OA21 = OMa2 + Ma A21 .

19

Using the circle constraint Ma A1 = HMa , GeoProver derives OA21 = OMa2 + HMa2 . The same argument is then instantiated for A2 , B1 , B2 , C1 , and C2 . The corresponding code is as follows: have h_OA1_sq : Inner.inner R (A1 - O) (A1 - O) = Inner.inner R (Ma - O) (Ma - O) + Inner.inner R (H - Ma) (H - Ma) := by calc Inner.inner R (A1 - O) (A1 - O) = Inner.inner R (A1 - Ma) (A1 - Ma) + Inner.inner R (Ma - O) (Ma - O) + 2 * Inner.inner R (A1 - Ma) (Ma - O) := by rw [inner_sq_expand A1 Ma O] _ = Inner.inner R (H - Ma) (H - Ma) + Inner.inner R (Ma - O) (Ma - O) + 2 * Inner.inner R (A1 - Ma) (Ma - O) := by rw [h_distA1_sq] _ = Inner.inner R (H - Ma) (H - Ma) + Inner.inner R (Ma - O) (Ma - O) + 2 * (0 : R) := by rw [h_inner_A1_zero] _ = Inner.inner R (Ma - O) (Ma - O) + Inner.inner R (H - Ma) (H - Ma) := by ring

D.2

IMO 2007 P2

Informal Statement Consider five points A, B, C, D and E such that ABCD is a parallelogram and BCED is a cyclic quadrilateral. Let l be a line passing through A. Suppose that l intersects the interior of the segment DC at F and intersects line BC at G. Suppose also that EF = EG = EC. Prove that l is the bisector of angle DAB.

Formal Statement

(generated by GeoFormalizer and repaired manually)

theorem IMOBench_IMO_2007_p2 : ∀ A : EuclideanSpace R (Fin 2), ∀ B : EuclideanSpace R (Fin 2), ∀ C : EuclideanSpace R (Fin 2), ∀ D : EuclideanSpace R (Fin 2), ∀ E : EuclideanSpace R (Fin 2), ∀ F : EuclideanSpace R (Fin 2), ∀ G : EuclideanSpace R (Fin 2), (¬ LinearIndependent (M := EuclideanSpace R (Fin 2)) R ![A -v B, C -v D] ∧ ¬ LinearIndependent (M := EuclideanSpace R (Fin 2)) R ![A -v D, C -v B]) → AffineIndependent R ![A, B, D] → EuclideanGeometry.Concyclic (P := EuclideanSpace R (Fin 2)) {B, C, E, D} → Sbtw R D F C → Collinear R {A, F, G} → Collinear R {B, C, G} → (Dist.dist (α := EuclideanSpace R (Fin 2)) E F) = (Dist.dist (α := EuclideanSpace R (Fin 2)) E C) → (Dist.dist (α := EuclideanSpace R (Fin 2)) E G) = (Dist.dist (α := EuclideanSpace R (Fin 2)) E C) → (D ̸= A ∧ A ̸= B) → ((EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) D A F) = (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) F A B)) := by sorry

20

Figure 8: The intended configuration of IMO 2007 P2.

Figure 9: An unintended counterexample found by GeoProver in the generated formalization of IMO 2007 P2, where ABCD is degenerate. Counterexample and Repair In the generated formalization, the condition “ABCD is a par−−→ −−→ −−→ −−→ allelogram” is formalized as “AB and CD, as well as AD and CB, are linearly dependent”, i.e. ¬ LinearIndependent R ![A -v B, C -v D] ∧ ¬ LinearIndependent R ![A -v D, C -v B]). The condition “BCED is a cyclic quadrilateral” is formalized as “BCED is concyclic.” The goal is formalized as ∠DAF = ∠F AB. Figure 8 shows the intended configuration, while Figure 9 presents a degenerate counterexample with D = (0, 0), A = (1/5, 0), F = G = (1/2, 0), B = C = (1, 0), E = (3/4, 1), where the parallelogram ABCD is degenerate to a segment, for which ∠DAF = π and ∠F AB = 0. The formalization omits the noncollinearity implicit in “ABCD is a parallelogram.” After adding that A, B, and D are noncollinear (AffineIndependent R ![A, B, D], the green line), GeoProver proves the repaired statement.

D.3

Lean-IMO-Bench Basic 028

Informal Statement In △ABC the altitudes BE and CF intersect at H. A circle (W ) is externally tangent to the Euler circle (E) of △ABC and also tangent to the sides AB and AC at X and Y , respectively, with (W ) being closer to A than the Euler circle. Let I ′ be the incenter of △AEF . Prove that AXI ′ Y is a rhombus.

Formal Statement

(from LEAP and repaired manually)

local notation "R2 " => EuclideanSpace R (Fin 2) theorem PBBasic028 (A B C : R2 ) (tri : AffineIndependent R ![A, B, C])

21

(ω : Sphere R2 ) (hω : midpoint R A B ∈ ω ∧ midpoint R B C ∈ ω ∧ midpoint R C A ∈ ω) (W : Sphere R2 ) (X Y : R2 ) (hX : W.IsTangentAt X (affineSpan R {A, B})) (hY : W.IsTangentAt Y (affineSpan R {A, C})) -- The tangency points lie on the actual sides, not their extended lines. (hXseg : Wbtw R A X B) (hYseg : Wbtw R A Y C) (tangent : W.IsExtTangent ω) (closer : dist A W.center < dist A ω.center) : let E := altitudeFoot ⟨![A, B, C], tri⟩ 1 let F := altitudeFoot ⟨![A, B, C], tri⟩ 2 let H := Triangle.orthocenter ⟨![A, B, C], tri⟩ ∀ tri2 : AffineIndependent R ![A, E, F], let I’ := incenter ⟨![A, E, F], tri2⟩ List.Pairwise (· = ·) [dist A X, dist X I’, dist I’ Y, dist Y A]

A

X

W

Y

I'

F

E

H

B

C

Figure 10: The intended configuration of Lean-IMO-Bench Basic 028 Counterexample and Repair The intended configuration is shown in Figure 10. However, the original formalization does not require X and Y to lie on the segments AB and AC, respectively, although these conditions are necessary for the conclusion to hold. If X and Y lie on the extended lines outside these segments, the quadrilateral AXI ′ Y may become concave, as illustrated in Figure 11. We therefore add Wbtw R A X B and Wbtw R A Y C, as required in the informal statement that the tangency points lie on the actual sides. With these assumptions, GeoProver proves the repaired statement.

22

W H

Y

X I' F E A

C

B

Figure 11: Unintended case allowed by the original formalization of Lean-IMO-Bench Basic 028, where X and Y are outside of the segments AB and AC and thus AXI ′ Y is concave.

D.4

Lean-IMO-Bench Advanced 010

Informal Statement. Let O and G be the circumcenter and centroid of a non-isosceles triangle ABC, respectively. Let H be the foot of the perpendicular from A to BC, and let M be the midpoint of BC. For a point X on the line OG, let the line BX intersect AC at P , and let the line CX intersect AB at Q. Let H1 be the foot of the perpendicular from P to the line AB, and let K be the reflection of A about H1 . Let T be the intersection other than P of the circumcircle of triangle KP Q and the circumcircle of triangle P HM . Prove that, as X moves along the line OG, the point T moves along a fixed circle.

Formal Statement (from LEAP and repaired manually) local notation "R2 " => EuclideanSpace R (Fin 2) theorem PBAdvanced010 -- a triangle ABC (A B C : R2 ) (tri : AffineIndependent R ![A, B, C]) -- ABC is non-isosceles (n_isosceles : [dist A B, dist A C, dist B C].Nodup) (O : R2 ) (hO : O = circumcenter ⟨![A, B, C], tri⟩) (G : R2 ) (hG : G = Finset.centroid R .univ ![A, B, C]) (H : R2 ) (hH : H = altitudeFoot ⟨![A, B, C], tri⟩ 0) (M : R2 ) (hM : M = midpoint R B C) : ∃ ω : Sphere R2 , ∀ (X : R2 ) (hX : Collinear R {X, O, G}) (P : R2 ) (hP : Collinear R {P, B, X} ∧ Collinear R {P, A, C}) (Q : R2 ) (hQ : Collinear R {Q, C, X} ∧ Collinear R {Q, A, B}) (H1 : R2 ) (hH1 : H1 = orthogonalProjection (affineSpan R {A, B}) P) (K : R2 ) (hK : K = reflection (affineSpan R {H1 }) A)

23

-- Non-degeneracy of two triangles (hKPQ : AffineIndependent R ![K, P, Q]) (hPHM : AffineIndependent R ![P, H, M]) -- Circumcircles of them are different

(hcircles : circumsphere (⟨![K, P, Q], hKPQ⟩ : Affine.Simplex R R2 2) ̸= circumsphere (⟨![P, H, M], hPHM⟩ : Affine.Simplex R R2 2))

(T : R2 ) (hT : T ̸= P ∧ Cospherical {T, K, P, Q} ∧ Cospherical {T, P, H, M}), T ∈ ω := by sorry

Figure 12: The intended configuration of Lean-IMO-Bench Advanced 010, where the dashed curve through T is the locus of T

Counterexample and Repair The intended configuration is shown in Figure 12. Figure 13 exhibits a counterexample admitted by the original formalization. Consider the configuration A = (0, 0),

B = (2, 0),

C = ( 12 , 2),

O = (1, 13 16 ),

G = ( 56 , 23 ),

24 H = ( 32 25 , 25 ),

M = ( 45 , 1).

Assume, for contradiction, that a fixed circle ω satisfying the original formalization exists. First, choose X1 = G. The corresponding construction gives P1 = ( 14 , 1),

Q1 = (1, 0),

H11 = ( 14 , 0),

K1 = ( 12 , 0). 24

Figure 13: Counterexample to the original formalization of LEAN-IMO-Bench Advanced 010. The configuration associated with X1 (points with subscript 1 ) makes circumcircles of △K1 P1 Q1 and △P1 H1 M1 the same and thus forces the fixed circle to be this circumcircle, whereas the configuration associated with X0 (points with subscript 0 ) admits a val.id point N not in that circumcircle. Consequently, the circle through K1 , P1 , Q1 and the circle through P1 , H, M coincide with the ninepoint circle Γ9 of △ABC. The points H, M , and Q1 are all distinct from P1 and lie on both circles, so each of them satisfies all the hypotheses imposed on T in the original formalization. They must therefore all lie on ω. Since H, M, Q1 are noncollinear, they determine a unique circle, and hence ω = Γ9 , since Γ9 is the circle through Q1 , H, M . Next, choose the intersection of OG and AB, 1 X0 = ( 14 , 0).

For this choice, the construction degenerates: P0 = H10 = K0 = A,

Q0 = X0 .

Now take 3 1 N = (− 100 , 25 ).

Direct substitution verifies that N lies on the circle through A, H, M , but does not lie on Γ9 . Moreover, {N, K0 , P0 , Q0 } = {N, A, X0 } is concyclic, since N, A, X0 are noncollinear, and {N, P0 , H, M } = {N, A, H, M } 25

is concyclic by the choice of N . Since N ̸= P0 , the point N also satisfies all the hypotheses imposed on T . The original formalization would therefore imply N ∈ ω, contradicting N ∈ / Γ9 = ω. Thus no such fixed circle ω exists. The counterexample exploits the degenerate case that two circumcircles are the same, allowed by the original formalization. The configuration X0 , P0 , Q0 , H10 , K0 is another kind of degenerate configuration, in which triple KP Q is degenerate, while other non-degenerate configurations also contradict as long as its T isn’t in that circumcircle. The phrase “Let T be the intersection other than P of the circumcircle · · · the point T ” implicitly requires both defining triples to be noncollinear and their circumcircles to be distinct. We therefore add these three conditions as explicit hypotheses, as highlighted in green in the formal statement above. With these conditions, GeoProver proves the repaired statement.

D.5

IMO 2026 P2

We record the three artifacts of the IMO 2026 Problem 2 run: the informal problem supplied to GeoFormalizer, the Lean 4 statement it produced, and the proof GeoProver constructed for that statement. Informal Statement. Let ABC be a triangle, and let M and N be the midpoints of AB and AC, respectively. Let K and L be points lying strictly inside triangles BM C and BN C, respectively, such that K lies strictly inside triangle ABL and L lies strictly inside triangle AKC. Suppose that ∠KBA = ∠ACL, ∠LBK = ∠LN C, ∠LCK = ∠BM K. Let O be the circumcenter of triangle AKL. Prove that OM = ON.

Formal Statement. GeoFormalizer deterministically translates the GeoIR program generated for this problem by Claude Opus 4.8 into the Mathlib-native theorem shown in Listing 1. Each condition that a point lies strictly inside a triangle is replaced by the weaker condition that the point belongs to the corresponding convex hull. The resulting formal theorem is therefore stronger than the original statement, and its verified proof immediately implies the original claim. Formal Proof. Using GPT-5.6-Sol, GeoProver produces a 569-line Lean file in a single agent round, with a wall-clock time of 4895.4 seconds. The resulting file compiles without sorry, preserves the audited statement unchanged, and depends only on propext, Classical.choice, and Quot.sound. The complete Lean source code is provided in Appendix F.

E

Additional Experimental Settings

E.1

Lean Toolchain and Computing Platform

All generated proofs were verified on Ubuntu 24.04.3 LTS (Linux x86-64) using Lean 4.27.0 and Mathlib at commit a3a10db. Goedel Prover inference was served on six NVIDIA A800 GPUs using

26

three-way data parallelism and two-way tensor parallelism (DP = 3, TP = 2). Lean verification and external symbolic computation were executed on CPU and did not use the GPUs. The CPU-side workloads were executed on a machine equipped with two AMD EPYC 7H12 processors, providing 128 physical cores and 256 hardware threads, and 251 GiB of RAM. Hilbert’s retrieval encoder was served separately on an NVIDIA RTX A6000 GPU.

E.2

Direct Formalization

The direct formalization evaluates whether an LLM can translate an informal geometry problem directly into a Mathlib-native Lean statement. Each problem receives exactly one generation (pass@1). The original informal problem is supplied verbatim as the user message. The following system prompt is used unchanged for all seven backbones: Translate the given natural-language plane-geometry problem into a single Lean 4 theorem. The theorem will be checked against Lean 4.27.0 with Mathlib imported, so you may use any Mathlib definitions and notations. Name the theorem problem. End the theorem with := by sorry. Do not attempt a proof; we are evaluating the statement only. # Output format Return a JSON object with exactly these fields:

lean the complete theorem as one string; answer for a “find” problem, the numeric or closed-form answer as a string; otherwise null; comment one short sentence describing the formalization choices.

E.3

Euclean

We use the authors’ official release with its prompts unmodified. It formalizes each informal problem in a single agentic run: a coding agent iterates against the Lean compiler, reading elaborator diagnostics through a Lean language-server tool and revising, until the statement elaborates or its ten-minute per-problem budget is exhausted. The released repository targets Lean/Mathlib v4.28.0; we run it on v4.27.0 so that all systems share one toolchain, and the geometry primitives involved are stable across these versions. Every backbone receives the same benchmark and budget, and we decide success by re-elaborating each generated statement in Lean ourselves rather than by the agent’s self-reported status. We measure model calls per problem: how many times the agent loop invokes the LLM. Counts are taken from the agents’ own session logs, one per LLM response, over successfully formalized problems only so that the measurement is comparable across backbones. Every backbone averages at least 14 model calls per problem, and the loop is unbounded within the time budget, so a single hard problem can consume hundreds of calls. GeoFormalizer instead emits one GeoIR program and applies at most four bounded repair rounds, two compiler-guided and two faithfulness-guided, for a worst case of five model calls. In comparison, Euclean requires between 14.0 and 116.4 model calls per successfully formalized problem on average across the evaluated backbones.

27

Model

Mean

Median

Range

GPT-5.6-Sol Claude Opus 4.8 DeepSeek-V4-Pro DeepSeek-V4-Flash Qwen3.7-Max MiniMax-M3 GLM-5.2

16.8 14.0 20.7 21.6 17.0 116.4 18.4

17 14 18 19 16 84 14

7–35 8–26 4–66 4–78 1–47 3–413 3–72

Table 7: Number of model calls per problem under the Euclean baseline (successfully formalized problems; 10-minute budget). The 14–116 values reported in the main text correspond to the range of mean calls across backbones, while the maximum number of calls on a single problem is 413.

E.4

Goedel Prover

We evaluate the released Goedel-Prover-V2-8B checkpoint as a sampling-based prover, which receives only the formal Lean statement. Using the released model’s prompt, we draw 32 independent completions per statement (pass@32) at temperature 1.0, top-p 0.95, and up to 16,384 tokens through vLLM, with no information shared across candidates. We extract the last fenced lean/lean4 block, or the whole response if none is present, and compile it as a standalone file under Lean 4.27.0 and the same Mathlib. A statement counts as solved only if at least one of its 32 candidates elaborates without changing the statement and uses only the permitted Lean axioms. This evaluation of Goedel-Prover-V2-8B is separate from the official Goedel-V2-32B leaderboard result reported in Table 6.

E.5

Numina-Lean-Agent

We use the official release at commit 01d8df2 with its default medium-mode prompt, unmodified, and its default limit of five interaction rounds per run—an internal loop of the agent, not five independent samples. The backbone is DeepSeek-V4-Pro; sampling parameters, including temperature and the thinking budget, are left at the provider’s defaults. Each problem receives a two-hour wall-clock budget and runs against Lean v4.27.0 in a sandbox that exposes the Lean project and toolchain read-only, masks the other problems, and disables network access.

E.6

Hilbert

We use the asynchronous implementation at commit bee1325 with its released configuration, changing only the backbone: the defaults pair a 32B fine-tuned prover with a 120B open-weight informal reasoner, and we replace both with DeepSeek-V4-Pro so that the comparison isolates the proving framework rather than the underlying model. Prompts, retrieval, proof checking, sampling parameters, and the agent’s internal recursion and repair limits are all left as released; the implementation fixes temperature at 0.6. Each problem receives one pass@1 run against Lean v4.27.0 under the same two-hour budget, within which its model calls are not otherwise capped. This modified Hilbert configuration is separate from the official Hilbert leaderboard result reported in Table 6.

28

theorem Midpoints_Interior_AKL : ∀ A : EuclideanSpace R (Fin 2), ∀ B : EuclideanSpace R (Fin 2), ∀ C : EuclideanSpace R (Fin 2), AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, C] → let M := midpoint (P := EuclideanSpace R (Fin 2)) R A B; let N := midpoint (P := EuclideanSpace R (Fin 2)) R A C; ∀ K : EuclideanSpace R (Fin 2), ∀ L : EuclideanSpace R (Fin 2), AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![B, M, C] → AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![B, N, C] → K ∈ convexHull R ({B, M, C} : Set (EuclideanSpace R (Fin 2))) → L ∈ convexHull R ({B, N, C} : Set (EuclideanSpace R (Fin 2))) → AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, L] → AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, K, C] → K ∈ convexHull R ({A, B, L} : Set (EuclideanSpace R (Fin 2))) → L ∈ convexHull R ({A, K, C} : Set (EuclideanSpace R (Fin 2))) → (K ̸= B ∧ B ̸= A) → (A ̸= C ∧ C ̸= L) → (L ̸= B ∧ B ̸= K) → (L ̸= N ∧ N ̸= C) → (L ̸= C ∧ C ̸= K) → (B ̸= M ∧ M ̸= K) → (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) K B A) = (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) A C L) → (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) L B K) = (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) L N C) → (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) L C K) = (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) B M K) → AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, K, L] → ∀ O : EuclideanSpace R (Fin 2), (Dist.dist (α := EuclideanSpace R (Fin 2)) O A) = (Dist.dist (α := EuclideanSpace R (Fin 2)) O K) → (Dist.dist (α := EuclideanSpace R (Fin 2)) O A) = (Dist.dist (α := EuclideanSpace R (Fin 2)) O L) → ((Dist.dist (α := EuclideanSpace R (Fin 2)) O M) = (Dist.dist (α := EuclideanSpace R (Fin 2)) O N))

Listing 1: The Lean 4 statement of IMO 2026 P2 produced by GeoFormalizer, reproduced verbatim from the checked file. The proof term supplied by GeoProver closes this goal without altering any hypotheses.

29

Table 8: GeoIR–Lean Specification The IR notations suffixed with ! are translated into Lean with non-degenerate conditions IR

Lean

Semantics

0. Statements and program structure

point A ;

(A : EuclideanSpace R (Fin 2))

introduce a free point of the plane (a binder of the theorem)

real r ;

(r : R)

introduce a free real parameter (a binder)

circle S ;

(S : EuclideanGeometry.Sphere (EuclideanSpace R (Fin 2)))

introduce a free circle (a binder)

let M = <expr> ;

let M := <expr>

denote a point, a number, or a circle as M

incircle S of A B C ; . . .

∀ h : AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, C], let S := Affine.Simplex.insphere (P := EuclideanSpace R (Fin 2)) ⟨![A, B, C], h⟩; . . .

name the incircle of triangle ABC

assume <prop> ;

<prop> →

a hypothesis; an implication premise before the conclusion

prove <prop>

prop (last statement)

1. Point constructors (values in the type of points)

( x , y )

!2 [(x : R), y]

the point with explicit coordinates

midpoint A B

midpoint (P := EuclideanSpace R (Fin 2)) R A B

midpoint of segment AB

centroid A B C

Finset.centroid (P := EuclideanSpace R (Fin 2)) R (Finset.univ (α := Fin 3)) ![A, B, C]

centroid of triangle ABC

lerp t A B

AffineMap.lineMap (P1 := EuclideanSpace R (Fin 2)) A B (t : R)

the point A + t (B − A) on line AB, t ∈ R

divide A B m n

AffineMap.lineMap (k := R) (P1 := EuclideanSpace R (Fin 2)) A B (m / (m + n) : R)

the point P on AB with AP : PB = m : n

center S

EuclideanGeometry.Sphere.center (S : EuclideanGeometry.Sphere (EuclideanSpace R (Fin 2)))

the centre of circle S

2. Circles (values in the type of circles)

circle O r

(⟨O, r⟩ : EuclideanGeometry.Sphere (EuclideanSpace R (Fin 2)))

the circle with centre O and radius r

3. Predicates (propositions) 3.1 About points and lines (arguments are points) continued on next page

30

Table 8 (continued) IR

Lean

Semantics

collinear A B C

Collinear R {A, B, C}

A, B, C lie on one line

noncollinear A B C

AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, C]

A, B, C form a genuine triangle (not collinear)

parallel A B C D

¬ LinearIndependent (M := EuclideanSpace R (Fin 2)) R ![A -v B, C -v D]

line AB is parallel to line CD (degenerate lines allowed)

nondegenerate_of_parallel A B C D

(A ̸= B ∧ C ̸= D)

non-degeneracy of

parallel! A B C D

(A ̸= B ∧ C ̸= D ∧ ¬ LinearIndependent (M := EuclideanSpace R (Fin 2)) R ![A -v B, C -v D])

parallel with the non-degeneracy conditions built in

perp A B C D

Inner.inner (E := EuclideanSpace R (Fin 2)) R (A -v B) (C -v D) = 0

line AB is perpendicular to line CD

perp! A B C D

(A ̸= B ∧ C ̸= D ∧ Inner.inner (E := EuclideanSpace R (Fin 2)) R (A -v B) (C -v D) = 0)

perpendicular with the non-degeneracy conditions built in

right_angle A B C

Inner.inner (E := EuclideanSpace R (Fin 2)) R (A -v B) (C -v B) = 0

the angle at B (in ABC) is 90◦

nondegenerate_of_right_angle A B C

(A ̸= B ∧ C ̸= B)

non-degeneracy of a right angle ABC

right_angle! A B C

(A ̸= B ∧ C ̸= B ∧ Inner.inner (E := EuclideanSpace R (Fin 2)) R (A -v B) (C -v B) = 0)

right angle with the non-degeneracy conditions built in

parallelogram A B C D

(¬ LinearIndependent (M := EuclideanSpace R (Fin 2)) R ![A -v B, C -v D] ∧ ¬ LinearIndependent (M := EuclideanSpace R (Fin 2)) R ![A -v D, C -v B])

ABCD is a parallelogram (AB ∥ CD and AD ∥ CB)

parallel A B C D

nondegenerate_of_parallelogram AffineIndependent (P := EuclideanSpace A B C D R (Fin 2)) R ![A, B, C]

non-degeneracy of a parallelogram ABCD

parallelogram! A B C D

(AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, C] ∧ ¬ LinearIndependent (M := EuclideanSpace R (Fin 2)) R ![A -v B, C -v D] ∧ ¬ LinearIndependent (M := EuclideanSpace R (Fin 2)) R ![A -v D, C -v B])

parallelogram with the non-degeneracy conditions built in

concyclic A B C D

EuclideanGeometry.Concyclic (P := EuclideanSpace R (Fin 2)) {A, B, C, D}

A, B, C, D lie on one circle (no auxiliary centre needed)

are P A B C concyclic_with_center O

(dist P O = dist A O ∧ dist P O = dist B O ∧ dist P O = dist C O)

P, A, B, C on a circle centred at O continued on next page

31

Table 8 (continued) IR

Lean

Semantics

is X weakly_between A B

Wbtw R A X B

X on segment AB, endpoints allowed

is X strictly_between A B

Sbtw R A X B

X strictly inside segment AB

is X in_convex_hull P1 . . . Pn

X ∈ convexHull R ({P1, . . ., Pn} : Set (EuclideanSpace R (Fin 2)))

X inside the convex hull of P1 , . . . , Pn (n ≤ 6)

nondegenerate_of_line A B

A ̸= B

non-degeneracy of line/segment AB: A ̸= B

nondegenerate_of_triangle A B C

AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, C]

non-degeneracy of triangle ABC (same as noncollinear)

nondegenerate_of_dist_line A B

A ̸= B

non-degeneracy of

dist_line P A B: A ̸= B

nondegenerate_of_angle A B C

(A ̸= B ∧ B ̸= C)

non-degeneracy of angle ABC

convex_quad A B C D

IsConvexQuad A B C D

ABCD is a convex quadrilateral (vertices in cyclic order)

nondegenerate_of_incircle A B C

AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, C]

non-degeneracy of the incircle of ABC: a genuine triangle

nondegenerate_circle r

(r : R) > 0

non-degeneracy of a circle of radius r: r > 0

is_tangent S A B

EuclideanGeometry.Sphere.IsTangent (S : EuclideanGeometry.Sphere (EuclideanSpace R (Fin 2))) (affineSpan R {A, B})

line AB is tangent to circle S

3.2 About circles

3.3 Comparisons (points, circles, or real numbers)

(a = b)

(a = b)

equality

(a != b)

(a ̸= b)

disequality

(a <= b)

(a ≤ b)

less than or equal

(a > b)

(a > b)

greater than

(a >= b)

(a ≥ b)

greater than or equal

(a < b)

(a < b)

less than

(p ∧ q)

conjunction

3.4 Comparisons (real numbers)

3.5 Logic connectives

(p and q)

continued on next page

32

Table 8 (continued) IR

Lean

Semantics

(p or q)

(p ∨ q)

disjunction

(not p)

¬ p

negation

(p iff q)

(p ↔ q)

biconditional

(p -> q)

(p → q)

implication

4. Functions (values in the type of real numbers) 4.1 Arguments are points

dist A B

Dist.dist (α := EuclideanSpace R (Fin 2)) A B

distance |AB|; squared form sq (dist A B) vs.

dist A B ^ 2 dot product of vectors AB and CD

dot A B C D

Inner.inner (E := EuclideanSpace R (Fin 2)) R (A -v B) (C -v D)

dist_line P A B

Dist.dist P distance from point P to ((EuclideanGeometry.orthogonalProjection line AB (V := EuclideanSpace R (Fin 2)) (affineSpan R {A, B})) P)

triangle_area A B C

(|(Module.Basis.orientation <| PiLp.basisFun 2 R (Fin 2)).areaForm (A -v B) (C -v B)| / 2)

the (unsigned) area of triangle ABC

xof P

(P : EuclideanSpace R (Fin 2)).ofLp 0

x-coordinate of a point P

yof P

(P : EuclideanSpace R (Fin 2)).ofLp 1

y-coordinate of a point P

angle A B C

EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) A B C

the undirected angle at B, in radians, in [0, π]

pi

Real.pi

the constant π (angles in radians)

natural number literal, e.g. 2

(2 : R)

any natural literal; numerals are real numbers

degree d

(Real.pi * (d : R) / 180)

d degrees, converted to radians (e.g. degree 90 = π/2)

sin a

Real.sin a

4.2 Real number constants

4.3 Angle and trigonometry

sine (of a radian value, e.g.

sin (angle A B C)) cos a

Real.cos a

cosine (of a radian value, e.g. cos (angle A B C))

sqrt a

Real.sqrt a

real square root

sq a

(a : R) ^ 2

the square of a

abs a

|(a : R)|

absolute value continued on next page

33

Table 8 (continued) IR

Lean

Semantics

radius S

EuclideanGeometry.Sphere.radius (S : EuclideanGeometry.Sphere (EuclideanSpace R (Fin 2)))

the radius of circle S

a + b

a + b

addition

a - b

a - b

subtraction

a * b

a * b

multiplication

a / b

a / b

division

(- a) a ^ 2

-a a ^ 2

unary minus a2

( e )

explicit priority; redundant parentheses are always allowed

4.4 Arithmetic

5. Others

( e )

34

F

A Complete Lean Proof of IMO 2026 P2

The problem statement is provided in Appendix D.5. 1 import 2 import

Mathlib GeoTheorem.ToPolyMacros

3 4 set_option 5 set_option

maxHeartbeats 5000000 maxRecDepth 100000

6 7 private

def dt (a b c d : R) : R := a*c+b*d def cr (a b c d : R) : R := a*d-b*c 9 private def ori (A B C : EuclideanSpace R (Fin 2)) : R := 10 cr (B 0-A 0) (B 1-A 1) (C 0-A 0) (C 1-A 1) 8 private

11 12 private 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44

theorem side_nonneg_of_mem_triangle (A B C X : EuclideanSpace R (Fin 2)) (hX : X ∈ convexHull R ({A,B,C} : Set (EuclideanSpace R (Fin 2)))) : 0 ≤ ori A B C * ori A B X := by apply (convexHull_min (k := R) ?_ ?_) hX · intro Z hZ simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ rcases hZ with hZ | hZ | hZ · subst Z change 0 ≤ ori A B C * ori A B A simp [ori, cr] · subst Z change 0 ≤ ori A B C * ori A B B dsimp [ori, cr] ring_nf norm_num · subst Z change 0 ≤ ori A B C * ori A B C simpa [pow_two] using sq_nonneg (ori A B C) · rw [convex_iff_add_mem] intro P hP Q hQ a b ha hb hab change 0 ≤ ori A B C * ori A B P at hP change 0 ≤ ori A B C * ori A B Q at hQ change 0 ≤ ori A B C * ori A B (a · P + b · Q) have hor : ori A B (a · P + b · Q) = a * ori A B P + b * ori A B Q := by have hb’ : b = 1-a := by linarith rw [hb’] dsimp [ori, cr] ring rw [hor, mul_add] simpa only [mul_assoc, mul_comm, mul_left_comm] using add_nonneg (mul_nonneg ha hP) (mul_nonneg hb hQ)

45 46 private 47 48 49 50 51 52 53

theorem ori_ne_zero_of_affineIndependent (A B C : EuclideanSpace R (Fin 2)) (h : AffineIndependent R ![A,B,C]) : ori A B C ̸= 0 := by to_poly at h dsimp [ori, cr] intro hz apply h linear_combination -hz

54 55 private 56 57 58 59 60 61 62

theorem same_sign_of_oriented (D a b : R) (hD : D ̸= 0) (ha : 0 ≤ D*a) (hb : 0 ≤ D*b) : (0 ≤ a ∧ 0 ≤ b) ∨ (a ≤ 0 ∧ b ≤ 0) := by rcases lt_or_gt_of_ne hD with hD | hD · right constructor <;> nlinarith · left constructor <;> nlinarith

63 64 private

theorem oriented_trans

35

65 66 67 68 69 70 71 72 73

(D E a : R) (hE : E ̸= 0) (hDE : 0 ≤ D*E) (hEa : 0 ≤ E*a) : 0 ≤ D*a := by rcases lt_or_gt_of_ne hE with hE | hE · have hD : D ≤ 0 := by nlinarith have ha : a ≤ 0 := by nlinarith exact mul_nonneg_of_nonpos_of_nonpos hD ha · have hD : 0 ≤ D := by nlinarith have ha : 0 ≤ a := by nlinarith exact mul_nonneg hD ha

74 75 private 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132

theorem three_angle_cross_signs (A B C K L : EuclideanSpace R (Fin 2)) (hABC : AffineIndependent R ![A,B,C]) (hABL : AffineIndependent R ![A,B,L]) (hAKC : AffineIndependent R ![A,K,C]) (hK1 : K ∈ convexHull R ({B, midpoint R A B, C} : Set (EuclideanSpace R (Fin 2)))) (hL1 : L ∈ convexHull R ({B, midpoint R A C, C} : Set (EuclideanSpace R (Fin 2)))) (hK2 : K ∈ convexHull R ({A,B,L} : Set (EuclideanSpace R (Fin 2)))) (hL2 : L ∈ convexHull R ({A,K,C} : Set (EuclideanSpace R (Fin 2)))) : let M := midpoint R A B let N := midpoint R A C ((0 ≤ ori B K A ∧ 0 ≤ ori C A L) ∨ (ori B K A ≤ 0 ∧ ori C A L ≤ 0)) ∧ ((0 ≤ ori B L K ∧ 0 ≤ ori N L C) ∨ (ori B L K ≤ 0 ∧ ori N L C ≤ 0)) ∧ ((0 ≤ ori C L K ∧ 0 ≤ ori M B K) ∨ (ori C L K ≤ 0 ∧ ori M B K ≤ 0)) := by dsimp only let M := midpoint R A B let N := midpoint R A C let D := ori A B C have hD : D ̸= 0 := ori_ne_zero_of_affineIndependent A B C hABC have hAabc : A ∈ convexHull R ({A,B,C} : Set (EuclideanSpace R (Fin 2))) := subset_convexHull R _ (by simp) have hBabc : B ∈ convexHull R ({A,B,C} : Set (EuclideanSpace R (Fin 2))) := subset_convexHull R _ (by simp) have hCabc : C ∈ convexHull R ({A,B,C} : Set (EuclideanSpace R (Fin 2))) := subset_convexHull R _ (by simp) have hMabc : M ∈ convexHull R ({A,B,C} : Set (EuclideanSpace R (Fin 2))) := by exact (convex_convexHull R _).midpoint_mem hAabc hBabc have hNabc : N ∈ convexHull R ({A,B,C} : Set (EuclideanSpace R (Fin 2))) := by exact (convex_convexHull R _).midpoint_mem hAabc hCabc have hKabc : K ∈ convexHull R ({A,B,C} : Set (EuclideanSpace R (Fin 2))) := by apply (convexHull_min (k := R) ?_ (convex_convexHull R _)) hK1 intro Z hZ simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ rcases hZ with hZ | hZ | hZ · simpa [hZ] using hBabc · simpa [M, hZ] using hMabc · simpa [hZ] using hCabc have hLabc : L ∈ convexHull R ({A,B,C} : Set (EuclideanSpace R (Fin 2))) := by apply (convexHull_min (k := R) ?_ (convex_convexHull R _)) hL1 intro Z hZ simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ rcases hZ with hZ | hZ | hZ · simpa [hZ] using hBabc · simpa [N, hZ] using hNabc · simpa [hZ] using hCabc have h11 : 0 ≤ D * ori B K A := by have hh := side_nonneg_of_mem_triangle B M C K (by simpa [M] using hK1 ) dsimp [D, M, ori, cr] at hh ⊢ to_poly at hh nlinarith have h12 : 0 ≤ D * ori C A L := by have hperm : L ∈ convexHull R ({C,N,B} : Set (EuclideanSpace R (Fin 2))) := by rw [show ({C,N,B} : Set (EuclideanSpace R (Fin 2))) =

36

133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200

{B, midpoint R A C, C} by ext Z simp only [N, Set.mem_insert_iff, Set.mem_singleton_iff] aesop] exact hL1 have hh := side_nonneg_of_mem_triangle C N B L hperm dsimp [D, N, ori, cr] at hh ⊢ to_poly at hh nlinarith have h21 : 0 ≤ D * ori B L K := by have hDE := side_nonneg_of_mem_triangle A B C L hLabc have hperm : K ∈ convexHull R ({B,L,A} : Set (EuclideanSpace R (Fin 2))) := by rw [show ({B,L,A} : Set (EuclideanSpace R (Fin 2))) = {A,B,L} by ext Z simp only [Set.mem_insert_iff, Set.mem_singleton_iff] aesop] exact hK2 have hEa := side_nonneg_of_mem_triangle B L A K hperm have hE : ori A B L ̸= 0 := ori_ne_zero_of_affineIndependent A B L hABL apply oriented_trans D (ori A B L) (ori B L K) hE · simpa [D] using hDE · dsimp [ori, cr] at hEa ⊢ nlinarith have h22 : 0 ≤ D * ori N L C := by have hperm : L ∈ convexHull R ({N,C,B} : Set (EuclideanSpace R (Fin 2))) := by rw [show ({N,C,B} : Set (EuclideanSpace R (Fin 2))) = {B, midpoint R A C, C} by ext Z simp only [N, Set.mem_insert_iff, Set.mem_singleton_iff] aesop] exact hL1 have hh := side_nonneg_of_mem_triangle N C B L hperm dsimp [D, N, ori, cr] at hh ⊢ to_poly at hh ⊢ nlinarith have h31 : 0 ≤ D * ori C L K := by have hpermK : K ∈ convexHull R ({A,C,B} : Set (EuclideanSpace R (Fin 2))) := by rw [show ({A,C,B} : Set (EuclideanSpace R (Fin 2))) = {A,B,C} by ext Z simp only [Set.mem_insert_iff, Set.mem_singleton_iff] aesop] exact hKabc have hDE0 := side_nonneg_of_mem_triangle A C B K hpermK have hpermL : L ∈ convexHull R ({C,K,A} : Set (EuclideanSpace R (Fin 2))) := by rw [show ({C,K,A} : Set (EuclideanSpace R (Fin 2))) = {A,K,C} by ext Z simp only [Set.mem_insert_iff, Set.mem_singleton_iff] aesop] exact hL2 have hEa0 := side_nonneg_of_mem_triangle C K A L hpermL have hE : ori A K C ̸= 0 := ori_ne_zero_of_affineIndependent A K C hAKC apply oriented_trans D (ori A K C) (ori C L K) hE · dsimp [D, ori, cr] at hDE0 ⊢ nlinarith · dsimp [ori, cr] at hEa0 ⊢ nlinarith have h32 : 0 ≤ D * ori M B K := by have hperm : K ∈ convexHull R ({M,B,C} : Set (EuclideanSpace R (Fin 2))) := by rw [show ({M,B,C} : Set (EuclideanSpace R (Fin 2))) = {B, midpoint R A B, C} by ext Z simp only [M, Set.mem_insert_iff, Set.mem_singleton_iff] aesop] exact hK1 have hh := side_nonneg_of_mem_triangle M B C K hperm dsimp [D, M, ori, cr] at hh ⊢ to_poly at hh ⊢ nlinarith

37

201 202 203

exact ⟨same_sign_of_oriented D _ _ hD h11 h12, same_sign_of_oriented D _ _ hD h21 h22, same_sign_of_oriented D _ _ hD h31 h32⟩

204 205 private 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248

theorem angle_tangent_of_same_sign (P Q R S T U : EuclideanSpace R (Fin 2)) (hPQ : P ̸= Q) (hRQ : R ̸= Q) (hST : S ̸= T) (hUT : U ̸= T) (ha : EuclideanGeometry.angle P Q R = EuclideanGeometry.angle S T U) (hsign : (0 ≤ cr (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) ∧ 0 ≤ cr (S 0-T 0) (S 1-T 1) (U 0-T 0) (U 1-T 1)) ∨ (cr (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) ≤ 0 ∧ cr (S 0-T 0) (S 1-T 1) (U 0-T 0) (U 1-T 1) ≤ 0)) : cr (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) * dt (S 0-T 0) (S 1-T 1) (U 0-T 0) (U 1-T 1) dt (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) * cr (S 0-T 0) (S 1-T 1) (U 0-T 0) (U 1-T 1) = 0 := by have hc := congrArg Real.cos ha have hs := congrArg Real.sin ha simp only [ToPoly.cos_angle’, ToPoly.inner, ToPoly.vsub_apply] at hc rw [ToPoly.sin_angle’ hPQ hRQ, ToPoly.sin_angle’ hST hUT] at hs simp only [ToPoly.vsub_apply] at hs have hnPQ : ∥P -v Q∥ ̸= 0 := norm_ne_zero_iff.mpr (vsub_ne_zero.mpr hPQ) have hnRQ : ∥R -v Q∥ ̸= 0 := norm_ne_zero_iff.mpr (vsub_ne_zero.mpr hRQ) have hnST : ∥S -v T∥ ̸= 0 := norm_ne_zero_iff.mpr (vsub_ne_zero.mpr hST) have hnUT : ∥U -v T∥ ̸= 0 := norm_ne_zero_iff.mpr (vsub_ne_zero.mpr hUT) field_simp [hnPQ, hnRQ, hnST, hnUT] at hc hs have hs’ : ∥S -v T∥ * ∥U -v T∥ * |cr (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1)| = ∥P -v Q∥ * ∥R -v Q∥ * |cr (S 0-T 0) (S 1-T 1) (U 0-T 0) (U 1-T 1)| := by simpa only [cr, mul_comm, mul_left_comm, mul_assoc] using hs have hs’’ : ∥S -v T∥ * ∥U -v T∥ * cr (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) = ∥P -v Q∥ * ∥R -v Q∥ * cr (S 0-T 0) (S 1-T 1) (U 0-T 0) (U 1-T 1) := by rcases hsign with hsign | hsign · simpa [abs_of_nonneg hsign.1, abs_of_nonneg hsign.2] using hs’ · rw [abs_of_nonpos hsign.1, abs_of_nonpos hsign.2] at hs’ linear_combination -hs’ dsimp [dt, cr] at * have hn : ∥S -v T∥ * ∥U -v T∥ ̸= 0 := mul_ne_zero hnST hnUT apply (mul_eq_zero.mp ?_).resolve_left hn linear_combination ( ((S 0 - T 0) * (U 0 - T 0) + (S 1 - T 1) * (U 1 - T 1)) ) * hs’’ ( ((S 0 - T 0) * (U 1 - T 1) - (S 1 - T 1) * (U 0 - T 0)) ) * hc

249 250 private 251

def cx (A B X : EuclideanSpace R (Fin 2)) : R := dt (B 0-A 0) (B 1-A 1) (X 0-A 0) (X 1-A 1)

252 253 private 254

def cy (A B X : EuclideanSpace R (Fin 2)) : R := cr (B 0-A 0) (B 1-A 1) (X 0-A 0) (X 1-A 1)

255 256 private 257 258 259 260 261 262 263

theorem coordinate_cr (A B P Q R : EuclideanSpace R (Fin 2)) : cr (cx A B P-cx A B Q) (cy A B P-cy A B Q) (cx A B R-cx A B Q) (cy A B R-cy A B Q) = dt (B 0-A 0) (B 1-A 1) (B 0-A 0) (B 1-A 1) * cr (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) := by dsimp [cx, cy, dt, cr] ring

264 265 private 266 267 268

theorem coordinate_dt (A B P Q R : EuclideanSpace R (Fin 2)) : dt (cx A B P-cx A B Q) (cy A B P-cy A B Q) (cx A B R-cx A B Q) (cy A B R-cy A B Q) =

38

269 270 271 272

dt (B 0-A 0) (B 1-A 1) (B 0-A 0) (B 1-A 1) * dt (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) := by dsimp [cx, cy, dt, cr] ring

273 274 private 275 276 277 278 279 280

theorem coordinate_sq (A B P Q : EuclideanSpace R (Fin 2)) : (cx A B P-cx A B Q)^2+(cy A B P-cy A B Q)^2 = dt (B 0-A 0) (B 1-A 1) (B 0-A 0) (B 1-A 1) * ((P 0-Q 0)^2+(P 1-Q 1)^2) := by dsimp [cx, cy, dt, cr] ring

281 282 private 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299

theorem coordinate_tangent (A B P Q R S T U : EuclideanSpace R (Fin 2)) (h : cr (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) * dt (S 0-T 0) (S 1-T 1) (U 0-T 0) (U 1-T 1) dt (P 0-Q 0) (P 1-Q 1) (R 0-Q 0) (R 1-Q 1) * cr (S 0-T 0) (S 1-T 1) (U 0-T 0) (U 1-T 1) = 0) : cr (cx A B P-cx A B Q) (cy A B P-cy A B Q) (cx A B R-cx A B Q) (cy A B R-cy A B Q) * dt (cx A B S-cx A B T) (cy A B S-cy A B T) (cx A B U-cx A B T) (cy A B U-cy A B T) dt (cx A B P-cx A B Q) (cy A B P-cy A B Q) (cx A B R-cx A B Q) (cy A B R-cy A B Q) * cr (cx A B S-cx A B T) (cy A B S-cy A B T) (cx A B U-cx A B T) (cy A B U-cy A B T) = 0 := by rw [coordinate_cr, coordinate_dt, coordinate_dt, coordinate_cr] linear_combination (dt (B 0-A 0) (B 1-A 1) (B 0-A 0) (B 1-A 1))^2 * h

300 301 private 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336

theorem coordinate_core (b u v x y p q : R) (hb : b ̸= 0) (hv : v ̸= 0) (hKB : (x-b)^2+y^2 ̸= 0) (hLC : (p-u)^2+(q-v)^2 ̸= 0) (h1 : cr (x-b) y (-b) 0 * dt (-u) (-v) (p-u) (q-v) dt (x-b) y (-b) 0 * cr (-u) (-v) (p-u) (q-v) = 0) (h2 : cr (p-b) q (x-b) y * dt (p-u/2) (q-v/2) (u/2) (v/2) dt (p-b) q (x-b) y * cr (p-u/2) (q-v/2) (u/2) (v/2) = 0) (h3 : cr (p-u) (q-v) (x-u) (y-v) * dt (b/2) 0 (x-b/2) y dt (p-u) (q-v) (x-u) (y-v) * cr (b/2) 0 (x-b/2) y = 0) : (x * q * ((b^2-u^2-v^2)/2) + y * (p^2+q^2) * (b-u) + (x^2+y^2) * p * (-v) (x^2+y^2) * q * (b-u) y * p * ((b^2-u^2-v^2)/2) x * (p^2+q^2) * (-v)) = 0 := by dsimp [dt, cr] at * let A1 : R := b*(v+y) let B1 : R := 2*(x^2+y^2)-b*(x+u) let A2 : R := -b*v-u*y+v*x let B2 : R := b*u-u*x-v*y let D : R := A1*B2-A2*B1 have bg8 : b * (A1*(p-u)+B1*(q-v))=0 := by dsimp [A1, B1] linear_combination -2*h1-4*h3 have g8 : A1*(p-u)+B1*(q-v)=0 := by exact (mul_eq_zero.mp bg8).resolve_left hb have bg9 : b * (A2*(p-u)+B2*(q-v))=0 := by dsimp [A2, B2] linear_combination h1 have g9 : A2*(p-u)+B2*(q-v)=0 := by

39

337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375

exact (mul_eq_zero.mp bg9).resolve_left hb have hDp : D*(p-u)=0 := by dsimp [D] linear_combination B2*g8-B1*g9 have hDq : D*(q-v)=0 := by dsimp [D] linear_combination A1*g9-A2*g8 have hD : D=0 := by by_contra hnD have hp : p-u=0 := (mul_eq_zero.mp hDp).resolve_left hnD have hq : q-v=0 := (mul_eq_zero.mp hDq).resolve_left hnD apply hLC rw [hp, hq] norm_num have hm : v * ((x-b)^2+y^2) * (x * q * ((b^2-u^2-v^2)/2) + y * (p^2+q^2) * (b-u) + (x^2+y^2) * p * (-v) (x^2+y^2) * q * (b-u) y * p * ((b^2-u^2-v^2)/2) x * (p^2+q^2) * (-v)) = 0 := by dsimp [D, A1, B1, A2, B2] at hD dsimp [A1, B1, A2, B2] at g8 g9 linear_combination (-(b^3*v - 2*b^2*v*x + 2*b*p*u*y + 2*b*q*v*y + b*v*x^2 + b*v*y^2 - 2*p*u*x*y - 2*p*v*y^2 + 2*q*u*y^2 - 2*q*v*x*y)/2)*g8 + (-(b^3*v + 2*b^3*y - 3*b^2*u*y + b^2*v*x 4*b^2*x*y + 2*b*p*u*y + 2*b*p*x*y + 2*b*q*v*y + 2*b*q*y^2 + b*u^2*y + 2*b*u*x*y + b*v^2*y 4*b*v*x^2 - 2*b*v*y^2 + 4*b*x^2*y + 4*b*y^3 4*p*x^2*y - 4*p*y^3 - 2*u*x^2*y - 2*u*y^3 + 2*v*x^3 + 2*v*x*y^2)/2)*g9 + ((-b^2*v + b*u*y + b*v*x - u^2*y - v^2*y)/2)*hD + (2*(b^2*y - b*u*y + b*v*x - 2*b*x*y v*x^2 - v*y^2 + 2*x^2*y + 2*y^3))*h2 have hn : v * ((x-b)^2+y^2) ̸= 0 := mul_ne_zero hv hKB exact (mul_eq_zero.mp hm).resolve_left hn

376 377 theorem 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404

Midpoints_Interior_AKL : ∀ A : EuclideanSpace R (Fin 2), ∀ B : EuclideanSpace R (Fin 2), ∀ C : EuclideanSpace R (Fin 2), AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, C] → let M := midpoint (P := EuclideanSpace R (Fin 2)) R A B; let N := midpoint (P := EuclideanSpace R (Fin 2)) R A C; ∀ K : EuclideanSpace R (Fin 2), ∀ L : EuclideanSpace R (Fin 2), AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![B, M, C] → AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![B, N, C] → K ∈ convexHull R ({B, M, C} : Set (EuclideanSpace R (Fin 2))) → L ∈ convexHull R ({B, N, C} : Set (EuclideanSpace R (Fin 2))) → AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, B, L] → AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, K, C] → K ∈ convexHull R ({A, B, L} : Set (EuclideanSpace R (Fin 2))) → L ∈ convexHull R ({A, K, C} : Set (EuclideanSpace R (Fin 2))) → (K ̸= B ∧ B ̸= A) → (A ̸= C ∧ C ̸= L) → (L ̸= B ∧ B ̸= K) → (L ̸= N ∧ N ̸= C) → (L ̸= C ∧ C ̸= K) → (B ̸= M ∧ M ̸= K) → (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) K B A) = (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) A C L) → (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) L B K) = (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) L N C) → (EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) L C K) =

40

405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472

(EuclideanGeometry.angle (P := EuclideanSpace R (Fin 2)) B M K) → AffineIndependent (P := EuclideanSpace R (Fin 2)) R ![A, K, L] → ∀ O : EuclideanSpace R (Fin 2), (Dist.dist (α := EuclideanSpace R (Fin 2)) O A) = (Dist.dist (α := EuclideanSpace R (Fin 2)) O K) → (Dist.dist (α := EuclideanSpace R (Fin 2)) O A) = (Dist.dist (α := EuclideanSpace R (Fin 2)) O L) → ((Dist.dist (α := EuclideanSpace R (Fin 2)) O M) = (Dist.dist (α := EuclideanSpace R (Fin 2)) O N)) := by intro A B C hABC dsimp only intro K L _ _ hK1 hL1 hABL hAKC hK2 hL2 hKB_A hAC_L hLB_K hLN_C hLC_K hBM_K ha1 ha2 ha3 hAKL O hOA_K hOA_L let M := midpoint R A B let N := midpoint R A C obtain ⟨sg1, sg2, sg3⟩ := three_angle_cross_signs A B C K L hABC hABL hAKC hK1 hL1 hK2 hL2 have t1 := angle_tangent_of_same_sign K B A A C L hKB_A.1 hKB_A.2.symm hAC_L.1 hLC_K.1 ha1 sg1 have t2 := angle_tangent_of_same_sign L B K L N C hLB_K.1 hLB_K.2.symm hLN_C.1 hLN_C.2.symm ha2 sg2 have t3 := angle_tangent_of_same_sign L C K B M K hLC_K.1 hLC_K.2.symm hBM_K.1 hBM_K.2.symm (by simpa [M] using ha3) (by simpa [M] using sg3) have ct1 := coordinate_tangent A B K B A A C L t1 have ct2 := coordinate_tangent A B L B K L N C t2 have ct3 := coordinate_tangent A B L C K B M K t3 let b := cx A B B let u := cx A B C let v := cy A B C let x := cx A B K let y := cy A B K let p := cx A B L let q := cy A B L have hb : b ̸= 0 := by have hBA := hKB_A.2 rw [ne_eq, ToPoly.eq’] at hBA intro hz apply hBA dsimp [b, cx, dt] at hz linear_combination hz have hv : v ̸= 0 := by simpa [v, cy, ori] using ori_ne_zero_of_affineIndependent A B C hABC have hKB’ : (x-b)^2+y^2 ̸= 0 := by have hne := hKB_A.1 rw [ne_eq, ToPoly.eq’] at hne intro hz apply hne have hid : (x-b)^2+y^2 = b*((K 0-B 0)^2+(K 1-B 1)^2) := by dsimp [x, y, b, cx, cy, dt, cr] ring rw [hz] at hid exact (mul_eq_zero.mp hid.symm).resolve_left hb have hLC’ : (p-u)^2+(q-v)^2 ̸= 0 := by have hne := hLC_K.1 rw [ne_eq, ToPoly.eq’] at hne intro hz apply hne have hid : (p-u)^2+(q-v)^2 = b*((L 0-C 0)^2+(L 1-C 1)^2) := by dsimp [p, q, u, v, b, cx, cy, dt, cr] ring rw [hz] at hid exact (mul_eq_zero.mp hid.symm).resolve_left hb have ch1 : cr (x-b) y (-b) 0 * dt (-u) (-v) (p-u) (q-v) -

41

473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540

dt (x-b) y (-b) 0 * cr (-u) (-v) (p-u) (q-v) = 0 := by dsimp [x, y, p, q, u, v, b, cx, cy, dt, cr] at ct1 ⊢ linear_combination ct1 have ch2 : cr (p-b) q (x-b) y * dt (p-u/2) (q-v/2) (u/2) (v/2) dt (p-b) q (x-b) y * cr (p-u/2) (q-v/2) (u/2) (v/2) = 0 := by dsimp [x, y, p, q, u, v, b, N, cx, cy, dt, cr] at ct2 ⊢ to_poly at ct2 linear_combination ct2 have ch3 : cr (p-u) (q-v) (x-u) (y-v) * dt (b/2) 0 (x-b/2) y dt (p-u) (q-v) (x-u) (y-v) * cr (b/2) 0 (x-b/2) y = 0 := by dsimp [x, y, p, q, u, v, b, M, cx, cy, dt, cr] at ct3 ⊢ to_poly at ct3 linear_combination ct3 have hF := coordinate_core b u v x y p q hb hv hKB’ hLC’ ch1 ch2 ch3 let ox := cx A B O let oy := cy A B O have eK : 2*ox*x+2*oy*y-(x^2+y^2)=0 := by have hh := hOA_K to_poly at hh have hcO := coordinate_sq A B O A have hcK := coordinate_sq A B O K have heq : (cx A B O-cx A B A)^2+(cy A B O-cy A B A)^2 = (cx A B O-cx A B K)^2+(cy A B O-cy A B K)^2 := by rw [hcO, hcK, hh] dsimp [ox, oy, x, y, cx, cy, dt, cr] at heq ⊢ linear_combination heq have eL : 2*ox*p+2*oy*q-(p^2+q^2)=0 := by have hh := hOA_L to_poly at hh have hcO := coordinate_sq A B O A have hcL := coordinate_sq A B O L have heq : (cx A B O-cx A B A)^2+(cy A B O-cy A B A)^2 = (cx A B O-cx A B L)^2+(cy A B O-cy A B L)^2 := by rw [hcO, hcL, hh] dsimp [ox, oy, p, q, cx, cy, dt, cr] at heq ⊢ linear_combination heq have hdet : x*q-y*p ̸= 0 := by have hori := ori_ne_zero_of_affineIndependent A K L hAKL have hc := coordinate_cr A B K A L have hxy : x*q-y*p = b*ori A K L := by dsimp [x, y, p, q, b, cx, cy, dt, cr, ori] at hc ⊢ linear_combination hc intro hz apply hori have hp : b * ori A K L = 0 := by rw [← hxy, hz] exact (mul_eq_zero.mp hp).resolve_left hb have eW : 2*ox*(b-u)+2*oy*(-v)-(b^2-u^2-v^2)/2=0 := by apply (mul_eq_zero.mp ?_).resolve_left hdet linear_combination (x*(-v)-y*(b-u))*eL (p*(-v)-q*(b-u))*eK - hF have hscalar : (ox-b/2)^2+oy^2 = (ox-u/2)^2+(oy-v/2)^2 := by linear_combination (-1/2)*eW have cxM : cx A B M = b/2 := by dsimp [M, b, cx, dt] to_poly ring have cyM : cy A B M = 0 := by dsimp [M, cy, cr] to_poly ring

42

541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569

have cxN : cx A B N = u/2 := by dsimp [N, u, cx, dt] to_poly ring have cyN : cy A B N = v/2 := by dsimp [N, v, cy, cr] to_poly ring have hcoord : (cx A B O-cx A B M)^2+(cy A B O-cy A B M)^2 = (cx A B O-cx A B N)^2+(cy A B O-cy A B N)^2 := by rw [cxM, cyM, cxN, cyN] simpa [ox, oy] using hscalar have hcM := coordinate_sq A B O M have hcN := coordinate_sq A B O N have hprod : b * (((O 0-M 0)^2+(O 1-M 1)^2) ((O 0-N 0)^2+(O 1-N 1)^2)) = 0 := by change dt (B 0-A 0) (B 1-A 1) (B 0-A 0) (B 1-A 1) * (((O 0-M 0)^2+(O 1-M 1)^2) ((O 0-N 0)^2+(O 1-N 1)^2)) = 0 rw [mul_sub, ← hcM, ← hcN] exact sub_eq_zero.mpr hcoord have hz := (mul_eq_zero.mp hprod).resolve_left hb to_poly dsimp [M, N] at hz to_poly at hz nlinarith

43

Related documents

• Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing#319726
• Spécification technique (pour mise à jour). Boîte de vérrouillage pour palonnier automatique#129160
• When Geometry Becomes Necessary: Constraint Mismatch and Iterative Geometric Modelling in Mixed#152737
• Simplified Engineering for Architects and Builders#473636
• Geometry-Based Metrics for Early-Stage Hull-Form Producibility Screening#1064088