Pith. sign in

REVIEW 5 major objections 4 minor 18 references

Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

T0 review · 5 major / 4 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read Autoformalizing geometry natively in Lean at 178K problems is feasible if implicit diagrammatic assumptions are turned into explicit hypotheses, and the resulting corpus measurably improves a general theorem prover's geometry success.

desk verdict Large native-Mathlib geometry corpus with a genuinely useful pipeline, but the abstract's dataset-quality claim runs ahead of what the paper's own evidence supports. read the letter →

arxiv 2607.19374 v1 pith:QTNMLZYF submitted 2026-06-17 cs.AI

Linbin Tang , Jingyan You , Zilin Kang , Hanzhang Liu , Sophia Zhang , Zenan Li , Chenrui Cao , Liangcheng Song
show 3 more authors
Jiaao Wu Xian Zhang Fan Yang
This is my paper · ORCID
classification cs.AI
keywords geometryformalizationLeanMathlibautoformalizationnon-degeneracyneuraltheoremprovingEuclideaniterativerepair
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

Euclean claims that the reason geometry lags behind algebra in formal theorem proving is not mathematical but logistical: natural-language geometry statements hide topological orderings, non-degeneracy conditions, and construction side conditions that a standard library like Mathlib refuses to accept implicitly. The paper's central claim is that a four-stage pipeline—explicating constraints, anchoring the configuration from a generated proof sketch, mapping informal terms to Mathlib primitives, and repairing against compiler feedback—can autoformalize plane geometry natively in Lean at a scale of 178,000 problems. As evidence, it presents the largest Lean geometry corpus built this way (768 competition problems plus 177,597 from a general math corpus), with human annotators judging 48.89% of first-ranked formalizations faithful and 73.33% of five-candidate sets faithful. It further shows that a general-purpose theorem prover, trained on algebra and number theory, already proves 13.6% of the formalized statements without geometry-specific training, rising to 15.1% after training on the corpus. If this holds, geometry can be folded into the same kernel-verified, library-backed infrastructure as the rest of mathematics instead of living in separate domain-specific systems.

What carries the argument

The load-bearing object is the type abbreviation Plane := EuclideanSpace R (Fin 2), which embeds every problem in Mathlib's inner-product-space infrastructure. Around it, the pipeline's four stages supply the real mechanism: (1) constraint explication injects explicit hypotheses (point distinctness A ≠ B, strict betweenness Sbtw A P B, affine independence AffineIndependent ![A,B,C], positive radii) so every function application is type-correct; (2) 'prove-first' configuration anchoring generates an informal proof first and reads off the intended topological configuration from its logical dependencies; (3) formalization mapping retrieves canonical Mathlib primitives—angle, dist, sphere, line,

What would settle it

Sample, say, 300 statements at random from Numina-Geometry, and for each one test (a) whether the hypotheses are consistent (no concrete counterexample points exist), (b) whether the conclusion is non-vacuous, and (c) whether a strong prover can prove it. If the proportion of statements that are false or over-strong (hypotheses admit a counterexample) exceeds about 25%, the corpus cannot support the claimed unification; the paper already reports removing exactly such cases from its 100-problem Aristotle evaluation.

Watch

Extended reading notes

Core claim

The central discovery is that native-Mathlib autoformalization of geometry is feasible at scale when the generator is forced to commit to a configuration before writing the statement. The key move is 'prove-first' anchoring: the model first writes an informal proof sketch, and the logical dependencies of that sketch (e.g., an area-summation argument only works if P lies strictly between B and C) determine which topological and non-degeneracy hypotheses the formal statement needs. Those hypotheses are mapped to Mathlib's analytic-geometry vocabulary—Sbtw for strict betweenness, AffineIndependent for triangles, orthogonalProjection for perpendicular feet, Metric.sphere for circles—and the stat

Load-bearing premise

Everything rests on the injected non-degeneracy and betweenness hypotheses matching the intended configuration of the original problem; the paper's own numbers (48.89% TOP1, and only 25 of 100 sampled statements proved after excluding false, trivial, and counterexample cases) show this premise fails on a substantial minority of problems.

Editorial extensions

