MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

Hao Shen, Junyu Guo, Tian Cui +2

We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework,…