Pith. sign in

REVIEW 3 major objections 4 minor 12 references

MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

T0 review · 3 major / 4 minor · reviewed 2026-08-04 · deepseek-v4-flash

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

Pith's one-line read Autoformalizing Euclidean geometry is mainly a statement problem, not a proof problem: MechGeo pairs repair-guided formalization with a proof engine whose Lean-verified counterexamples expose missing conditions, yielding kernel-checked proo

desk verdict Solid, well-packaged systems paper with real Lean artifacts, but the '44 automated IMO proofs' headline is softer than it reads: 14 of the 43 historical statements required expert repair before proof. read the letter →

arxiv 2608.02295 v1 pith:CNFDYYSH submitted 2026-08-03 cs.AI cs.LO

Hao Shen , Junyu Guo , Tian Cui , Yuxuan Xiao , Lihong Zhi This is my paper · ORCID
classification cs.AIcs.LO MSC 03B3551M0568V1568T01
keywords autoformalizationEuclideangeometryLean4proofassistantcounterexample-guidedrepairalgebraiccertificatesIMOproblemsagenticreasoning
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

The paper claims that the hard part of formalizing geometry is getting the statement right, not writing the proof. Its two-stage loop first translates an informal problem into a Lean 4 statement via an intermediate representation, scores the translation, and repairs it; then it either proves the statement or refutes it with a formally checked counterexample. On 43 historical IMO geometry problems, the loop produced 29 direct proofs and 14 counterexamples, and all 14 repaired statements were then proved, giving 44 kernel-checked IMO geometry proofs together with IMO 2026 Problem 2. The method also shows that selectively algebraizing only part of a proof, with certificates checked by Lean's kernel, turns intractable coordinate systems into feasible subproblems.

What carries the argument

The load-bearing mechanism is the combination of GeoIR, a compact typed intermediate representation with a deterministic rule-based translation to Mathlib-native Lean 4, and GeoProver's selective algebraization library. The algebraization works through rewrite lemmas that express geometric predicates and quantities as polynomial equalities and inequalities, so the agent can keep structural arguments synthetic and algebraize only chosen subgoals; external computer algebra systems generate certificates, but every certificate and final proof is checked by Lean's kernel. The equivalence-form rewrite rules guarantee that algebraization never strengthens or weakens the statement.

What would settle it

For each of the 14 repaired Lean statements, run the counterexample search again with the added hypotheses in force and free coordinate choice; any configuration that still satisfies the formal assumptions but violates the intended figure — for instance, a labeled intersection falling outside the intended segment or a supposed parallelogram still degenerate — would show the 44-proof claim does not cover that problem. A complementary check is a blind geometrician comparing each repaired statement against the official problem without seeing which conditions were added.

Watch

Extended reading notes

Core claim

The central claim is that trustworthy formalization and certified proof construction can be solved in one verification loop: GeoFormalizer translates an informal problem through a compact typed intermediate language into Mathlib-native Lean 4, scores the candidate against the source text, and repairs it; GeoProver then either proves the statement or refutes it with a Lean-verified counterexample. A counterexample exposes a missing nondegeneracy or point-order condition; once that condition is added, the repaired statement is proved. Applied to 43 historical IMO geometry problems, the loop produced 29 direct proofs, 14 formal counterexamples, and proofs of all 14 repaired statements, and toge

Load-bearing premise

The load-bearing premise is that the only defects in the 14 autoformalized IMO statements were the missing nondegeneracy and point-order conditions that the Lean counterexamples exposed; if any repaired statement still misses an implicit condition, its proof is not a proof of the original IMO problem.

Editorial extensions

If this is right

  • A formal statement is only accepted after the proof-or-refutation loop terminates; human semantic scoring alone missed 22 flawed statements that formal counterexample search later refuted.
  • Missing order and nondegeneracy conditions are not cosmetic: they change whether the theorem is true, and this loop locates them automatically.
  • Decomposing a proof into synthetic lemmas and small polynomial subsystems, as in IMO 2008 P1, makes algebraic discharge feasible where whole-configuration algebraization is not.
  • Structured formalization gives its largest gains for weaker LLM backbones, so formalization quality can be partially decoupled from model strength.
  • The resulting 44-proof collection is a reusable Mathlib artifact, not a one-off output: the same statements and proofs can be extended or rechecked as the library evolves.

Reading between the lines

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

  • The counterexample-as-diagnostic pattern suggests a general methodology for autoformalization: a prover's refusal to prove a statement is a feature, not a bug, because the refusal can be converted into a concrete repair signal for the formalization.
  • Because 14 of 43 statements required repair, informal geometry problems are systematically under-specified; the same is likely true of any diagram-dependent mathematical text, and a similar proof-or-refute loop may be needed in other formalization domains.
  • The loop's outer semantic check still rests on an LLM judge, so the hard guarantee comes from the kernel; the strength of the overall claim is bounded by how faithfully the repaired statements match the intended problems.
  • A testable extension is to apply the same two-stage loop to non-geometric domains — inequalities, extremal problems, or algebraic word problems — where degenerate cases are less well catalogued, to see whether counterexample search generalizes beyond geometry.
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 / 4 minor

