Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean
For researchers in neural theorem proving and formal mathematics, Euclean addresses the fragmentation between geometry formalization and mainstream Lean libraries, enabling unified model development and large-scale training.
Euclean introduces a four-stage framework for automatically formalizing geometry problems in Lean's native Mathlib, creating the largest geometry formalization dataset (177,597 problems). Human evaluation shows 48.89% TOP1 and 73.33% TOP5 accuracy, and training Goedel v2 on this data improves proof success from 13.6% to 15.1%.
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.