MechGeo：从几何规划到选择性代数化，Lean 4攻克44道IMO几何题

MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4

论文原文 ↗ 论文发布 2026-08-03 解读发布 2026-09-09 解读：AI前沿分享

在神经符号数学推理的众多赛道中，欧几里得平面几何一直处于聚光灯下。从能够通过大规模辅助线生成与符号演绎解决大量国际数学奥林匹克（IMO）题目的 AlphaGeometry，到后续结合更广语言表达的 AlphaGeometry2，机器证明在特定几何语言上的突破有目共睹。然而，这些专门的几何求解器大多工作在定制的形式化语言与专有规则系统之中，其证明链条无法直接被通用的交互式定理证明器（ITP）采纳，也难以无缝接入当代数学家广泛使用的形式化数学大本营——Lean 4 及其数学库 Mathlib。

ArXiv URL：https://arxiv.org/abs/2608.02295

将几何问题搬进 Lean 4，表面上看是“把自然语言题目翻译成形式化代码，再交给大模型调库求解”的工程问题，但实际上面临着两座难以逾越的高山：语义失真的自动形式化与组合爆炸的证明搜索。一方面，自然语言的几何题目严重依赖图形直觉与约定俗成的非退化假设（例如“点 $D$ 在线段 $BC$ 上”是否包含端点、$B$ 与 $C$ 是否重合等），若形式化稍有疏漏，写出的 Lean 代码即便顺利通过编译，表达的数学事实也早已偏离原意，甚至沦为伪命题或平凡命题；另一方面，如果纯靠纯几何综合法（Synthetic Geometry），大模型很难在大跨度的辅助线搜索空间中找到目标，而如果直接将全图一次性坐标化（Algebraization），多项式系统将面临极其致命的维数爆炸，现有的计算机代数系统往往会直接卡死。

针对这一困境，研究者提出了面向 Lean 4 与 Mathlib 原生的智能体框架 MechGeo。该框架将自动形式化与形式化证明置于统一的验证闭环中：前半段通过解耦的中间表示语言 GeoIR 实现确定性编译与语义修复；后半段则提出“几何证明规划”与“选择性代数化”相结合的双层求解机制，借助外部代数计算系统（CAS）生成证书，最终全部交由 Lean 4 严格内核（Kernel）完成机器验证。在覆盖 43 道历史 IMO 几何题及 IMO 2026 第 2 题的评测中，MechGeo 实现了全套核验通过的形式化证明；在知名基准 Lean-IMO-Bench 的 14 道几何题上，它首次完成了其中 12 道的核验，并成功反驳且修复了其余 2 道存在非退化漏洞的题目。

隐式假设的幽灵：为什么几何自动形式化频频暴雷？

自然语言几何题目的表达是高度压缩的。人类数学竞赛选手在阅读一道题目时，脑海中浮现的是一幅标准的几何图景。我们天然知晓“三角形 $ABC$”意味着三点不共线，“$P$ 是内角平分线与外接圆的交点”意味着 $P$ 不是顶点 $A$，“点在直线之间”代表着特定的顺序拓扑。

但在形式化系统 Lean 4 中，编译器并不知道这些“不言而喻”的几何直觉。更棘手的是，Mathlib 为了追求代数结构的通用性，其内建的很多几何与代数定义在退化输入下依然可以完成“类型展开（Elaboration）”。这就导致了一个极具欺骗性的现象：一段存在致命逻辑漏洞的形式化命题，在 Lean 4 编译器里能够绿灯通过编译。

举例而言，当自然语言说“$D$ 落在边 $BC$ 上”时，形式化代码可能被写成 $D$ 属于射线、闭线段、开线段，亦或是仅在直线 $BC$ 上。如果漏掉了 $B \neq C$ 或点在开区间的约束，代码在语法和类型层面完全合法，甚至有些退化情况还能被自动证明器用平凡的恒等式“证明”出来，但这道题实际上已经不再是原本的 IMO 竞赛题。以往的形式化研究主要聚焦于“给定已写好的 Lean 命题求证明”，避开了这个源头陷阱；而一旦直面自动形式化（Autoformalization），传统的大模型单步直译就会频繁输出看似合理、实则走样的残缺代码。