Summary. MechGeo is a Lean-4-native agentic system for Euclidean geometry that separates autoformalization (GeoFormalizer) from proof construction (GeoProver). Informal statements are first written in a typed intermediate language GeoIR, deterministically translated to Mathlib, and repaired through compiler-guided and LLM-semantic-judge-guided loops. GeoProver combines synthetic geometric reasoning with selective algebraization and externally generated algebraic certificates, all of which are rechecked in Lean. On 43 historical IMO geometry problems the system proves 29 generated formal statements directly, refutes 14 with Lean-verified counterexamples, and then proves all 14 after expert repair; with IMO 2026 P2 this yields a claimed collection of 44 IMO geometry proofs. On LEAP's Lean-IMO-Bench it proves 12 of 14 original statements, refutes 2, and proves both repaired statements. The paper also reports ablation studies showing the contribution of CAS and algebraization, and it makes the Lean sources publicly available.

Significance. If the claims are taken at face value, this is a significant advance in end-to-end formal geometry: the proofs are kernel-checked, the IMO 2026 P2 proof is printed in full in Appendix F, the algebraization lemmas are verified in Lean, and the repo/Mathlib commit are given. The separation of autoformalization from proving, the use of formal counterexamples to expose missing nondegeneracy assumptions, and the careful axiom ledger are genuine strengths. The main caution is that the headline '44 IMO geometry proofs' depends on 14 expert-repaired statements whose faithfulness to the original informal problems is asserted rather than independently audited; Section 4.2's own data show that human semantic judgments are fallible on exactly this kind of implicit-condition issue. The paper is therefore valuable as a systems contribution, but the central quantitative claim needs to be restated or supported by a stronger faithfulness audit.

