Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

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.

AI systems are becoming good at solving math problems because they learn from many examples checked by computers. Geometry has not benefited as much: large collections of checkable geometry examples are scarce, and geometry problems often leave facts for humans to infer from a picture. When a problem says a point lies "on" a segment, it may require a specific ordering of points or exclude cases where two points coincide. A proof-checking program cannot rely on hidden assumptions; everything must be explicit. We introduce Euclean, a system that turns natural-language geometry problems into precise statements for Lean, a proof-checking program. Euclean makes hidden conditions explicit, translates lines, angles, and circles into Lean's standard mathematical library, Mathlib, and uses Lean's error messages to repair mistakes. Unlike systems built on custom geometry languages or external solvers, Euclean keeps geometry in the same trusted setting as algebra, number theory, and analysis. Using Euclean, we create OMNI-Geometry with 768 competition problems and Numina-Geometry with 177,597 broader problems, the largest Lean geometry formalization dataset to date. These resources give AI systems many more checked geometry examples to learn from and test on, moving geometry toward a unified and reliable foundation.