Pith. sign in

REVIEW 3 major objections 5 minor 3 cited by

LeanGeo: Formalizing Competitional Geometry problems in Lean

T0 review · 3 major / 5 minor · reviewed 2026-08-05 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper establishes the first Lean-based formal system for competition-level Euclidean geometry, backed by a 260-theorem library and a 122-problem benchmark.

desk verdict A genuinely useful formal-geometry library and benchmark, but the 'machine-checked by Lean' claim is ahead of the kernel's actual trust boundary because esmt accepts CVC5 'unsat' without proof reconstruction. read the letter →

arxiv 2508.14644 v1 pith:CSB5XADM submitted 2025-08-20 cs.AI

Chendong Song , Zihan Wang , Frederick Pu , Haiming Wang , Xiaohan Lin , Junqi Liu , Jia Li , Zhengying Liu This is my paper
classification cs.AI MSC 03B3551M0568V20
keywords Lean4EuclideangeometrycompetitionformalverificationSMTsolvingIMOproblemsLLMtheoremprovingreinforcementlearning
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Competition geometry has largely stayed outside formal proof assistants because its proofs lean on diagrams and few geometry theorems are formalized. This paper introduces LeanGeo, a formal system inside the Lean 4 proof assistant that states and proves competition-level geometry problems the way human solvers do: definitions such as midpoint, circumcenter, and radical axis sit on a small set of Euclidean axioms, and a library of 260 manually verified theorems supplies high-level proof steps. On top of it the paper builds LeanGeo-Bench, a 122-problem benchmark that includes every IMO geometry problem since 2000, together with 43 machine-checked formal solutions. Tested LLMs solve at most about a quarter of the benchmark and none of the 62 Olympic/IMO problems; a reinforcement-learning pass lifts one model's first-attempt success rate from about 2.5% to about 11%, indicating the library can support learning. If the framework holds up, olympiad-style diagram reasoning becomes machine-checkable inside the same proof assistant that already hosts algebra and number theory.

What carries the argument

The load-bearing machinery is the LeanGeo theorem library together with the esmt tactic. The library contains 260 manually proved theorems built on SystemE's axiomatic core, plus 52 abbreviations such as Midpoint, Circumcenter, and RadicalAxis that make statements concise. The esmt tactic takes the current hypotheses, the SystemE inference axioms, and the negated goal, and asks the CVC5 SMT solver for an unsatisfiability check; a cache of parsed axiom expressions and a global dependency graph keep repeated calls efficient. On top of it, euclid_apply and euclid_finish let a proof be written as a sequence of theorem applications, mirroring human multi-step arguments. Nine additional axioms, in

What would settle it

Take any LeanGeo proof counted as formal and bypass or disable CVC5, then run only native Lean proof reconstruction; if the script no longer compiles, the 'machine-checked' claim is weakened. Alternatively, derive False in native Lean from the nine declared axioms, which would show the extended SystemE is inconsistent.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that human-style, declarative formalization of competition geometry is feasible in Lean: start from SystemE, a formal axiomatic system for Euclidean geometry; add 52 geometric abbreviations and nine new axioms for circles, similarity, and area; manually prove 260 theorems on top of them; and expose those theorems through euclid tactics that delegate routine side-conditions to an SMT solver. The same layer formalizes a 122-problem benchmark spanning textbook and olympiad problems, including all IMO geometry problems since 2000, and produces 43 Lean-checked solutions, two of them IMO problems. The strongest claim is that LeanGeo is the first framework

Load-bearing premise

The soundness of LeanGeo's verified proofs currently depends on trusting the external CVC5 solver's 'unsatisfiable' answers, because, as the paper itself notes in Section 6.1, those certificates are not yet converted into Lean's native kernel proofs; the system also assumes nine geometry axioms—triangle area, right-triangle sine/cosine, and similarity rules—rather than proving them.

Editorial extensions

