Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

Linbin Tang, Jingyan You, Zilin Kang +8

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 relie…