计算几何

首个经形式化验证的多边形相交算法由AI代理一次性实现

本文介绍了首个经过形式化验证的多边形相交算法实现，使用Lean 4证明助手确保算法在任何输入配置下的正确性。项目利用AI代理，最新模型能够一次性提供带有形式证明的算法实现，而旧模型需要多次步骤。