If this is right

  • A single Lean environment can now host geometry together with algebra and analysis: IMO 2001 P1 is formalized by importing a trigonometric inequality from Mathlib into the geometric proof, a route isolated geometry systems cannot take.
  • Library-based training works on this benchmark: using the theorem library, an RL pipeline raises first-attempt success on LeanGeo-Bench from 2.52% to 10.92%.
  • Benchmarking becomes standardized: future geometry provers can be compared on machine-checked formal statements, where the best tested LLM reaches 27.05% among four samples and no model solves any of the 62 Olympic/IMO problems.
  • Formal verification is stricter than diagrammatic proof: Lean requires every positional case to be handled, so LeanGeo proofs cover configurations that natural-language and graph-based geometry systems silently ignore.
  • The paper's stated next step, reconstructing CVC5 certificates as native Lean proofs, would make every LeanGeo proof fully kernel-verified and the library a trusted training corpus.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A reader's natural test is to run full native proof reconstruction on the 43 formal solutions; the fraction that still compile without trusting CVC5's unsat answer directly measures how much of the claimed rigor is currently kernel-level.
  • Because the nine new axioms are declared rather than proved, the benchmark's verified status should be read as conditional on SystemE plus those axioms being consistent; checking the axioms against a concrete Euclidean model would make this explicit.
  • The synthetic generation pipeline, which produced 5,000 attempts with 14% full-proof pass rate, could plausibly be redirected from training theorems to generating new contest-style problems, expanding the benchmark without the same human formalization cost.
  • The RL setup's random selection of ten theorems per prompt suggests that, as the library grows beyond 260 theorems, learned theorem retrieval may matter at least as much as proof search.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper introduces LeanGeo, a Lean 4 framework for expressing and proving competition-level Euclidean geometry problems, built on SystemE/LeanEuclid with an SMT-based tactic layer. It contributes a 260-theorem library of high-level geometry theorems, a 122-problem benchmark (LeanGeo-Bench) that includes IMO geometry problems since 2000, 43 formalized benchmark solutions, and an LLM evaluation plus an RL training pipeline. The central claim is that LeanGeo is the first Lean framework capable of human-like, rigorous, machine-checked reasoning about competition geometry, with benchmark results and RL experiments demonstrating current LLM limitations and some improvements after training.

Significance. If the verification claims can be made sound, LeanGeo is a genuinely useful contribution: it provides a large, open-source library of declarative geometry theorems in Lean, a substantial benchmark with IMO coverage, and a testbed for LLM-based theorem proving that is integrated with Mathlib. The human-readable, hierarchical proof style is a real strength compared with flat symbolic traces. The RL data-generation and training pipeline is also a concrete and reproducible contribution. However, the main advertised guarantee—rigorous machine-checked verification using Lean's foundational logic—is currently weakened by the reliance on unverified CVC5 answers and by unproved axioms, and the benchmark contains a nontrivial in-distribution component. These issues are fixable but are load-bearing for the paper's headline claims.

major comments (3)
  1. [§3.2, §6.1] The central verification claim is not currently established. Section 3.2 states that the esmt tactic passes local hypotheses, SystemE axioms, and the negated goal to CVC5 and accepts an `unsat` answer as a proof of entailment. Section 6.1 explicitly admits that these certificates are not converted into native Lean proofs and lists end-to-end soundness as future work. Since euclid_intros, euclid_apply, and euclid_finish (Appendix C.1; Listings 6, 7, 10) all delegate to this SMT path, every library theorem and every one of the 43 benchmark solutions using these tactics is checked by CVC5 and the custom translator, not by the Lean kernel. The abstract's 'rigorous proof verification' and Section 4.1's 'machine-checked in Lean' therefore overstate the guarantee. Please either implement and document kernel-level proof reconstruction/certificate replay, or explicitly redefine the verification c
  2. [Listing 5, §3.1, Appendix B] The nine axioms in Listing 5 (rightTriangle_sin, rightTriangle_cos, similar_AA/SAS/SSS, triangle_area_foot, threePoints_existCircle, exists_centre, rightAngle_eq_pi_div_two) are assumed, not derived, and no consistency proof relative to SystemE is supplied. These axioms add substantial deductive power; if any of them is inconsistent with SystemE or with the real-number trigonometry used via Mathlib, then every proof that relies on them is vacuous. The problem is compounded by the fact that the library is described in §3.1 as 'formally proved' and 'auto-verified by Lean4 and LeanSMT.' Please either prove these statements from SystemE, provide a semantic model or consistency argument, or explicitly mark them as additional axioms and adjust the 'formally proved library' claim accordingly.
  3. [Table 2, §5.1, Table 3] The benchmark evaluation is substantially in-distribution. Table 2 shows that 10 of 122 problems come from the LeanGeo library itself and 20 are generated by Gemini using the LeanGeo library; Section 5.1 then synthesizes RL training data from the same library by prompting Gemini with five randomly sampled library theorems. Table 3 shows that all evaluated models solve problems mainly in the UG/LB/SP/HSC sections and none solve any OP or IMO problem at pass@4. This suggests that the reported successes partly measure the ability to retrieve and apply the very theorem library that is provided in the prompt, rather than general geometric reasoning. The benchmark is still useful, but the paper should either report a strictly held-out split or explicitly analyze how library overlap affects the reported capabilities and limitations.
