24小时热榜

<a href="https://xcancel.com/eastdakota/status/2062860530360959273" rel="nofollow">https://xcancel.com/eastdakota/status/2062860530360959273</a>

据我所知，这是第一个经过正式验证的多边形交集算法实现。<p>在这个项目中与人工智能代理合作的经验随着最近模型的发布发生了很大变化，正如我在自述文件中所描述的那样。Opus 4.8能够一次性提供带有正式证明的算法实现，而之前的模型则需要我分步骤提供证明策略。<p>对正确性的信任完全来自于Lean检查器和对小规格的人工审查，而不是来自大型语言模型（LLM）。<p>还可以查看自述文件中链接的围绕经过验证的核心构建的网络演示：<a href="https:&#x2F;&#x2F;schildep.github.io&#x2F;verified-polygon-intersection&#x2F;" rel="nofollow">https:&#x2F;&#x2F;schildep.github.io&#x2F;verified-polygon-intersection&#x2F;</a>。它支持包括孔洞、自交和重叠边的多边形。