If this is right

  • Existing general-purpose Lean provers can be pointed at geometry immediately: the base model already proves 13.6% of Numina-Geometry with no geometry-specific training, and SFT/DPO on successful proof traces lifts this to 15.1% and 15.0%.
  • The corpus gives the Mathlib ecosystem 177,597 formally typed geometry statements plus 768 competition problems, letting standard tactics and library theorems be reused for geometry proofs without custom axiom systems or SMT oracles.
  • Because every statement is checked by the Lean kernel, geometry proofs obtained from these statements carry the same formal guarantees as algebra and number-theory proofs, shrinking the trusted computing base.
  • The pipeline itself is a template for other under-formalized domains: constraint explication, configuration anchoring, mapping, and repair is a general recipe for turning informal prose into type-correct statements.
  • Hard problems remain limiting: TOP1 semantic faithfulness drops to 20.00% for difficulty 8+ problems, and the modest downstream gain suggests proof-trace scarcity rather than statement count is the next bottleneck.

Reading between the lines

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

  • A natural next step the paper hints at but does not develop: use the candidate pool itself for semantic filtering—take the TOP5 formalizations of a problem, attempt proofs with a strong prover, and keep statements that are neither trivially provable nor refuted by counterexample; this could push effective fidelity well above the 48.89% TOP1 figure.
  • The 'prove-first' trick should transfer to any diagram-heavy domain (planar graph problems, geometry of numbers, configuration-space arguments in combinatorics): generate the dependent reasoning first, and read the hidden hypotheses off its inference steps.
  • The 13.6→15.1% gain being consistent across two provers suggests the bottleneck is the scarcity of geometry proof traces in existing corpora; the released 178K statements only pay off once a frontier prover generates proofs on them at scale.
  • Text-only formalization means the pipeline's ceiling is set by the precision of the original wording; as written, it will silently miss configurations that are only carried by a diagram, so a multimodal front-end is the condition for extending this to diagram-heavy sources.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 4 minor

Summary. The paper introduces EUCLEAN, a four-stage framework for automatically formalizing natural-language plane-geometry problems into native Mathlib Lean statements, addressing implicit topological and non-degeneracy constraints. It constructs two datasets: OMNI-Geometry (768 competition problems) and Numina-Geometry (177,597 problems), the largest geometry formalization corpus in Lean. The authors validate the pipeline via ablations, a human evaluation on 180 OMNI-Geometry problems (48.89% TOP1, 73.33% TOP5), and downstream fine-tuning of the Goedel v2 theorem prover, reporting Pass@1 improvement from 13.6% to 15.1% on Numina-Geometry. The paper claims this improvement validates dataset quality for unified neural theorem proving.

Significance. If the central claims hold, the paper would provide a valuable, large-scale, Mathlib-native geometry corpus and an automated formalization pipeline that avoids custom axiom systems. The main contribution is the scale and ecosystem compatibility: 177k problems dwarfing previous Lean geometry datasets. The code and datasets are released, and the proof-success transfer from a general prover to geometry is a positive signal. However, the validation evidence is substantially weaker than the abstract suggests: the training/evaluation overlap is in-sample, the human evaluation covers only OMNI-Geometry, and the paper's own Aristotle audit indicates a high rate of false/trivial/counterexample statements in Numina-Geometry.