minor comments (5)
  1. [§4.1, Table 2] The claim that the IMO section contains 'all IMO geometry problems since 2000' would be easier to verify with an explicit problem list or mapping to IMO years/numbers. Please include one in the appendix.
  2. [Appendix D] The evaluation prompt repeatedly refers to 'LeanEuclid' instead of 'LeanGeo' (e.g., 'You are using a new Lean 4 system called LeanEuclid'). This is confusing for readers and for LLMs being evaluated. Please make the system name consistent.
  3. [Various] There are frequent typos and formatting issues: 'Competitional' in the title, 'descrepencies' in Appendix B, 'High Shool' in Table 2, and Listing 2's caption contains 'tactic usage]Example'. A thorough proofreading pass is needed.
  4. [§4.2] Please clarify the exact definition of pass@k and the relationship between 'OVERALL SUCCESS RATE (%)' and 'SUCCESS NUMBER(pass@4)' in Table 3. As presented, the reader cannot easily reconstruct pass@4 numbers from the rates.
  5. [§3.1] For reproducibility, please include the exact commit hash of the open-source repository and the Lean/Mathlib versions used, since the theorem library and benchmark will evolve.

Circularity Check

2 steps flagged · score 4.0 of 10

LeanGeo's formalization chain is not circular, but the benchmark's Library and Synthetic sections are generated from the same LeanGeo library that is supplied to the models and used to synthesize training data, making part of the reported evaluation in-distribution by construction.

  1. other [Table 2 and Section 4.2 (Evaluation Method)]
    "Table 2 lists 'Library(LB) 10 LeanGeo Library Manually Written'; Section 4.2 states the prompt contains 'the full set of theorems from the LeanGeo theorem library'."

    The 10 Library-section goals are themselves entries in the LeanGeo theorem library, and the same library is supplied in the evaluation prompt and loaded into the Lean verification server. An LB theorem can therefore be discharged by directly citing the already-proven library theorem, so success on this section measures retrieval/restatement of a provided result rather than independent geometric reasoning. The paper reports LB separately, and the external HSC/OP/IMO sections are not affected, so this is a partial evaluation circularity rather than a collapse of the central formalization claim.

  2. other [Table 2 and Sections 5.1/5.3 (RL data generation and training)]
    "Table 2: 'Synthetic Problem(SP) 20 LeanGeo Library Generated by gemini'. Section 5.1: 'we prompt it with five randomly sampled theorems from our existing LeanGeo library. The LLM is then instructed to synthesize a new theorem and a corresponding proof'. Section 5.3: 'This training regimen also yields enhanced performance on our evaluation benchmark, with the pass@1 rate rising from 2.52% to 10.92%'."

    The SP section of the benchmark is generated from the LeanGeo library, and the RL training data is synthesized from that same library with the same Gemini-based generative pipeline. Hence a 20-problem block of the benchmark is drawn from the same distribution used to create and train the model; the reported pass@1 increase is partly an in-distribution gain rather than evidence of transfer to unseen geometry. The olympiad-level sections still show zero solves, so the paper's main limitation conclusion is independently supported.

