---
title: "MechGeo：在Lean 4中自动形式化并证明欧氏几何的智能体框架"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2608.02295v1"
permalink: "https://feed.astralor.com/items/itm_3112dbbac485bb23803e64ad"
published: "2026-08-03T14:24:12.000Z"
score: 78
channel: "ai"
tags: ["Lean 4","Mathlib","MechGeo","反例引导诊断","欧氏几何","自动形式化"]
---

# MechGeo：在Lean 4中自动形式化并证明欧氏几何的智能体框架

## AI 点评

> 这项工作的亮点在于把反例引入形式化修复流程，并让Lean内核作为最终裁判，真正实现了“机器证明可被机器验证”。对做自动推理、形式化数学和LLM对齐的人来说，这套框架值得认真研究，尤其是它在弱模型上带来的显著提升，说明可靠的中间表示比一味堆模型更管用。

## 速览

MechGeo是一个依托Mathlib的智能体框架，联合解决欧氏几何的忠实自动形式化与可验证证明构建问题。框架中的GeoFormalizer用GeoIR表示非正式问题，确定性翻译为Lean 4，并通过结构诊断与语义评估迭代修复候选语句；GeoProver构建几何证明计划、推导中间引理，并对合适子目标选择性代数化。Singular或SymPy可生成代数证书，但所有证明与反例均经Lean内核校验。在43道历史IMO几何题中，GeoFormalizer生成的形式语句有29个被GeoProver证明，其余14个构造了Lean验证的反例，专家修正后全部得证。加上IMO 2026第2题，该工作成为已知最大的自动化、内核校验的IMO几何Lean证明集合。

## 关键点

- GeoFormalizer通过GeoIR进行确定性翻译和迭代修复，显著提升低能力LLM的自动形式化效果。
- GeoProver采用证明规划、中间引理推导和选择性代数化，所有证明与反例最终由Lean内核严格校验。
- 在43道IMO几何题中，29道被完全自动证明，14道通过反例引导修复后由专家修正得证。
- 在LEAP的Lean-IMO-Bench上，首次成功证明12道几何题，形式化驳斥剩余2道，并证明修复后的语句。

## 全文

We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework, GeoFormalizer represents informal problems in GeoIR, deterministically translates them into Lean 4, and iteratively repairs candidate statements using structural diagnostics and semantic evaluation. GeoProver constructs geometric proof plans, derives intermediate lemmas, and selectively algebraizes suitable subgoals through a library verified in Lean. Singular or SymPy may generate algebraic certificates, but all resulting proofs and counterexamples are checked by Lean's kernel. Experiments across seven LLM backbones show substantial improvements in autoformalization, particularly for models with weaker direct translation performance. On 43 historical IMO geometry problems, GeoFormalizer generates formal statements that GeoProver proves in 29 cases; for the remaining 14, it constructs counterexamples verified in Lean and proves all repaired statements after expert correction. Together with IMO 2026 Problem 2, this yields, to the best of our knowledge, the largest reported collection of automated, kernel-checked Lean proofs for IMO geometry problems. On the 14 geometry statements in LEAP's Lean-IMO-Bench, MechGeo proves 12 for the first time, formally refutes the remaining two, and proves both repaired statements. These results establish counterexample guided diagnosis, geometric reasoning, and certified symbolic computation as a practical foundation for trustworthy formal geometry.

---

引用前请核对原文;本文由星际流动整理:https://feed.astralor.com/items/itm_3112dbbac485bb23803e64ad