major comments (5)
  1. [§5.3, Table 5] The headline result — Goedel v2 Pass@1 improving from 13.6% to 15.1% — is computed on the full Numina-Geometry set, which is also the corpus used to collect the SFT/DPO training traces. This is an in-distribution measurement: the model may be learning statement patterns, over-strong hypotheses, or trivial consequences of injected non-degeneracy conditions rather than faithful geometry formalizations. The abstract's clause 'validating dataset quality' is therefore not supported by this experiment. The held-out OMNI-Geometry results in Section D (6.90→7.68%) are more relevant but receive little discussion and lack a control/ablation. The paper should either provide genuine held-out evaluation or substantially qualify the claim.
  2. [§5.3, §G] The Aristotle audit on 100 randomly sampled Numina-Geometry problems is the most direct evidence about the largest part of the corpus. After excluding cases Aristotle refuted as false, dismissed as trivial misformalizations, or gave concrete counterexamples, only 25 problems were proved and 19 remained unresolved. By the authors' own account, this implies roughly 56 of 100 statements failed a basic semantic-fidelity screen. Reporting this as 'a rough but informative lower-bound signal' in the main text does not reconcile with the abstract's unconditional 'validating dataset quality'. The paper should state the exclusion counts explicitly in Section 5.3, discuss what fraction of Numina-Geometry may be semantically unusable, and temper the abstract accordingly.
  3. [§5.2, Table 4] The human evaluation covers only 180 OMNI-Geometry problems with difficulty ≥4.0. No confidence intervals, inter-annotator agreement, or per-annotator consistency are reported, and no human evaluation is performed on Numina-Geometry. Moreover, 48.89% TOP1 means that more than half of the first-ranked formalizations are judged semantically incorrect. The abstract's bare statement 'Human evaluation shows 48.89% TOP1 and 73.33% TOP5 accuracy' omits these caveats and the fact that it applies only to a curated, harder-than-average OMNI subsample, not to the 177k dataset.
  4. [§3.2.2, §6] The 'Prove-First' step generates an informal proof sketch that then determines which configuration and non-degeneracy constraints are injected. This introduces a potential circularity: the formal statement is shaped by the LLM's own sketch, so a flawed sketch can yield over-strong, under-specified, or inconsistent statements. The paper itself acknowledges in Section 6 that 'the LLM to identify and explicate implicit geometric constraints' may overlook necessary conditions or inject redundant/over-strong hypotheses. Given that the Aristotle audit shows a substantial number of false/trivial statements, the paper should quantify how often the proof sketch is at fault and whether the pipeline's output is faithful when the sketch is correct.
  5. [§5.1, pass@3 paired evaluation] The claim that configuration anchoring improves semantic faithfulness despite lowering compilation rate rests on a paired human evaluation on 30 problems with a 7-3 win/loss margin. This sample is far too small to support a robust conclusion, and no significance test or confidence interval is given. Since one of the paper's central methodological innovations is this anchoring step, the evidence should be strengthened or the claim scaled back to 'suggests a net improvement'.
minor comments (4)
  1. [§4.2] The filtering criterion 'problem type == Geometry' is not specified beyond this string. Please provide the exact NuminaMath field and value, and any manual/automatic verification of this label.
  2. [§5.3, §D] The DPO training section mentions '2 generation attempts per problem' but Section D reports 7,148 preference pairs. Please clarify how many problems contributed pairs and whether any filtering was applied to form the preference pairs.
  3. [Table 2] The table labels 'OMNI-Geo' and 'Numina-Geo', while the text uses 'OMNI-Geometry' and 'Numina-Geometry'. Please use consistent names throughout, including in the appendix tables.
  4. [§5.2] The human evaluation reports TOP5 accuracy, but it is unclear how the five candidates were selected from the 32 generations and whether the annotators saw them in a fixed or randomized order. Please provide the annotation protocol.

Circularity Check

0 steps flagged · score 5.0 of 10

The abstract's dataset-quality validation reduces to an in-sample training/evaluation loop; external checks are partial and the paper's own audit undercuts the claim.

full rationale

Much of the paper is non-circular: the Lean type-checking, the human evaluation on 180 OMNI-Geometry problems (48.89% TOP1 / 73.33% TOP5), and the external base-rate 13.6% from Goedel v2 are independent signals. However, the abstract's central validation sentence reduces to an in-sample loop: SFT/DPO training traces are collected on the same 177,597 Numina-Geometry statements used for evaluation, so the 13.6→15.1 gain is a fitting/memorization signal, not a semantic-quality certificate. The 'Prove-First' stage further selects hypotheses from the model's own proof sketch, making subsequent proof success partly endogenous. The paper is unusually honest in Section 6, stating that 'semantic validation remains difficult at corpus scale' and that formalizations 'should not be considered ground truth without expert review'; the Aristotle audit also reveals 56/100 sampled statements were false, trivial, or counterexample cases. These admissions corroborate that the abstract overclaims. Score 5 reflects partial circularity: the headline claim is substantially in-sample, but independent human and external-prover checks prevent the derivation from being entirely circular.

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

The pipeline relies on text-only problem completeness, LLM proof-sketch fidelity, and the R^2 analytic encoding. No new mathematical entities are introduced, and no free parameters are fitted in the derivation — the only tunable quantities are training hyperparameters.

