← All papers
First page of Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

Linbin Tang, Jingyan You, Zilin Kang, Hanzhang Liu, Sophia Zhang, Zenan Li, Chenrui Cao, Liangcheng Song, Jiaao Wu, Xian Zhang, Fan Yang

cs.AI Jun 17, 2026 · v1
Autoformalizes natural-language geometry problems into Lean 4 statements using native Mathlib Euclidean space constructs, producing large datasets for prover training.
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.

Formal reasoning systems handle algebra and number theory in Lean, but geometry still relies on domain-specific languages with weak formal guarantees. Existing geometry-in-Lean efforts use custom axiom systems that are incompatible with Mathlib and contain fewer than 1,100 problems.

Euclean is a four-stage LLM pipeline (constraint explication, configuration anchoring, formalization mapping, iterative repair). It translates informal geometry problems into Lean 4 theorems over Mathlib's EuclideanSpace ℝ (Fin 2). It makes implicit diagrammatic assumptions explicit, such as non-degeneracy via AffineIndependent and ordering via Sbtw. DeepSeek-V3 is used as the generator, with 32 candidates per problem.

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 invali

The pipeline produced OMNI-Geometry (768 competition problems, 98.5% retention) and Numina-Geometry (177,597 problems). Human evaluation gives 48.89% TOP1 and 73.33% TOP5 accuracy. Fine-tuning Goedel v2 on the formalizations raises pass@1 from 13.6% to 15.1%.

ModelPass@1 (%)
Goedel v2 (base)13.6
base + SFT (round 1 passed)15.1
base + DPO (pass/fail pairs)15.0
Downstream prover training (Pass@1)
ConfigurationCompiling
Basic prompting125 (13.0%)
+ concepts formalization mapping254 (26.5%)
+ iterative code repair465 (48.4%)
+ constraints formalization mapping500 (52.1%)
+ configuration anchoring480 (50.0%)
Ablation: compiling formalizations out of 960 candidates