MechGeo：在 Lean 4 中自动形式化并证明欧氏几何

MechGeo 是原生集成 Mathlib 的智能体框架，联合处理欧氏几何题的忠实形式化与内核认证证明。GeoFormalizer 将自然语言转为 GeoIR 和 Lean 4，并通过结构诊断、语义评估迭代修复；GeoProver 规划证明、生成引理并选择性代数化子目标。43 道历史 IMO 几何题中，29 道被证明，14 道被 Lean 核验为反例并在专家修正后全部证明；Lean-IMO-Bench 的 14 题中证明 12 道并形式反驳 2 道。