assumptions (3)
  • domain assumption Informal competition geometry problems are fully specified in natural language text; no diagram information is needed.
    Section 6 (Text-Only Formalization) asserts that all relevant properties must be explicitly stated in text. If diagrammatic information (e.g., orientation, betweenness) is required, the generated formalizations are under-specified.
  • domain assumption The 'Prove-First' proof sketch produced by DeepSeek-V3 correctly identifies the intended geometric configuration.
    Section 3.2.2 uses the sketch to determine which betweenness/sidedness constraints to inject. The 48.89% TOP1 human accuracy indicates this assumption fails often.
  • domain assumption Euclidean competition geometry can be faithfully encoded in R^2 using Mathlib's Metric.sphere, affine spans, and orthogonalProjection.
    Section 3.1 chooses Plane = EuclideanSpace R (Fin 2); Section 6 acknowledges that Mathlib's coverage limits expressiveness, so constructions outside this encoding are excluded.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean." pith.science (2026). https://pith.science/paper/QTNMLZYF

@misc{pith2026260719374,
  author       = {Pith},
  title        = {Pith review of: Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QTNMLZYF}},
  note         = {Machine review of arXiv:2607.19374}
}
abstract

Recent formal reasoning systems have reached IMO-level performance, yet they leave a fragmented landscape: algebra and number theory are handled in Lean, while geometry still relies on domain-specific languages with limited formal guarantees. This split increases the trusted computing base and hinders unified model development. Existing geometry-in-Lean efforts (LeanEuclid, LeanGeo) introduce custom axiom systems incompatible with standard Mathlib, and their small scale ($<$ 1,100 problems) limits large-scale training. Native Mathlib autoformalization of geometry, however, poses distinct challenges: implicit diagrammatic assumptions (e.g., topological configuration and non-degeneracy) must be made explicit rather than deferred to external solvers, and models must adapt to Mathlib's small, rapidly evolving geometry infrastructure. We present Euclean, a four-stage framework - constraint explication, configuration anchoring, formalization mapping, and iterative repair - for automatically formalizing geometry in native Mathlib. We construct OMNI-Geometry (768 competition problems) and Numina-Geometry (177,597 problems), the largest geometry formalization dataset in Lean. Human evaluation shows 48.89% TOP1 and 73.33% TOP5 accuracy. Training Goedel v2 on our formalizations improves proof success from 13.6% to 15.1%, validating dataset quality for unified neural theorem proving. Code and datasets: https://github.com/tlb-22/Euclean.

Figures

Figures reproduced from arXiv: 2607.19374 by the authors.

Figure 1
Figure 1. Overview of the EUCLEAN formalization pipeline. Left (Ambiguity in Input): The process begins with an informal natural language statement containing topological ambiguity—for instance, “Point P on BC” could topologically imply a segment, ray, or line. The diagrams illustrate that while the left configuration is the intended solution, the right configuration (on the extension) is invalid for the problem’s logic. Midd… view at source ↗
Figure 2
Figure 2. Example formalization from OMNI-Geometry (HMMT 2011 Problem 794). It illustrates how EUCLEAN makes implicit ge￾ometric information explicit by (i) translating topological ordering into a strict betweenness constraint and (ii) adding non-degeneracy guards required to make triangles well-defined in MATHLIB. This formalization is proved in Section G. onto a line). Accordingly, the pipeline automatically injects AffineI… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