不仅编译器无法甄别这种深层语义漂移，就连专业的人类数学研究者在进行人工审查时也极易“被眼睛欺骗”。在 MechGeo 的基准测试评估中，三位专家独立审查了大模型生成的 200 个形式化命题，最初有 157 个被专家认定为忠实翻译；然而后续证明系统利用反例搜索算法，竟在这 157 个“专家认可”的命题中抓出了 22 个存在隐式退化与顺序错误的非真命题。这充分说明，必须在形式化前端引入严格的结构化约束与反例诊断机制。

GeoFormalizer：解耦语法烦恼与语义自纠

为了化解形式化失真，MechGeo 在前端设计了自动形式化模块 GeoFormalizer。该模块由四个核心阶段构成：中间语言生成、规则化确定性翻译、结构与语义打分，以及迭代修复回路。

GeoFormalizer 没有让大模型直接书写繁冗的 Mathlib 代码。Mathlib 的 API 迭代频繁，其类型类的隐式参数、类型强制转换（Coercion）极为严苛，要求大模型在一次推理中同时兼顾数学逻辑、Lean 语法规范和最新的库接口，负担过重。团队设计了一种紧凑、类型安全的中间表示语言 GeoIR。大模型只需在有限的几何语义标记空间内表达几何配置，例如对象的声明（Declarations）、构图操作（Constructions）、几何关系（Geometric Relations）和度量值（Values）。

在得到合法的 GeoIR 规范后，系统通过一个确定性的规则翻译器（Rule-based Translator）将其直接映射为 Mathlib 原生命题。这个翻译器完全由程序逻辑写死，不引入任何大模型的随机性：它把 GeoIR 解析为抽象语法树（AST），再递归遍历并拼装对应的 Lean 4 代码。当 Mathlib 的底层定义发生重构时，开发者只需更新翻译表的映射逻辑，旧有的 GeoIR 就能一键无损迁移，彻底隔离了语义逻辑与底层接口变动的耦合。

翻译完成后的形式化命题并不会立刻入库，而是进入严格的评估过滤网。系统结合语义忠实度评分与结构覆盖率构成综合评分函数：

\[F = 0.7 S_{\mathrm{judge}} + 0.3 S_{\mathrm{struct}}\]

其中 $S_{\mathrm{judge}}$ 由模型评判生成的 Lean 命题与原始自然语言题意之间的对应程度，分为一致（1.0）、部分一致（0.5）与不一致（0.0）；$S_{\mathrm{struct}}$ 则计算几何点集的覆盖率，即 GeoIR 中声明的点与自然语言题干提及点的重合比例。阈值 $\tau$ 被设定为 0.6，这意味着只有当语义判断落入模糊的 0.5 时，点集结构的完整性才具有决定权。未通过阈值或静态检查报错的代码会被退回给构造器，结合类型诊断、断言反例与缺失约束进行多轮自纠，直至生成真正无损原意的形式化目标。

告别全局硬算：GeoProver 的几何规划与选择性代数化

拿到正确、严格的形式化 Lean 命题后，证明引擎 GeoProver 登场。长期以来，机器证明几何定理存在两条路线之争：一条是基于公理体系的“综合几何法”，需要搜索庞大的引理库并添加大量辅助线；另一条是以吴方法（Wu’s Method）和 Gröbner 基为代表的“代数坐标法”，把所有几何条件转为多项式消元。

全局坐标化的痛点在于“状态爆炸”。一道高难度的 IMO 几何题如果直接把所有点设定为坐标变量，会瞬间生成数十个变量和大量高次多项式方程，计算复杂度随贝祖数呈指数级上升，任何顶尖的代数系统都会瞬间内存耗尽。MechGeo 的破局之道在于：以几何规划为宏观骨架，以局部选择性代数化为微观攻坚利器。