full rationale

LeanGeo's central derivation—encoding SystemE in Lean, building the 260-theorem library from explicit axioms, and producing formalized IMO/HSC solutions—does not exhibit fitted-parameter circularity, imported uniqueness from the authors, or ansatz smuggled via citation. The nine axioms in Listing 5 are explicit assumptions, and the esmt tactic's reliance on CVC5 unsat certificates (Section 3.2, with Section 6.1 conceding 'these certificates must be converted into a native Lean proof') is an external-oracle soundness limitation, not a self-referential reduction. The two steps above are the real self-referential parts: the evaluation benchmark contains 10 library theorems already supplied to the model and 20 synthetic problems generated from the same library, while the RL data is synthesized from that same library. Because the external sections (20 HSC, 19 OP, 43 IMO) are not touched by this and all models score zero on the 62 olympiad-level problems, the central claim retains independent content. Score 4 reflects partial evaluation circularity, not a circular derivation.

Assumptions & free parameters 0 free parameters · 11 assumptions · 0 invented entities

The central claim does not rely on fitted numeric parameters. It relies on inherited SystemE axioms, on nine newly declared axioms in Appendix B / Listing 5, and on trusting CVC5 unsat results without Lean kernel reconstruction. The benchmark's ground truth is also partially expert-validated rather than machine-checked.

assumptions (11)
  • domain assumption SystemE axioms for points, lines, circles, betweenness, congruence, angles, and constructions (inherited from Avigad et al. via LeanEuclid)
    Section 3 states LeanGeo builds on SystemE and inherits most foundational objects and relations; all LeanGeo proofs assume this background.
  • ad hoc to paper triangle_area_foot: triangle area equals (foot distance) * (base length) / 2
    Listing 5; one of nine axioms added because the paper says they cannot be derived from the original SystemE.
  • ad hoc to paper threePoints_existCircle: every non-collinear triangle has a circumcircle
    Listing 5; assumed as an axiom rather than derived.
  • ad hoc to paper exists_centre: every circle has a center
    Listing 5; assumed as an axiom rather than derived.
  • ad hoc to paper rightAngle_eq_pi_div_two: a right angle measures pi/2
    Listing 5; assumed as an axiom rather than derived.
  • ad hoc to paper rightTriangle_sin: sin(angle) = opposite / hypotenuse in a right triangle
    Listing 5; assumed as an axiom rather than derived.
  • ad hoc to paper rightTriangle_cos: cos(angle) = adjacent / hypotenuse in a right triangle
    Listing 5; assumed as an axiom rather than derived.
  • ad hoc to paper similar_AA: equal two angles imply triangle similarity
    Listing 5; assumed as an axiom rather than derived.
  • ad hoc to paper similar_SAS: side-angle-side criterion for triangle similarity
    Listing 5; assumed as an axiom rather than derived.
  • ad hoc to paper similar_SSS: side-side-side criterion for triangle similarity
    Listing 5; assumed as an axiom rather than derived.
  • domain assumption SystemE-specific axioms encoded in SMT commands, e.g., zero_segment_if: |a-b| = 0 implies a = b
    Listing 2 shows Euclidean axiom declarations used by the SMT bridge; these are part of the inherited formal background.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LeanGeo: Formalizing Competitional Geometry problems in Lean." pith.science (2026). https://pith.science/paper/CSB5XADM

@misc{pith2026250814644,
  author       = {Pith},
  title        = {Pith review of: LeanGeo: Formalizing Competitional Geometry problems in Lean},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CSB5XADM}},
  note         = {Machine review of arXiv:2508.14644}
}
read the original abstract

