2026
Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean
ICML 2026poster
Recent formal reasoning systems achieve IMO-level performance, but create a fragmented landscape: algebra and number theory use Lean, while geometry relies on domain-specific languages with limited formal guarantees. This fragmentation increases the trusted computing base and hinders unified model d…