让每一个几何想法，
都经得起形式验证。

从自然语言到 GeoIR，再到 Lean 内核检查。MechGeo 将直觉转化为透明、可编辑、可复现的机器证明。