Geometry problems are a crucial testbed for AI reasoning capabilities. Most existing geometry solving systems cannot express problems within a unified framework, thus are difficult to integrate with other mathematical fields. Besides, since most geometric proofs rely on intuitive diagrams, verifying geometry problems is particularly challenging. To address these gaps, we introduce LeanGeo, a unified formal system for formalizing and solving competition-level geometry problems within the Lean 4 theorem prover. LeanGeo features a comprehensive library of high-level geometric theorems with Lean's foundational logic, enabling rigorous proof verification and seamless integration with Mathlib. We also present LeanGeo-Bench, a formal geometry benchmark in LeanGeo, comprising problems from the International Mathematical Olympiad (IMO) and other advanced sources. Our evaluation demonstrates the capabilities and limitations of state-of-the-art Large Language Models on this benchmark, highlighting the need for further advancements in automated geometric reasoning. We open source the theorem library and the benchmark of LeanGeo at https://github.com/project-numina/LeanGeo/tree/master.

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. MIRROR: Learning from the Other View for Multi-Modal Reasoning

    cs.AI 2026-07 conditional novelty 6.0 of 10

    An RL method that selects the best-performing view of each geometry problem as an internal teacher and distills it into weaker views improves VLM reasoning accuracy and consistency.

  2. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

  3. An Ontology-Based Approach to Optimizing Geometry Problem Sets for Skill Development

    math.HO 2025-09 conditional novelty 4.0 of 10

    The paper presents a retrospective ontology-and-solution-graph framework for curriculum design in Euclidean geometry, with a research agenda for automated solution validation.

Reference graph

Works this paper leans on

62 extracted references · 60 canonical work pages · cited by 3 Pith papers

  1. [1]

    EG // AB [07] & EH // AB [10] � EH // EG [20]

    work page

  2. [2]

    Zhitao He, Zongwei Lyu, Dazhong Chen, Dadi Guo, and Yi R Fung

    Accessed on 2025-07-25. Zhitao He, Zongwei Lyu, Dazhong Chen, Dadi Guo, and Yi R Fung. Matp-bench: Can mllm be a good automated theorem prover for multimodal problems? ����� �������� ����������������, 2025. Hiyouga. Geometry3k dataset, 2025. URL https://huggingface.co/datasets/ hiyouga/geometry3k. Predrag Janicic, Julien Narboux, and Pedro Quaresma. The A...

    work page doi:10.1007/s10817-010-9209-7 2025

  3. [3]

    DH = DB [11] & DF = DB [04] � D is the circumcenter of \Delta BHF [22]

    work page

  4. [4]

    D is the circumcenter of \Delta BHF [22] & DB � BA [01] � � ABH = � BFH [23]

    work page

  5. [5]

    D is the circumcenter of \Delta BHF [22] & DB � BA [01] � � ABF = � BHF [24]

    work page

  6. [6]

    := by rw [Real.cos_add] have h22 : cos ( � / 6) = Real.sqrt 3 / 2 := by rw [cos_pi_div_six] have h23 : sin ( � / 6) = 1 / 2 := by rw [sin_pi_div_six] have h24 : sin B * cos (B + � / 6) = (Real.sqrt 3 / 2) * sin B * cos B - (1 / 2) * sin B ˆ 2 := by rw [h21, h22, h23] 16 ring_nf have h25 : (Real.sqrt 3 / 2) * sin B * cos B - (1 / 2) * sin B ˆ 2 � 1 / 4 := ...

    work page 2001

  7. [7]

    EH // EG [20] � E,G,H are collinear [21]

    work page

  8. [8]

    � BFH = � KHB [25] & � BHF = � HKB [26] (Similar Triangles) � BF:BH = BH:BK [27]

    work page

