形式化验证的多边形交集算法——Opus 4.8 单次生成，此前模型均失败

据我所知，这是首次正式验证的多边形交叉算法实现。在该项目中与人工智能代理合作的经验，随着最新模型的发布而发生了巨大变化，我在 README 中对此进行了详细描述。Opus 4.8 能够一次性提供带有正式证明的算法实现，而此前的模型则要求我分多个步骤来提供证明策略。
对正确性的信任完全源自 Lean 检查器以及对一小段规范的人工审核，而非来自大语言模型。
此外，还请查看围绕 README 中所链接的已验证核心构建的网络演示。
该工具支持多重多边形，包括孔洞、自相交以及重叠边。