Show HN：形式化验证的多边形交集算法——Opus 4.8 一次搞定，此前失败
该项目首次实现了形式化验证的多边形交集算法，利用 Lean 4 证明助手确保无限点集交集等式的正确性。开发过程借助 AI 代理（Claude Opus 4.8）自动完成证明和实现，人类只需审查 87 行规格说明。文章介绍了算法背景、验证挑战以及 AI 代理能力的演进。
文章情报
要点
- 首个经过形式化验证的多边形交集算法实现，使用 Lean 4 证明助手。
- AI 代理（Claude Opus 4.8）能够自主编写证明和代码，人类仅需审查简短规格。
- 形式化验证确保了即使面对无限配置的输入，算法也保证正确。
- Opus 4.8 相比早期版本能处理更大规模的证明策略，并自动规避错误中间定理。
为什么重要
这条新闻值得关注，因为首个经过形式化验证的多边形交集算法实现，使用 Lean 4 证明助手。
技术影响
可能影响模型选型、推理成本、产品能力和评测基准。
在计算几何领域，多边形交集是一个基础但复杂的问题。近日，开发者 schildep 在 GitHub 上发布了“verified-polygon-intersection”项目，宣称实现了首个经过形式化验证的多边形交集算法。该项目利用 Lean 4 证明助手，从数学上严格证明了算法对于任意多边形配置的正确性。
传统的软件测试无法穷举所有输入情况，尤其是多边形顶点可能存在无数种特殊排列。形式化验证则通过严谨的逻辑推理，保证算法满足规格说明，从而彻底消除不确定性。在本项目中，人类审查者只需阅读 87 行的规格文件（定义基本几何概念和交集属性），其余数千行代码和证明均由 AI 代理自动生成。
文章详细介绍了多边形交集的数学基础：将多边形视为由顶点定义的内部点集，交集即为两个点集的公共部分。这一看似直观的概念，在形式化证明中却需要处理大量隐含的几何事实。例如，证明定义的内部集与射线方向无关就耗费了上千行 Lean 代码。
AI 代理的能力演进是本文的另一亮点。开发者最初在年初尝试使用 Claude Opus 4.5 和 4.6，但发现它们需要用户提供详尽的证明策略。Opus 4.7 有所改善，能自动完成一些步骤，但仍需人工提示。直到 Opus 4.8，模型能够在无人干预下，从零开始证明核心定理并生成完整的算法代码。值得注意的是，Opus 4.8 在遇到可能的错误中间定理时，会自主转向替代策略，甚至并行运行多个子代理试探不同方案。
尽管 AI 代理完成了大部分工作，但开发者强调信任完全来源于 Lean 检查器，而不是大语言模型。同时，他们也指出当前代码为了通过验证而牺牲了部分性能，后续计划优化算法、简化证明，并添加 SVG 导入/导出等功能。
该项目不仅展示了形式化验证在计算几何中的应用潜力，也反映了 AI 在定理证明领域的快速进步。对于关注软件可靠性或 AI 能力的读者来说，这无疑是一个值得关注的开源项目。