GeoProver 仅接收形式化的 Lean 命题作为输入。证明规划智能体首先在不调用底层复杂计算的情况下，还原全局几何构型，撰写一份包含辅助构图、中间关键引理、导角（Angle Chasing）和局部代数关系的有序非形式化证明大纲。这种大纲将一个复杂的全局定理拆解成多个小尺度的局部子目标（Subgoals）。

接下来，系统调用专门构建的 Lean 原生代数化工具库进行“选择性代数化”。该模块由一系列在 Lean 中经过严密形式化核验的等价引理和化简策略 to_poly 构成：

基础向量化：策略 to_basic 首先将高层几何谓词（如共线、共圆、垂直）转化为向量、内积与范数的基本表达。
多项式展开：策略 basic_to_poly 将上述基础向量按选定的坐标基底展开为坐标分量的多项式等式与不等式。

由于 to_poly 所调用的每一条化简规则都是双向等价的已证引理，这种转换在逻辑上绝不会弱化或擅自强化原命题。最关键的是，智能体拥有对化简位置的选择权：它允许一部分适合几何推理的分支保留在 Mathlib 几何引理层，只把真正适合代数计算的复杂代数恒等子目标送进坐标展开。

这种分而治之的威力在 IMO 2008 第 1 题的求解中体现得淋漓尽致。如果不加规划，该题的全局多项式系统包含 22 个标量坐标变量和 16 个二次方程，直接代数求解在工程上完全不可行。而在 GeoProver 的规划下，全局系统被拆解为 6 个仅包含 10 个变量、3 个二次方程与 1 个非零约束的局部小系统，外加两个仅含 2 到 3 个方程的对称子系统，计算开销瞬间下降了数个数量级。

外部代数加速与 Lean 内核审查的双重保险

当选择性代数化将子目标转换为多项式目标后，GeoProver 面临的形式化目标通常呈现为：在假设多项式 $p_1 = 0, \ldots, p_n = 0$ 的前提下，证明目标多项式 $q = 0$。

在 Lean 4 原生环境中，完全依赖内部自带的化简策略（如 ring 或 linarith）处理高次非线性多项式理想隶属问题仍然非常吃力。为此，GeoProver 采取了一种“外脑计算，内部分析”的核验机制：

系统将多项式方程组导出，调用外部高性能计算机代数系统 Singular 或 SymPy。
外部 CAS 计算出 Bézout 恒等式系数（Cofactors）$c_1, \ldots, c_n$，使得目标多项式满足：

\[q = \sum_{i=1}^{n} c_i p_i\]

智能体将这组代数系数写回 Lean 4，构造为一个纯粹的代数重写证明项。

这里的核心原则是外部 CAS 的输出完全不作为可信基（Trusted Computing Base）。Singular 或 SymPy 可以出现浮点误差、实现 bug 甚至崩溃，但它们传回给 Lean 的仅仅是一组候选系数证书；Lean 4 最小内核通过纯粹的符号项还原展开并校验 $\sum c_i p_i - q = 0$ 是否在实数域或复数域上严格成立。如果证书有误，Lean 编译即刻报错，杜绝了符号计算系统的逻辑污染。对于不等式、符号判断和非零边界条件，则依托 Lean 内部的形式化符号引理和分情况讨论进行严格闭环。

不仅能证，还能“驳”。当面对一个可能存在形式化缺陷的命题时，GeoProver 会尝试进行形式化反例搜索。系统通过显式坐标赋值，在 Lean 中构造具体的退化反例点集，并向 Lean 内核提交该反例满足所有假设却违背结论的机器检查证明。这种双向能力不仅保证了证明结果的真值，更成为了修复失真形式化代码的最强探针。

实验评测：从多模型横评到消融真相