major comments (3)
  1. [§4.4, Table 5, Appendix D.2–D.4] The claim of '44 IMO geometry proofs' counts 14 statements that were human-repaired after formal counterexample search. The Lean kernel certifies the repaired statements, not that they express the original IMO problems. The paper says the repairs add conditions implicit in the informal text, but no independent audit of those 14 repairs is reported. This matters because Table 4 shows that 22 of 157 statements initially judged faithful by three human experts were later formally refuted—so expert judgment is demonstrably fallible on precisely this type of missing-degeneracy/order question. Please either (a) restate the headline as '29 autoformalized and proved, 14 proved after expert repair', or (b) provide an independent auditing protocol for the 14 repaired statements (e.g., blind second-expert review or a formal derivation of each added hypothesis from the informal text under stated comp
  2. [§3.1.3, Eq. F=0.7S_judge+0.3S_struct, §4.2] The semantic acceptance criterion uses a single LLM judge (GPT-5.6-Sol) and hand-chosen weights and threshold τ=0.6. No calibration of S_judge against human labels is reported, and the paper's own Table 4 shows large disagreement between human judgments and formal outcomes. Since the word 'faithful' in the title and abstract rests on this semantic evaluation, the paper should report judge accuracy on a labeled subsample, the sensitivity of the headline results to τ, and the inter-rater agreement of the human judges. This is not a complaint about the formal proofs, but about the load-bearing semantic-validation step.
  3. [Appendix D.5, Listing 1] The formal statement of IMO 2026 P2 replaces 'strictly inside' with convex-hull membership and adds several nondegeneracy/order hypotheses (e.g., AffineIndependent ![B,M,C], AffineIndependent ![A,B,L], AffineIndependent ![A,K,C], and the disequalities). The paper asserts that the formal theorem is stronger and therefore the proof transfers. This is plausible, but the implication from the informal hypotheses to each added conjunct is not demonstrated. Because this is a flagship result, please give a short justification or a checkable lemma for each newly added hypothesis, or state explicitly which of them are redundant and which are consequences of the informal 'strictly inside' reading.
minor comments (4)
  1. [Section 3, Figure 2 vs Appendix F, Listing 1] The theorem shown in Figure 2 is named `imo_2026_p2` and has a shorter hypothesis list, while Listing 1 is `Midpoints_Interior_AKL` with additional hypotheses. This is likely an intended simplification, but it is confusing; please add a note that Figure 2 is a schematic excerpt and Listing 1 is the verbatim statement.
  2. [Table 1] Minor formatting glitch: 'Euclean 43 (100) 43 (100)43 (100)' is missing a space before the last 43.
  3. [§4.4] The sentence 'GeoProver proves 28 of the 43 statements generated by GeoFormalizer within two hours, and one additional statement in 2 hours and 6 minutes' is followed later by 'Manual inspection confirms that all 29 are semantically faithful.' The term 'faithful' here is a human judgment; please make that explicit to avoid appearing as a machine-certified property.
  4. [§4.1.2, Table 7] The main text says Euclean makes '14–116 model calls per problem', which is the range of means; the maximum on a single problem is 413. That is clear from Table 7, but the wording in the main text could be read as a per-problem range. Suggest clarifying.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the kernel-verified proof and counterexample claims are self-contained.

full rationale

The paper's central mathematical claims are self-contained: every theorem proof and every formal counterexample is checked by Lean's kernel, so the existence of a proof never depends on the framework's own semantic metric or on a fitted parameter being renamed as a prediction. The autoformalization score F = 0.7*S_judge + 0.3*S_struct is an evaluation instrument, not a premise of any Lean proof, and no quantity is fit to a subset of data and then reported as an independent prediction. The repaired IMO/LEAP statements do involve a semantic faithfulness judgment (e.g., adding AffineIndependent R![A,B,D] in IMO 2007 P2 or segment-membership conditions in Lean-IMO-Bench Basic 028); however, the paper explicitly acknowledges that 'establishing statement faithfulness remains a challenging problem' (Section 4.3) and that 'the repaired statements differ from the original benchmark inputs' (Appendix C.3). That acknowledged assumption is a correctness/overclaim risk, not a circular derivation: the repaired statements are not definitionally identical to the informal problems, and the kernel proofs are not produced by the human repair step. No load-bearing self-citation or imported uniqueness theorem is used; comparisons to Numina-Lean-Agent, Hilbert, Goedel-Prover-V2, and LEAP are external baseline evaluations. Thus, under the required evidentiary standard, no specific circular reduction can be exhibited.

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

The central proof claims are kernel-checked, so no fitted constants or invented entities are needed. The design parameters (0.7/0.3 weights, threshold 0.6) affect autoformalization quality measures, not the Lean proofs. The main epistemic load is the assumption that Mathlib's geometry definitions and the human/LLM semantic audit capture the informal problems.

free parameters (3)
  • F-score weight S_judge = 0.7
    Hand-chosen weight for the semantic judge score in GeoFormalizer's acceptance function; affects which formalizations are accepted but not the correctness of final Lean proofs.
  • F-score weight S_struct = 0.3
    Hand-chosen weight for the structural point-coverage score; design choice, not fitted to the benchmark.
  • Acceptance threshold tau = 0.6
    Statements are accepted when F >= 0.6; chosen to make the structural score decisive only in ambiguous cases (Section 3.1.3).
assumptions (3)
  • domain assumption Mathlib's EuclideanSpace R (Fin 2), Concyclic, convexHull, angle and distance definitions faithfully model the intended Euclidean plane geometry.
    All formal statements and proofs are expressed in Mathlib's Euclidean geometry; if these definitions deviate from informal Euclidean geometry, the kernel-checked proofs would not establish the informal claims.
  • domain assumption Human semantic audit and the LLM semantic judge can determine whether a formal Lean statement matches the informal problem.
    Faithfulness claims for the 44 IMO/LEAP statements rely on manual inspection (Section 4.4) because Lean only checks the formal statement against itself; Table 4 shows human judgments are fallible, with 22/157 initially-faithful statements later refuted formally.
  • ad hoc to paper For IMO 2026 P2, replacing 'strictly inside triangle' with convex-hull membership plus the added nondegeneracy hypotheses yields a statement implied by the informal problem, so the proof transfers to the original claim.
    The paper asserts the resulting formal theorem is stronger than the original statement (Section D.5). This is a semantic claim about the informal text and is not kernel-checked.

how reviews work

0 comments
Cite this review

Pith. "Pith review of MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4." pith.science (2026). https://pith.science/paper/CNFDYYSH

@misc{pith2026260802295,
  author       = {Pith},
  title        = {Pith review of: MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CNFDYYSH}},
  note         = {Machine review of arXiv:2608.02295}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2608.02295 by the authors.

Figure 1
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. … view at source ↗
Figure 2
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 state￾ment formalization through constraint explication, configuration … view at source ↗
Figure 3
Figure 3. a shows the intended configuration, while Figure 3b presents a degenerate counterex￾ample 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 … view at source ↗
Figures from the paper (11 more)
Figure 4
Figure 4. Figure 4: Lean-IMO-Bench Basic 028 [PITH_FULL_IMAGE:figures/full_fig_p012_4.png]
Figure 1
Figure 1. Figure 1: 12 [PITH_FULL_IMAGE:figures/full_fig_p012_1.png]
Figure 5
Figure 5. Figure 5: Cumulative distribution of wall-clock time for the 29 proofs of the original formalizations. [PITH_FULL_IMAGE:figures/full_fig_p017_5.png]
Figure 6
Figure 6. Figure 6: Cumulative distribution of wall-clock time for the 14 proofs of the expert-repaired formal [PITH_FULL_IMAGE:figures/full_fig_p018_6.png]
Figure 7
Figure 7. Figure 7: IMO 2008 P1 straints. Algebraizing these constraints and the conclusion as a single system creates an unneces￾sarily large elimination problem. Proof Decomposition. Instead of translating the entire theorem into one large polynomial system, GeoProver first constructs a…
Figure 8
Figure 8. Figure 8: The intended configuration of IMO 2007 P2. [PITH_FULL_IMAGE:figures/full_fig_p021_8.png]
Figure 9
Figure 9. 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 −−→…
Figure 10
Figure 10. Figure 10: The intended configuration of Lean-IMO-Bench Basic 028 [PITH_FULL_IMAGE:figures/full_fig_p022_10.png]
Figure 11
Figure 11. Figure 11: Unintended case allowed by the original formalization of Lean-IMO-Bench Basic 028, [PITH_FULL_IMAGE:figures/full_fig_p023_11.png]
Figure 12
Figure 12. Figure 12: The intended configuration of Lean-IMO-Bench Advanced 010, where the dashed curve [PITH_FULL_IMAGE:figures/full_fig_p024_12.png]
Figure 13
Figure 13. Figure 13: Counterexample to the original formalization of LEAN-IMO-Bench Advanced 010. The [PITH_FULL_IMAGE:figures/full_fig_p025_13.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

12 extracted references · 4 linked inside Pith

  1. [1]

    convert derived expressions to basic expressions: the “Derived” part, theto_basictactic; 16

  2. [2]

    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 Y...

    arXiv 2026

  3. [3]

    Pn X∈convexHullR({P1,

    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 CollinearR{A, B, C}A, B, Clie on one line noncollinear A B C AffineIndependent (P := EuclideanSpace R(Fin 2))R![A, B, C] A, B, Cform a genuine triangle (not collinear) parallel A B C D¬LinearIndependen...

  4. [4]

    Chendong Song, Zihan Wang, Frederick Pu, Haiming Wang, Xiaohan Lin, Junqi Liu, Jia Li, and Zhengying Liu

    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, J...

    arXiv 2025

  5. [5]

    Others ( e ) ( e )explicit priority; redundant parentheses are always allowed 34 F A Complete Lean Proof of IMO 2026 P2 The problem statement is provided in Appendix D.5. 1import Mathlib 2import GeoTheorem.ToPolyMacros 3 4set_option maxHeartbeats 5000000 5set_option maxRecDepth 100000 6 7private def dt (a b c d :R) :R:= a*c+b*d 8private def cr (a b c d :R...

    2026

  6. [6]

    ABCDis a par- allelogram

    convert basic expressions to algebraic expressions: the “Basic” part, thebasic_to_polytactic. The two steps can also be done in a single tacticto_poly. These three tactics can be called with an extra argumentat POSITION(s)likesimp, such asto_poly at h, which is for selective algebraization. Step 1 and its reverse can also serve as a bridge between differe...

    2008

  7. [7]

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

    Statements and program structure point A ; (A : EuclideanSpaceR(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 (EuclideanSpaceR(Fin 2))) introduce a free circle (a binder) let M = <expr> ; let M := <expr>denote a point, a number, or a c...

  8. [8]

    Point constructors (values in the type of points) ( x , y ) ! 2[(x :R), y]the point with explicit coordinates midpoint A B midpoint (P := EuclideanSpaceR(Fin 2))RA B midpoint of segmentAB centroid A B C Finset.centroid (P := EuclideanSpaceR (Fin 2))R(Finset.univ (α:= Fin 3)) ![A, B, C] centroid of triangleABC lerp t A B AffineMap.lineMap (P1 := EuclideanS...

Show all 12 references
  1. [9]

    Circles (values in the type of circles) circle O r (⟨O, r⟩: EuclideanGeometry.Sphere (EuclideanSpaceR(Fin 2))) the circle with centreO and radiusr

  2. [11]

    F unctions (values in the type of real numbers) 4.1 Arguments are points dist A B Dist.dist (α:= EuclideanSpaceR(Fin 2)) A B distance|AB|; squared formsq (dist A B)vs. dist A B ^ 2 dot A B C D Inner.inner (E := EuclideanSpaceR (Fin 2))R(A - v B) (C -v D) dot product of vectors...

  3. [2024]

    Julien Narboux

    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 ofLecture Notes in Computer Science, pages 2...

    2004 arXiv

  4. [2026]

    Michael Beeson, Julien Narboux, and Freek Wiedijk

    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 arith...

    2026 arXiv

Pith tools

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