24小时热榜

据我所知，这是首个经过正式验证的三维构造实体几何（CSG）操作实现：网格交集，使用Lean 4实现，并根据简明的规范进行了验证，该规范准确地确定了生成网格的表面，并保证了三角剖分的实际良构性条件。 该项目也是一个避免依赖AI生成代码的实验。人类审阅者只需阅读93行正式规范，并运行Lean检查器来认证内核的正确性，从而跳过复杂的1000多行AI编写的实现代码。为了证明正确性，AI自主编写了超过60,000行的Lean证明，这些证明也无需人类检查。Lean检查器在编译时保证符合规范，对任何大型语言模型（LLM）没有任何信任。这使我们能够将实现和证明视为一个黑箱。我引导代理通过readme中描述的里程碑，达成了这里展示的结果。 同时，请查看网页演示 <a href="https:&#x2F;&#x2F;schildep.github.io&#x2F;verified-3d-mesh-intersection&#x2F;" rel="nofollow">https:&#x2F;&#x2F;schildep.github.io&#x2F;verified-3d-mesh-intersection&#x2F;</a>，该演示在您的浏览器中运行经过验证的网格交集内核，已编译为WebAssembly。