首个形式化验证多边形相交算法实现

近日，一位开发者发布了名为“verified-polygon-intersection”的开源项目，据称这是首个经过形式化验证的多边形相交算法实现。该项目托管在GitHub上，并引起了Hacker News社区的广泛关注。项目核心亮点在于，它不仅提供了一个可靠的多边形相交检测函数，更通过Lean定理证明器完成了完整的数学验证，确保算法在所有输入情况下均能给出正确结果。

多边形相交是计算几何中的基础问题，广泛应用于图形学、地理信息系统、物理引擎和计算机辅助设计等领域。然而，传统实现往往依赖于大量的边界条件处理和浮点数近似，导致算法容易在极端情况（如退化多边形、共线边、自相交多边形）下出错。虽然单元测试和模糊测试可以覆盖常见场景，但无法穷举所有可能性。形式化验证则通过数学证明，为算法正确性提供了最高级别的保障。

该项目采用Lean 4作为验证工具。Lean是一种交互式定理证明器，被数学界和计算机科学界用于证明复杂定理和验证软件正确性。开发者表示，整个验证过程分为两部分：首先编写一个符合算法规范的函数，然后使用Lean证明该函数满足所有前置和后置条件。最终，任何调用该函数的代码都可以确信，只要输入合法，输出一定正确。

特别值得关注的是，开发者在项目README中详细描述了AI助手在开发过程中的作用。他指出，随着AI模型能力的快速迭代，使用AI辅助形式化验证的体验发生了质变。早期版本的模型（如Claude Opus 3）需要开发者手动提供证明策略，并分多个步骤引导模型完成证明。而最新的Claude Opus 4.8模型，仅需一次提示（one-shot）即可生成包含完整形式化证明的算法实现，无需人工介入证明细节。

这一进步意义深远。形式化验证传统上被认为是高门槛、低效率的技术，需要开发者同时精通算法和定理证明语言，导致其在实际工程中应用有限。AI的介入有望打破这一瓶颈：开发者只需用自然语言描述算法需求，AI即可自动生成Lean代码和证明脚本。这相当于将形式化验证从“专家手工活”降级为“工程师可用的工具”，可能加速安全关键系统（如自动驾驶、航空航天、医疗设备）中软件的验证流程。

当然，该项目也提醒用户，对算法正确性的信任完全来源于Lean检查器的验证结果，以及开发者对少量核心代码的人工审查。这意味着，只要Lean检查器本身可靠，且证明脚本正确，算法就不会出现逻辑错误。但浮点数精度、内存溢出等运行时问题仍需通过其他手段保证。

目前，该项目支持凸多边形和简单多边形的相交判定，未来计划扩展到任意多边形和三维空间。开发者已将代码开源，并欢迎社区贡献更多的测试用例和优化。对于希望学习形式化验证或计算几何的开发者而言，这是一个兼具学术价值和工程参考意义的案例。