Show all 62 references
  1. [9]

    DF = DB [04] & DH = DB [11] & DE = DB [02] � E,B,F,H are concyclic [28]

  2. [10]

    E,G,H are collinear [21] & G,K,H are collinear [18] & � BFH = � ABH

  3. [11]

    D is the circumcenter of \Delta BFE [29] & DB � BA [01] � � EBA = � EFB [30]

  4. [12]

    E,G,H are collinear [21] & G,K,H are collinear [18] & B,F,K are collinear [19] & � BHF = � ABF [24] & AB // EG [07] � � BHF = � HKB [26]

  5. [13]

    E,B,F,H are concyclic [28] & � EFB = � BEH [31] � EB = BH [32]

  6. [14]

    CE = CA [03] & CG = CA [08] � C is the circumcenter of \Delta AEG [33]

  7. [15]

    DF = DB [04] & DE = DB [02] � D is the circumcenter of \Delta BFE [29]

  8. [16]

    I,G,A are collinear [13] & � BAE = � AGE [34] & EG // AB [07] � � IAB = � BAE [35]

  9. [17]

    E,G,H are collinear [21] & � EFB = � EBA [30] & AB // EG [07] � � EFB = � BEH [31]

  10. [18]

    D is the circumcenter of \Delta BHE [36] & DB � BA [01] � � ABH = � BEH [37]

  11. [19]

    I,B,H are collinear [14] & � ABH = � BEH [37] & EH // AB [10] � � ABE = � IBA [38]

  12. [20]

    C is the circumcenter of \Delta AEG [33] & AC � AB [00] � � BAE = � AGE [34]

  13. [21]

    � IAB = � BAE [35] & � ABE = � IBA [38] (Similar Triangles) � AI = AE [40]

  14. [22]

    DH = DB [11] & DE = DB [02] � D is the circumcenter of \Delta BHE [36]

  15. [23]

    & AB // EG [07] � � BFH = � KHB [25] 19

  16. [24]

    IB:BF = BK:IB [41] & � KBI = � FBI [42] (Similar Triangles) � BK:IK = IB:IF [43]

  17. [25]

    � IAB = � BAE [35] & � ABE = � IBA [38] (Similar Triangles) � BI = BE [39]

  18. [26]

    CF = CA [05] & CG = CA [08] & CE = CA [03] � E,G,F,A are concyclic [45]

  19. [27]

    BF:BH = BH:BK [27] & EB = BH [32] & BI = BE [39] � IB:BF = BK:IB [41]

  20. [28]

    B,F,K are collinear [19] & I,B,H are collinear [14] & � FBH = � FBH

  21. [29]

    � � KBI = � FBI [42]

  22. [30]

    I,B,F,A are concyclic [48] � � IBA = � IFA [49]

  23. [31]

    E,B,F,H are concyclic [28] � � FEH = � FBH [44]

  24. [32]

    E,G,H are collinear [21] & G,K,H are collinear [18] & J,F,A are collinear [15] & � IBA = � IFA [49] & I,B,H are collinear [14] & � ABH = � BEH [37] & EH // AB [10] & AB // EG [07] � � BEK = � JFI [51]

  25. [33]

    E,G,F,A are concyclic [45] � � GEF = � GAF [46]

  26. [34]

    I,G,A are collinear [13] & I,B,H are collinear [14] & � FEH = � FBH

  27. [35]

    J,G,H are collinear [16] & E,G,H are collinear [21] & � BAE = � AFE

  28. [36]

    � IAF = � IBF [47] � I,B,F,A are concyclic [48]

  29. [37]

    � JEA = � AFE [54] & � JAE = � FAE [55] (Similar Triangles) � JA:EA = EA:FA [56]

  30. [38]

    I,B,F,A are concyclic [48] � � IFB = � IAB [50]

  31. [39]

    I,G,A are collinear [13] & J,F,A are collinear [15] & � GAF = � GAF

  32. [40]

    CE = CA [03] & CF = CA [05] � C is the circumcenter of \Delta AEF [52]

  33. [41]

    C is the circumcenter of \Delta AEF [52] & AC � AB [00] � � BAE = � AFE [53]

  34. [42]

    � BEK = � JFI [51] & � BKE = � FJI [60] (Similar Triangles) � BE:IF = BK:IJ [61]

  35. [43]

    BK:IK = IB:IF [43] & BE:IF = BK:IJ [61] & BI = BE [39] � BK:JI = BK:IK [62]

  36. [44]

    & EH // AB [10] & � GEF = � GAF [46] & EG // AB [07] � � IAF = � IBF [47]

  37. [45]

    J,F,A are collinear [15] & � FAE = � FAE [06] � � JAE = � FAE [55]

  38. [46]

    EA:FA = JA:EA [56] & IA = EA [40] � IA:FA = JA:IA [57]

  39. [48]

    � � IAF = � IAJ [58]

  40. [49]

    IA:FA = JA:IA [57] & � IAF = � IAJ [58] (Similar Triangles) � � AIF = � IJA [59]

  41. [50]

    B,F,K are collinear [19] & E,G,H are collinear [21] & G,K,H are collinear [18] & J,F,A are collinear [15] & � AIF = � IJA [59] & I,G,A 20 are collinear [13] & � IFB = � IAB [50] & AB // EG [07] � � BKE = � FJI [60]

  42. [53]

    & AB // EG [07] � � JEA = � AFE [54]

  43. [54]

    PythagoreanTheorem_point

    BF:BK = BF:BK [17] & BK:JI = BK:IK [62] � JI = IK ==========================� � Listing 9: Proof of AlphaGeometry for IMO 2000 Problem 1 In contrast, the LeanGeo proof is structured more hierarchically, perfectly reflecting the problem’s intrinsic geometric structure. The proo...

    2000

  44. [55]

    have hX: P := by

    You can use standard Lean tactics such as <by_cases>, <cases>, <split_ands> and <constructor> <by_contra> to structure your proof. 23 Specifically, you are encouraged to use "have hX: P := by" to divide the whole problems to small proposition. However, you should not use imper...

  45. [56]

    euclid_apply intersection_lines L1 L2 as O

    You should be careful to check the degenerate case and special cases. For example, sometimes you want to get the intersection of two lines. You may use"euclid_apply intersection_lines L1 L2 as O" but before that you should guarantee that the SMT can deduce that L1 and L2 intersects

  46. [57]

    You must ensure that every step in your proof is rigorous, not only in natural language, but in LeanEuclid. For example, in the following proof, <error_example1> theorem altitude_hypotenuse_similar: � (A B C D: Point) (BC : Line), RightTriangle A B C � distinctPointsOnLine B C...

  47. [58]

    euclid_assert

    "euclid_assert" make very few progress in the proof. Try to use less "euclid_assert X", but use more "have h: X := by � � �"

  48. [59]

    *" symbol for multiplication, please ensure there is a space on both sides of the

    When using the " *" symbol for multiplication, please ensure there is a space on both sides of the " *" symbol. For example, the correct expression should be " �(A-M)� * �(B-M)�" instead of " �(A-M)�*�(B-M)�"

  49. [60]

    coll_angles_eq

    Sometimes when chasing angles, especially using "coll_angles_eq" and "coll_supp_angles" you are encouraged to use "line_from points" to construct the between-line, for example, in the following theorem, <error_example> theorem median_is_half_side_implies_right_triangle: � (A B...

  50. [61]

    Right Triangle ABC with right angle ABC

    Take care of the order of parameter. For example, if you want to express "Right Triangle ABC with right angle ABC", you should use "RightTriangle B A C" (First parameter is rightangle) instead of "rightTriangle A B C". When apply lemma or writing formal statement, always check...

  51. [62]

    euclid_apply line_from_points X Y as XY

    At the beginning of your proof, you should firstly using "euclid_apply line_from_points X Y as XY" To obtain all the the line you needed in the problem, if the problem does not give these lines. This step is benificial to the later SMT steps

  52. [63]

    euclid_apply

    When using "euclid_apply", do not add additional condition to it, for example, do not use "euclid_apply coll_supp_angles A E C B h_between_AEC hA". Instead, use "euclid_apply coll_supp_angles A E C B". SMT will automatically search whether the absent condition is satisfied. --...

  53. [2020]

    � " a ":

    doi: 10.1145/3372885.3373824. Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark Barrett. Lean-smt: An smt tactic for discharging proof goals in lean. In������������� ���������� �� �������� ����� ��������...

    2025

  54. [2025]

    Art of Problem Solving

    Accessed on 2025-07-25. Art of Problem Solving. Art of problem solving. Website. URL https:// artofproblemsolving.com. Accessed: 2025-08-12. Jeremy Avigad, Edward Dean, and John Mumma. A formal system for euclid’s elements. ��� ������ �� �������� �����, 2(4):700–768, 2009. Han...

    2025 arXiv

Pith tools

Reviewed August 5, 2026 · model on record in the stance chip above.