通过 Lean 4 和 AI Agent 实现的形式化验证多边形交集算法"}],

形式化验证多边形交集概述

verified-polygon-intersection 项目是已知首个针对多边形（multipolygons）交集算法的形式化验证实现。通过使用 Lean 4 证明助手，该项目确保了两个多边形（定义为内部点集）的交集在任何可能的输入配置下在数学上都是正确的，从而消除了计算几何中与传统测试相关的风险。

计算几何验证的挑战

由于输入配置的无限多样性和罕见边缘情况的存在，计算几何算法通过传统测试进行验证是非常困难的。 \n### 无限输入集由于多边形的内部是一个无限点的集合，传统测试无法穷尽地验证两个此类集合的交集是否在代码中得到了正确表示。形式化验证允许将内部集合视为数学实体，而非仅仅是解释。

复杂的边缘情况

特殊的配置，例如将一个十字形与一个带有孔洞的正方形相交，会产生非平凡的挑战。在这些情况下，算法必须将线段划分为闭合边界组件并进行排序。项目指出，这一过程与欧拉回路（Eulerian cycles）有关，这是一个必须经过证明的非平凡事实，以确保算法在所有情况下都能正常工作。

利用 Lean 4 实现无须信任的正确性

对算法正确性的信任源于 Lean 检查器和对极简规范的专家评审，而非对生成代码的 AI 的信任。

极简人工评审

为了减轻人工评审人员的负担，项目将规范（specification）与实现分离。评审人员只需检查三个文件——DataStructures.lean、Defs.lean 和 MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean——这些文件构成了大约 87 行简单的 Lean 规范。实际的实现和证明过程要庞大且复杂得多，但它们由 Lean 检查器自动验证。

公理验证

为了确保 AI Agent 没有在证明中引入不必要的或不健全的公理，项目允许用户检查定理所依赖的公理。当前的实现仅依赖于受信任的公理：propext、Classical.choice 和 Quot.sound。

AI Agent 在形式化证明中的能力演进

该项目的开发突显了 LLM 在处理形式化验证任务方面的重大飞跃，具体表现为从翻译人类草图到自主制定策略的转变。

模型演进

Claude Opus 4.5/4.6: 这些模型可以处理非平凡的 Lean 证明，但需要人类开发者提供极其严谨的证明草图。例如，证明内部集合定义独立于射线方向需要将证明拆分为许多由人类引导的小步骤。
Claude Opus 4.7: 该模型可以采取更大的步幅，并证明任何两个多边形之间存在交集的结论，尽管它在处理欧拉回路和特定的棘手边缘情况时仍需要人类提示。
Claude Opus 4.8 (Ultracode mode): 该模型展示了自主制定并执行大规模证明策略的能力。它能够在没有任何提示的情况下，从头开始重新证明主要的多边形交集定理，并扩展了算法以处理重叠线段——这是 Opus 4.7 曾失败的任务。

AI 行为转变

对 Opus 4.8 中间输出的观察表明，它能更有效地处理错误中间定理带来的风险。该模型现在不再仅仅卡在错误的定理上，而是会对自己的路径产生怀疑，并自主转向不同的策略，或者部署并行子 Agent 来测试多种方法。

实现的权衡与未来工作

虽然形式化验证确保了正确性，但它也引入了一些实际的弊端。作者指出，强制 AI Agent 形式化验证其实现往往会导致代码运行速度较慢，或者忽略了数学规范中未涵盖的实际优化。这归因于验证的难度迫使 AI 向更简单、更易于证明的代码方向靠拢。

未来路线图

性能优化: 测量并改进实现的执行速度。
证明简化: 使用最新的 AI 模型来消除当前证明中的不必要的弯路。
功能扩展: 添加 SVG 导入和导出功能。