Euclean Numina-Geometry is a generated Lean 4 / Mathlib geometry
formalization dataset released with the ICML 2026 paper:
Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean
GitHub repository:
https://github.com/tlb-22/EucleanThis release contains 183,796 Numina-derived geometry problems with generated
Lean theorem statements. The formalizations were regenerated with Codex GPT-5.4
using… See the full description on the dataset page:
https://huggingface.co/datasets/tlb-22/euclean-numina-geometry.