为了全方位检验该系统的效能，研究团队构建了包含 200 个几何题目的评测集 MG200（囊括 43 道历史 IMO 几何题、77 道来自 LeanGeo-Bench 的非 IMO 竞赛题、22 道经典代数几何基准题 CertiGeo，以及 58 道精选自 OMNI-Geometry 的平面几何题），并额外引入了 PutnamBench 中的 31 道欧几里得几何题与 LEAP 团队建立的 Lean-IMO-Bench 中的全部 14 道几何题。

在 RQ1（自动形式化能力）的评估中，研究团队选用了覆盖闭源商用与开源生态的七大主流大语言模型，包括 GPT-5.6-Sol、Claude Opus 4.8、DeepSeek-V4-Pro、DeepSeek-V4-Flash、Qwen3.7-Max、MiniMax-M3 和 GLM-5.2。实验统一在 Lean 4.27.0 环境下进行。

结果表明，相较于直接将自然语言翻译为 Lean 代码，基于 GeoIR 与诊断修复的 GeoFormalizer 带来了极其显著的展开成功率跃升。这种优势在直接翻译能力相对偏弱的基模上体现得尤为夸张：在部分数据集上，基础直接翻译的成功率不足 30%，而经由 GeoFormalizer 流程后直接飙升至 80% 以上，展现出极强的模型泛化适应性与鲁棒性。

在 RQ2（自动化定理证明与反驳）的严格两小时单题算力沙盒测试中，GeoProver 与当前领域的顶尖基线展开了正面交锋。对比对象包括同样采用 DeepSeek-V4-Pro 后端的 Numina-Lean-Agent 与 Hilbert，以及经典的开源专用证明模型 Goedel-Prover-V2-8B。

在由 Claude Opus 4.8 生成的 200 道 MG200 命题及 31 道 PutnamBench 命题组成的 231 道综合测试集中，各系统的最终核验战果呈现出阶梯式的巨大差距：

Goedel-Prover-V2-8B：在严格的单题 pass@32 采样下，最终获证数量为 0 道。这印证了仅靠小参数模型在缺乏几何符号环境支持下，完全无法在庞大的 Mathlib 证明空间内完成长程逻辑闭环。
Hilbert：在相同的两小时预算与 DeepSeek-V4-Pro 驱动下，成功证明了 13 道题。
Numina-Lean-Agent：依托其通用智能体框架，成功完成了 44 道题的核验。
GeoProver（本文系统）：在 MG200 上斩获 67 道，在 PutnamBench 上拿下 6 道，总计攻破 73 道题，几乎达到了最强通用智能体基线（44道）的 1.6 倍以上。

为了剖析其超额收益的来源，研究团队进行了极具说服力的模块剥离实验（Ablation Study）。在保持基模型完全不变的前提下：

移除外部代数计算系统（CAS）的证书生成支持后，GeoProver 的证明数量从 73 道断崖式下挫至 29 道。这证实了外部符号代数求解器在化解深层代数恒等式方面的不可替代性。
进一步移除团队自研的 Lean 端代数化工具箱（即剥离 to_poly 体系，仅保留纯粹几何形态搜索），系统得分再次暴跌至 19 道。这一附加跌幅表明，即使不连接外部代数工具，将几何关系结构化展开为多项式约束的表征层本身，就能为 Lean 内部策略提供关键的高阶引导线索。

攻克 IMO 殿堂级题目与形式化纠错实战

最具学术含金量的结果出现在 RQ3——针对奥林匹克最高级别几何题的集中攻坚。在全部 43 道历史 IMO 几何题上，GeoProver 直接证明了由 GeoFormalizer 生成的 28 道题目（均在两小时内完成，另有 1 道在 2 小时 06 分钟完成）。所有这 29 道获证命题经过专家团队的二次逐行审计，确认全部属于 100% 忠实于原题题意的非退化无损形式化。

而针对剩下的 14 道未能直接证明的初始形式化命题，GeoProver 并非盲目耗尽时间，而是自主构建并提交了经由 Lean 内核检查验证的形式化反例。这些反例明确揭示了大模型在初次形式化时遗漏的隐式约束。

