Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean
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.
- ▪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 mod
Opening excerpt (first ~120 words) tap to expand
Computer Science > Artificial Intelligence arXiv:2607.19374 (cs) [Submitted on 17 Jun 2026] Title:Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean Authors:Linbin Tang, Jingyan You, Zilin Kang, Hanzhang Liu, Sophia Zhang, Zenan Li, Chenrui Cao, Liangcheng Song, Jiaao Wu, Xian Zhang, Fan Yang View a PDF of the paper titled Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean, by Linbin Tang and 10 other authors View PDF HTML (experimental) 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.
…
Excerpt limited to ~120 words for fair-use compliance. The full article is at arXiv.org.
Discussion
0 commentsMore from arXiv.org
