据我所知，这是第一个正式验证的 3D 构造固体几何 (CSG) 操作的实现：网格相交，采用 Lean 4 实现，并根据简洁的规范进行验证，以准确确定生成网格的表面，并保证三角剖分的实用良构性条件。（另见相关工作。）该项目还实验避免信任 AI 生成的代码。人类审查员只需阅读 93 行正式规范，并按照以下描述运行 Lean 检查器以认证核心的正确性，从而跳过复杂的 1000 多行 AI 编写的实现。为了证明正确性，AI 独立编写了超过 60,000 行的 Lean 证明，这些证明也不需要人类进行检查。Lean 检查器保证在编译时符合规范，对任何大型语言模型 (LLM) 不存在信任。这使我们可以将实现和证明视为黑箱。我引导代理通过下面描述的里程碑，以得出这里展示的结果。网页演示 尝试使用围绕经验证的核心构建的网页演示，您可以相交示例网格或从 STL 文件导入和相交网格。编译后的 Lean 代码在您的浏览器中本地运行；数据从未发送到服务器。请注意，尽管核心是正式验证的，但 UI 和连接代码并不是。我们的实现速度远低于最先进的网格相交实现：计算两个 70k 三角形斯坦福兔子的确切相交需要 24 秒。在这个项目中，我们优先考虑最小化对正确性的人工审查工作，而非性能。请注意，这种性能差距并不是正式验证软件的基本限制，原则上它可以和传统软件一样快。详情请见。输出网格被保证满足下面描述的属性，但在我们尚未正式化的其他标准方面，网格可能并不理想；例如，它可能生成一个比必要的更细的网格。背景和形式化 一个三角网格是一组三角形，通常期望形成一个不穿透自身的封闭表面，以及我们之后要讨论的其他良构性条件。人类直觉上将三角网格与“固体”关联，即 3D 空间中的一个体积：所有不在表面上的点，但“在”网格内的点。（“内部”可以通过带符号的光线相交计数进行数学描述。）这种固体的概念使我们能够理解像网格相交算法这样的算法输出应该是什么样的，即使处理实际网格数据结构的实现复杂，并且必须用专用代码处理许多几何特例。对于网格相交算法，我们期望良构输入网格的固体的集合相交是输出网格的固体，并且输出再次是良构的网格。（我们也期望该算法能够正确检测和报告输入是否是良构的。） solid（meshIntersect M₁ M₂）= solid M₁ ∩ solid M₂ 这准确地将生成网格的表面锁定为相交固体的边界。处理三角网格的算法可以有效地计算出我们心目中的固体的网格，但传统编程语言无法明确表示“固体”或做出关于它们的声明，因为这些是无限集。在 Lean 中，这是可能的，我们可以例如对这些无限集进行相交或证明两个无限集相等。此外，Lean 允许我们证明一个函数对于所有可能的输入网格都满足某个条件，而传统编程语言仅允许我们测试函数对特定输入是否满足某个条件。我们定义网格的良构性，以捕捉实际网格处理工具通常期望的条件 - 密封表面，包围一个数量为一的固体，具有一致的外指向性，没有退化的三角形，没有自相交 - 但有一个放宽：表面可以接触自身，不在面内部，而是在边缘和顶点上。因此，不需要严格的 2-流形条件。参见为什么总是生成流形网格的相交算法是不可能的。最小化对 AI 的信任的人工审核 为了认证核心的正确性，该核心检查输入的良构性前提并计算网格相交，审查员只需阅读 93 行正式规范，并按照下面的描述运行 Lean 检查器。审查员可以跳过复杂的 1000 多行 AI 编写的实现。Lean 检查器保证在编译时符合规范，对任何 LLM 不做信任假设。只需阅读 CSG/DataStructures.lean、CSG/Def.lean、CSG/MeshIntersectWithPreconditionCheck.lean 和 CSG/WellFormedCheckMsg.lean 中的文件。