Euclean：在Lean中带统一验证的自动几何问题形式化

摘要

近期的形式推理系统已达到IMO级表现，却留下碎片化格局：代数与数论在Lean中处理，几何仍依赖形式保证有限的领域专用语言。这种割裂扩大可信计算基、阻碍统一模型开发。既有几何入Lean的努力（LeanEuclid、LeanGeo）引入与标准Mathlib不兼容的自定义公理系统，其小规模（<1,100题）限制大规模训练。而原生的Mathlib几何自动形式化面临独特挑战：隐式的图形假设（如拓扑构型与非退化性）必须被显式化而非推给外部求解器，且模型须适配Mathlib小巧而快速演化的几何基础设施。我们提出Euclean，一个四阶段框架——约束显式化、构型锚定、形式化映射与迭代修复——用于在原生Mathlib中自动形式化几何。我们构建OMNI-Geometry（768道竞赛题）与Numina-Geometry（177,597题），是Lean中最大的几何形式化数据集。人工评估显示48.89%的TOP1与73.33%的TOP5准确率。在我们的形式化上训练Goedel v2把证明成功率从13.6%提升到15.1%，验证了数据集对统一神经定理证明的质量。代码与数据集：https://github.com/tlb-22/Euclean。

Euclean：在Lean中带统一验证的自动几何问题形式化：论文配图 — 图 1：Euclean 形式化流程概述。左（输入中的歧义）：该过程从包含拓扑歧义的非正式自然语言语句开始，例如，“BCBC 上的点 PP”可能在拓扑上暗示线段、射线或直线。这些图说明，虽然左侧配置是预期的解决方案，但右侧配置（在扩展上）对于问题的逻辑无效。中（约束解释）：系统采用“证明优先”策略来解决这些歧义。生成的中间证明依赖于面积求和 (SABC=SABP+SACPS_{ABC}=S_{ABP}+S_{ACP})，这是一种逻辑依赖性，仅当 PP 严格位于 BCBC 段内时才成立。这种推理“锚定”了配置，迫使系统明确注入非简并和拓扑条件。右（形式化映射和修复）：检索这些明确的约束并将其映射到规范的 mathlib 原语（例如，将“三角形”映射到 AffineIndependent 约束）。最后，系统利用基于Lean编译器反馈的迭代修复循环来合成严格的、经过类型检查的定理语句。总的来说，这支持可靠的 mathlib 原生形式化。