多边形相交是计算几何中的基础操作，广泛应用于矢量图形编辑、地理信息系统、计算机辅助设计等领域。然而，这一看似简单的几何操作却隐藏着巨大的验证难题：输入多边形的配置空间是无限的，传统单元测试无法穷尽所有边界情况；每个多边形的内部点集也是无限的，代码中的集合运算本质上只是对数学概念的近似表达。这种 "无限性" 使得形式化验证成为确保算法正确性的唯一可靠途径。
近期，开发者 schildep 完成了首个经过形式化验证的多边形相交算法实现，该项目使用 Lean 4 证明助手构建完整的数学保证体系。"To my knowledge, this is the first formally verified implementation of an intersection algorithm for polygons." 这一成果的意义不仅在于算法本身的正确性，更在于展示了 AI 辅助形式化验证的新范式。
证明工程的演进：从人机协作到自主证明
形式化验证的核心挑战在于将数学直觉转化为机器可检查的证明步骤。在早期的尝试中，即使使用 Claude Opus 4.5 和 4.6，开发者仍需将证明拆分为大量细粒度步骤，并手动提供每个中间引理的策略提示。例如，仅证明 "射线方向无关性"（即多边形内部点定义不依赖于射线方向）就需要数千行 Lean 代码和密集的人工干预。
Opus 4.7 带来了显著的能力提升，能够处理更大粒度的证明步骤。开发者可以仅提供高层思路（如使用欧拉回路处理边界组件选择问题），模型便能自主填充细节。然而，面对重叠边等特殊情形时，仍需要人类提供针对性的处理提示。
真正的范式转变发生在 Opus 4.8。在 ultracode 模式下，该模型展现出前所未有的自主证明能力：开发者启动两个并行会话，一个要求从零开始重建整个证明体系而不提供任何提示，另一个要求扩展算法以处理先前失败的特殊情形。令人惊讶的是，两个会话均在数小时内自主完成。关键突破在于 Opus 4.8 能够准确评估中间引理的风险：当某个辅助定理证明受阻时，模型会主动怀疑其正确性，自主转向替代策略，或并行启动子代理尝试多种路径。这种 "元认知" 能力大幅降低了人类在证明策略层面的参与成本。
可信代码生成的人机边界
该项目的架构设计体现了对 "信任来源" 的清晰划分。人类审查者只需阅读三个规范文件（DataStructures.lean、Defs.lean、MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean），总计 87 行简洁的 Lean 代码，即可理解算法的数学规格。这些规范定义了多边形的数据结构、内部点集的数学定义，以及算法应满足的正确性条件。
其余所有实现代码（...Impl.lean）和证明代码（...Proofs.lean）均由 AI 代理自主生成，且从未经过人类逐行审查。可信性完全来自 Lean 检查器的机械验证：只要规范正确且检查器通过，实现代码必然满足规格要求。这种分离使得审查负担与代码复杂度脱钩 —— 即使算法实现扩展优化，人类审查的规范文件保持不变。
验证完成后，可通过以下命令检查定理依赖的公理基础：
#print axioms multipolygonIntersectionAlgorithmWithPreconditionCheck_interior_eq
#print axioms multipolygonIntersectionAlgorithmWithPreconditionCheck_complete
该项目仅依赖 [propext, Classical.choice, Quot.sound] 三个可信公理，确保了证明基础的最小化。
工程落地的权衡与参数
形式化验证并非没有代价。实践中观察到一个显著倾向：经过形式化验证的代码往往比手写版本更慢，且可能忽略实际工程中的性能考量。这源于两方面原因：一是证明难度推动实现向更简单、更易验证的方向演化；二是训练数据中缺乏经过形式化验证的实用软件，模型缺乏优化验证代码的经验。
对于希望采用类似路径的团队，以下参数可作为参考基准：
- 规范代码量：约 80-100 行 Lean 代码定义核心数据结构和不变量
- 实现 / 规范比：未优化实现已达规范代码的 2 倍以上，优化后差距将进一步扩大
- 模型版本门槛：Opus 4.7 可处理高层策略提示，Opus 4.8 可实现完全自主证明
- 验证工具链：Lean 4（v4.15.0）、elan 管理器、可选 WebAssembly 构建用于 Web 演示
- 审查焦点：数据结构的数学定义、前置条件检查、正确性定理的陈述
结语
多边形相交算法的形式化验证项目展示了 AI 辅助可信软件开发的成熟路径。Opus 4.8 的能力跃迁标志着形式化验证正从专业研究者的领域工具，转变为普通开发者可借助的工程质量保障手段。当 AI 能够自主处理证明策略的复杂性，人类得以将精力集中于规格设计的正确性 —— 这正是形式化方法的本质价值所在。
资料来源
- GitHub: schildep/verified-polygon-intersection
- GitHub: schildep/challenge-verified-polygon-intersection-Opus-4.8
内容声明：本文无广告投放、无付费植入。
如有事实性问题，欢迎发送勘误至 i@hotdrydog.com。