18 extracted references · 1 linked inside Pith

  1. [1]

    The correctness of proofs may depend on random choices during diagram generation

    Orientation Checking.Orientation is determined by numerically generated diagrams without rigorous math- ematical foundation. The correctness of proofs may depend on random choices during diagram generation

  2. [2]

    For example, the rule cyclic A B P Q⇒eqangle P A P B Q A Q B is mathematically incorrect in general configurations

    Incorrect Inference Rules.The deductive database contains invalid rules. For example, the rule cyclic A B P Q⇒eqangle P A P B Q A Q B is mathematically incorrect in general configurations

  3. [3]

    These issues underscore the need for geometry reasoning grounded in verified proof assistants like Lean withMATH- LIB

    Non-degeneracy Conditions.Conditions like non- collinearity are checked by inspecting an internal graph representation rather than through formal reasoning, which is significantly more challenging and error- prone. These issues underscore the need for geometry reasoning grounded in verified proof assistants like Lean withMATH- LIB. F. Comparison with Rela...

    2025

  4. [4]

    Avigad, J., Dean, E

    https://huggingface.co/datasets/AI -MO/NuminaMath-LEAN, 2025. Avigad, J., Dean, E. T., and Mumma, J. A formal system for Euclid’s Elements.Rev. Symb. Log., 2(4):700–768,

    2025

  5. [5]

    The external bisector (perpendicular to internal) has angles $(\pi+\alpha)/2$ and $(\pi-\alpha)/2$, which are not equal unless $\alpha=0$

  6. [6]

    angle_nonneg B A P ]; ·refine’ lt_of_le_of_ne ( EuclideanGeometry

    := by use (r - 1), (1 - s), (s - r); exact⟨by ring, by convert sub_eq_zero.mpr hs ’ using 1 ; ext ; norm_num ; ring, by contrapose! hr ; linarith⟩; obtain⟨a, b, c, h 1, h 2, h 3 ⟩:= h_affine_dep; specialize h_affine { 0, 1, 2 } ( fun i => if i = 0 then a else if i = 1 then b else c ) ; simp_all + decide [ Finset.sum_range_succ ] ; exact h 3.elim ( fun ha ...

  7. [7]

    Let ℓ1 be the line through A perpendicular 17 Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean to AB, ℓ2 the line through B perpendicular to AC, and P=ℓ 1 ∩ℓ 2. FindP C. theorem find_PC (A B C P : Plane) (h_affine_indep : AffineIndependentR![A, B, C]) (hAB : dist A B = 1) (hBC : dist B C = Real.sqrt 7) (hCA : dist C A = ...

  8. [8]

    * (B 1 - A 1) = 0 := by -- Since $P$ lies on the perpendicular line $\ ell_1$, we have $(P - A) \cdot (B - A) = 0$. have hP_ell1 : (P 0 - A 0) * (B 0 - A 0) + (P 1 - A 1) * (B 1 - A 1) = 0 := by have hP_ell1_def : P - v A∈(Submodule.spanR{ B - v A})⊥ := by exact hP.1 convert hP_ell1_def ( B - v A ) ( Submodule. mem_span_singleton_self _ ) using 1 ; norm_n...

Show all 18 references
  1. [9]

    * (C 1 - A 1) = 0 := by obtain⟨hP 1, hP 2 ⟩:= hP; simp_all +decide [ Submodule.mem_orthogonal’ ] ; convert hP 2 ( C - A ) ( Submodule. mem_span_singleton_self _ ) using 1 ; ring; norm_num [ Fin.sum_univ_two, inner ] ; ring!; rw [ Real.sqrt_eq_iff_mul_self_eq_of_pos ] at * <;> ...

  2. [11]

    $v_B, v_C$ are unit vectors

  3. [12]

    $w = v_B + v_C$ is the internal bisector direction

  4. [13]

    The condition $\angle B A P = \angle C A P$ implies $P$ lies on the internal or external bisector

  5. [14]

    As analyzed, for ‘EuclideanGeometry.angle‘ (which is in $[0, \pi]$), the condition $\angle(AB, AP) = \ angle(AC, AP)$ is satisfied by both the internal bisector (angle $\alpha/2$) and the opposite ray ( angle $\pi - \alpha/2$)

  6. [16]

    Thus $P$ must lie on the line spanned by $w$

  7. [17]

    So $P - A$ is collinear with $w$

  8. [18]

    Thus $P = A + t w$. -/ lemma angle_bisector_locus (A B C P : Plane) (hAB : dist A B = 21) (hBC : dist B C = 55) (hCA : dist C A = 56) (h_cos : Real.cos (angle B A C) = 23 / 98) (hP : angle B A P = angle C A P) (hP_ne_A : P̸=A) : let vB := (1 / 21 :R)·(B - A) let vC := (1 / 56 ...

  9. [56]

    :R)·(C - A)∥= 11 / 7 := by -- Calculate the norm of $w$ using the given cosine value. have hw_norm :∥(1 / 21 :R)·(B - A) + (1 / 56 : R)·(C - A)∥ˆ2 = (11 / 7)ˆ2 := by norm_num [ EuclideanSpace.norm_eq, dist_eq_norm’ ] at *; rw [ Real.sq_sqrt ( by positivity ) ] ; rw [ Real.sqrt...

  10. [2009]

    ByteDance Seed Team

    doi: 10.1017/S1755020309990098. ByteDance Seed Team. Seed-prover: Deep and broad reasoning for automated theorem proving, 2025. URL https://arxiv.org/abs/2507.23726. Chou, S.-C. An introduction to Wu’s method for mechanical theorem proving in geometry.Journal of Automated Reas...

    2025 arXiv

Pith tools

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