一个极具代表性的案例是 IMO 2007 第 2 题：

题目设定 $ABCD$ 为平行四边形，$BCED$ 为圆内接四边形。过 $A$ 引直线 $l$ 交线段 $DC$ 内部于 $F$，交直线 $BC$ 于 $G$。若 $EF=EG=EC$，求证 $l$ 是 $\angle DAB$ 的角平分线。

在大模型的初始形式化中，它精准翻译了所有连线和等长条件，却唯独将“$ABCD$ 是平行四边形”简单等价为了向量平移 $\vec{AB} = \vec{DC}$，漏掉了三点不共线的非退化要求。结果，GeoProver 迅速搜寻出一个退化反例：

取点坐标为 $D=(0,0)$，$A=(1/5,0)$，$F=G=(1/2,0)$，$B=C=(1,0)$，$E=(3/4,1)$。在这个构型中，所有的代数向量关系完全成立，但整个图形已经退化为一条基线上的线段重叠，此时 $\angle DAF = \pi$ 而 $\angle FAB = 0$，“角平分线”结论直接被物理击碎。

在收到该反例后，形式化专家仅需在命题中补入“$A, B, C$ 不共线”这一显式前提，GeoProver 随后便自动构建出了完整的 Lean 4 证明。正是借助这种“反例暴露缺陷 $\rightarrow$ 精确人工修复 $\rightarrow$ 自动证明攻坚”的敏捷闭环，团队最终拿下了全部 43 道历史 IMO 题目的机器证明。加上系统在无需人工干预下独立端到端完成的 IMO 2026 第 2 题（从自然语言生成 GeoIR、自动编译到输出纯核验通过的代码），MechGeo 创造了目前公开文献中规模最大、经过 Lean 4 严格内核核验的 IMO 几何题自动化证明集合。

同样的硬核实力在 LEAP 团队的 Lean-IMO-Bench 基准上得到了再次验证。该基准收录了 14 道极具挑战的几何命题，此前的通用求解器在此基准上一筹莫展。MechGeo 首次成功直接证明了其中的 12 道；对剩下的 2 道题目，系统同样形式化构造了反例——发现其原题库中的形式化代码遗漏了动点必须在“开线段内部”的顺序关系约束（例如 Basic 028 题中切点落在了三角形边延长线之外的异常分支）。在补正这些顺序约束后，GeoProver 将这两道修复后的命题也全部成功证明。

迈向真正可信的形式化数学智能

MechGeo 的探索为形式化数学研究提供了一个非常清晰的方法论信号：脱离了形式化语义验证的纯“定理证明”存在巨大的结构盲区，而脱离了几何宏观规划的“暴力代数求解”也注定走入死胡同。

长期以来，AI 数学社区在讨论“机器证明 IMO”时，往往默认人类专家已经给出了一套绝对精准的形式化代码，AI 的任务只是玩好单向的“代码补全游戏”。但真实科研和广泛竞赛中的非形式化表述充满了省略、隐喻和图形语义，自动形式化不可避免地会产生大量能够通过编译的“劣质代码”。MechGeo 证明了，真正的数学智能体不应只是单向的代码生成器，它必须具备像人类数学家一样的“挑错与证伪”意识——当一个命题无法被证明时，利用代数与几何反例进行主动反驳，往往是倒逼形式化走向严密的关键动力。

同时，在底层机制上，Mathlib 生态下的通用证明并不意味着要全盘照搬纯逻辑推理。通过在 Lean 内部精心构造严格等价的降维代数化接口，让前沿的高性能 CAS 充当高维多项式计算的“无信任算力插槽”，既守住了 ITP 小内核严格把关的安全底线，又打破了传统交互式定理证明器在非线性代数计算上的算力天花板。这种神经符号协同的混合架构，不仅照亮了欧几里得几何的形式化前路，也为未来大模型进军代数几何、拓扑与分析学等更庞杂数学疆域提供了兼具鲁棒性与严谨性的实现范式。