正式验证的多边形交集 据我所知，这是第一个正式验证的多边形交集算法实现。（此外，可以与相关工作进行比较）与 AI 代理合作的经历随着最新模型的发布而发生了很大变化。最新模型能够一次性提供带有正式证明的算法实现，而之前的模型则需要我分多步提供证明策略。（AI 代理的能力）对正确性的信任完全来自 Lean 校验器和对小规格的人工审查，而非来自 LLM。（请参见 AI 代理的使用）尝试一下 尝试围绕验证核心构建的网络演示，您可以在其中绘制并交叉多边形。 背景 多边形交集是许多矢量图形编辑器的标准功能。多边形由多边形组件和多边形孔的列表定义，每个组件由顶点列表定义。它描述了一个二维区域：内部点的集合。这个集合可以通过计算从平面上每个点投射的射线与多边形相交的次数的奇偶性来正式定义。给定两个多边形，我们构造一个新的多边形，其内部集合是两个输入多边形的内部集合的交集。输入多边形有无穷多种配置，因此，如果没有正式验证，经典测试无法全面验证每种配置的属性。此外，对于每个多边形，内部点的集合是无限的，因此如果没有正式验证，内部集合及其交集只是一个无法在代码中表示的解释。在这一开发中，交集规范被正式描述并通过 Lean 4 证明助手完全验证。因此，我们可以保证这些无限的内部点集合实际上满足交集等式，对于任何输入多边形的配置都是如此。 计算几何算法如这一类的实现是著名的难以通过经典测试进行验证，因为输入的稀有特殊配置可能造成算法的大部分复杂性。例如，考虑以下例子，其中我们将一个十字形（下图中的蓝色多边形）与一个带孔的正方形（下图中的黄色多边形）进行交集。为了生成描述交集的多边形，算法必须选择封闭的边界组件并排列顶点。在这种情况下，选择哪些绿色线段属于同一个边界并不是唯一的（例如，它可以是四个正方形或一个带正方形孔的十字形），但如果黄色孔稍微大或小一些，它就会是唯一的。一个非平凡的事实（与欧拉回路有关）是，在所有情况下都可以将线段划分和排列成封闭的边界组件。该存储库中正式验证的长度大部分不来自算法，而是因为许多看似显而易见的几何事实并没有简短的严格证明。只有上面描述的关于“内部”的定义与射线的方向无关的证明需要数千行 Lean 代码。 AI 代理的使用 该存储库的设置旨在最小化验证多边形交集算法实现正确性所需的人为审查。人工审查者只需阅读 3 个文件 DataStructures.lean、Defs.lean 和 MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean，并运行 Lean 校验器。这些是 87 行简单易懂的 Lean 规范，主要设定多边形的基本几何定义。实现算法的未优化代码已经是以上两倍且更复杂。一旦我们添加优化，代码将大幅增长。另一方面，人工审查者必须阅读的规范将保持相同的大小。审查正确性不需要阅读其他文件。我还阅读并指导了其他不以 ...Proofs.lean 和 ...Impl.lean 结尾的文件内容，以引导策略（在 Opus 4.8 之前，请参见 AI 代理的能力）。这些其他文件中的主要定理作为检查点，因此我可以使用 Lean 检查器确定代理何时成功完成某项任务。...Proofs.lean 和 ...Impl.lean 文件中实现及其正确性的正式证明是 AI 代理自主编写的，从未由我或任何其他人类审查，但多亏了 Lean 检查器，我和任何人类审查者在这个过程中都不需要信任任何 LLM。这种分离的结构方式在 CLAUDE.md 中有所描述，并可能不符合 Lean 的习惯用法。我观察到的一个缺点是，强迫 AI 代理正式验证其实现往往会产生代码，这些代码速度较慢或忽略其他实际考虑，这些考虑并未在规范中体现。这可能源于正式验证的困难。