该项目首次实现了3D网格相交的正式验证，使用Lean 4编写，核心规范仅93行，而AI编写的实现代码超1000行。人类只需审查规范并运行验证器，即可确保正确性，无需信任AI生成的代码。

据我所知，这是首个经过形式化验证的3D构造实体几何（CSG）操作实现：网格交集算法。该实现采用Lean 4编写，并依据一份简洁的规范进行了验证。这份规范精确地定义了结果网格的表面，并保证了三角剖分在实践中的良好形态条件。

该项目也是一次避免信任AI生成代码的实验。人工审核者只需阅读93行形式化规范，并运行Lean检查器，即可验证核心算法的正确性，而无需审阅超过1000行由AI编写的复杂实现代码。为了证明正确性，AI自主编写了超过6万行的Lean证明，这些证明同样无需人工检查。Lean检查器在编译时确保代码符合规范，无需信任任何大语言模型。这使得我们可以将实现和证明视为一个黑盒。我通过下文所述的里程碑节点引导AI代理，最终得到了当前的结果。

网络演示

您可以尝试基于已验证核心构建的网络演示，在其中对示例网格进行交集运算，或从STL文件导入网格进行交集运算。编译后的Lean代码在您的浏览器本地运行，不会向服务器发送任何数据。请注意，虽然核心算法经过了形式化验证，但用户界面和胶水代码并未验证。

我们的实现速度远慢于最先进的网格交集算法：计算两个各含7万个三角形的斯坦福兔子的精确交集需要24秒。在本项目中，我们优先考虑最小化人工审核正确性的工作量，而非性能。需要注意的是，这种性能差距并非形式化验证软件的根本限制，理论上它可以和传统软件一样快。

背景与形式化

三角形网格是一组三角形的集合，通常期望形成一个封闭且不自交的表面，此外还需满足其他一些良好形态条件。

人们直观地将三角形网格与“实体”联系起来，即三维空间中所有不在表面上但位于网格“内部”的点的集合。（“内部”可以通过有符号射线相交计数来数学描述。）

这种实体的概念使我们能够理解网格交集算法等输出的预期形态，即使处理实际网格数据结构的实现非常复杂，并且需要用专门的代码处理许多几何特例。

对于网格交集算法，我们期望：形态良好的输入网格的实体集合的交集，等于输出网格的实体，并且输出网格本身也是形态良好的。（我们还期望，如果输入网格形态不佳，算法能够正确检测并报告。）

solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂

这精确地确定了结果网格的表面，即相交实体的边界。

在三角形网格上工作的算法可以高效地计算出我们心目中的实体网格，但传统编程语言无法显式表达“实体”或对其进行断言，因为它们是无限集合。在Lean中，这是可能的，例如我们可以对这些无限集合进行交集运算，或证明两个无限集合相等。此外，Lean允许我们证明一个函数对所有可能的输入网格都满足某个条件，而传统编程语言只允许我们针对特定输入测试该函数是否满足条件。

我们定义的网格良好形态条件涵盖了现实世界网格处理工具通常期望的条件——水密表面、以多重性1包围实体且具有一致的外向法向、无退化三角形、无自交——但有一个放宽：表面可以自接触，但不能在面的内部，而可以在边和顶点处接触。因此，不要求严格的2-流形性。

最小化人工审核，无需信任AI

为了验证核心算法的正确性（该算法检查输入的良好形态前置条件并计算网格交集），审核者只需阅读93行形式化规范，并按下文所述运行Lean检查器。审核者可以跳过算法中超过1000行由AI编写的复杂实现代码。Lean检查器在编译时确保代码符合规范，无需信任任何大语言模型。

• 只需阅读文件CSG/DataStructures.lean、CSG/Def.lean、CSG/MeshIntersectWithPreconditionCheck.lean和CSG/WellFormedCheckMsg.lean，并按下文所述运行Lean检查器。这些文件（不含注释）仅93行代码。其他文件无需阅读，因为指定meshIntersectWithPreconditionCheck的定理陈述仅依赖于这4个文件中定义的声明。
• 审核者可以跳过CSG/Impl/目录下4个文件中超过1000行的meshIntersectWithPreconditionCheck实现，因为确定性的Lean检查器保证其符合人工审核过的规范。
• 这得益于CSG/Proof/目录下6万行由AI编写的形式化证明，这些证明同样无需人工检查。

这种从实现到规范的压缩和简化之所以可能，是因为实现必须处理的许多问题可以与规范完全解耦：

• 实现必须处理特殊的几何情况，这构成了算法的大部分复杂性；而形式化规范之所以简短，是因为数学可以一般性地表述。Lean检查器保证所有特殊情况都按照规范处理，而无需在规范中列举这些特殊情况。
• 实现使用加速数据结构来避免二次方的时间复杂度和其他优化。虽然我们没有形式化运行时复杂度，但Lean检查器保证，在所有这些优化下，我们仍然能产生符合规范的结果。

如果未来的提交中我们进一步提高了运行时性能或输出网格的质量，已审核的规范保持不变，我们就能保证正确性，无需重新审核。另请参阅我如何仅通过塑造这个规范来开发这个项目。

开发过程

在开发过程中，我只控制一个小的规范，将证明和详细实现作为黑盒交给AI代理。我从一个我认为相对容易实现和形式化证明的规范开始，然后逐步增加需求。在下面列出的每个步骤中，我都让AI代理实现并形式化证明该规范。这种逐步精化的方式使我能够将大量工作委托给AI代理，同时获得关于我的规范是否可满足的反馈，并在每个里程碑验证AI代理朝着最终目标的进展。我指示AI代理在形式化之前先编写非形式化的证明。

• 我首先让一个AI代理形式化了一篇论文，该论文提供了一个基于单纯链描述实体的数学框架。这给了我一个形式化的存在性结果，但没有具体的实现。
• 然后，我要求提供一个带有正确性证明的实现。这已经满足了一个类似于我最终目标的规范。但重叠三角形和其他问题仍然被允许，并且确实出现了。
• 接着，我为输出网格指定了限制条件（类似于当前WellFormedMesh的状态），以禁止第一次实现中出现的那种问题。我还引入了对输入的一般位置限制（后来移除了），以避免实现在此步骤中考虑大量特殊情况。更严格的要求迫使进行完全重写，但部分形式化框架可以重用。
• 然后，我移除了对输入的一般位置限制，这迫使AI代理正确处理所有特殊的几何情况。
• 接着，我让AI代理使用包围体层次结构和其他优化来优化实现。我没有形式化运行时要求，但Lean验证了优化仍然满足相同的规范。因此，在这一步中，我无需重新审核任何内容来确保正确性。
• 最后，我进一步加强了规范，并使其更易于审核。

这个过程产生了您可以在CSG/文件夹顶层看到的规范，以及CSG/Proof/中的证明和CSG/Impl/中的实现。

对于上述大部分步骤，我使用了Claude Opus 4.8。对于某些步骤，我使用了Fable 5来创建初始的非形式化证明策略，然后让Opus编写形式化证明和实现。上述某些步骤需要AI代理自主工作超过24小时。

与非形式化规范的“氛围编码”对比

与常规的“氛围编码”不同，将AI与形式化验证相结合，能产生严格的保证，我们知道这些保证对所有输入都成立，并且在程序的每次后续修改中都能得到强制执行。但就像常规的“氛围编码”一样，每一步的开发都可能积累一些技术债务：我最终得到的实现和证明远非整洁，也不遵循一个连贯的设计，就像由人类掌控全局时那样。此外，这里还有一些我们没有形式化的约束，例如运行时性能或输出实体面的三角剖分方式（除了良好形态条件之外）。因此，这些约束与常规的“氛围编码”一样难以控制。

作为对比，我给了Opus 4.8一个非形式化的规范描述，并要求它在C++中实现。实现（不包括测试、胶水代码等）的长度与Lean实现相当，也在1000多行。尽管它编写了单元测试并迭代修复了自己的实现，但经过一个独立AI代理将其与形式化验证的Lean实现进行比较审查后，在C++几何核心中发现了3个不同的错误，并在特定输入上复现。所有这些错误都很罕见，几乎不可能通过黑盒测试发现。由其他AI代理根据非形式化规范对代码进行迭代对抗性审查可能会发现这些错误。但如果没有形式化验证，就不可能确切知道实现中是否还有更多错误。

将形式化验证与“氛围编码”相结合的缺点：

• 它往往会产生较慢的代码，或忽视规范中未捕获的其他实际考虑。这源于形式化验证的难度促使代码更简单，以及训练数据中缺乏经过形式化验证的实用软件。
• AI代理自主开发形式化证明所需的时间和token数量，可能比非形式化地推理其实现要多出几个数量级。
• 许多实际问题没有一个简单的形式化规范。

在我撰写本文时，AI代理处理大型明确定义任务的能力正随着每个模型版本的发布而迅速提高。人类审查其输出并对其进行推理的能力却没有。我希望我们可以利用形式化验证等方法作为杠杆来保持控制。

构建与检查

需要elan。Lean版本在lean-toolchain文件中固定（当前为leanprover/lean4:v4.15.0），以简化WebAssembly构建；elan会在首次使用时自动安装。

首先从社区缓存下载预构建的Mathlib（否则下一步将从源码编译Mathlib，这需要很长时间）：

lake exe cache get

如果此操作因SG_READ_ONLY相关的dyld错误而中止（macOS最新版本）：此处固定的Lean版本捆绑了一个存在已知问题的链接器，该问题已在后续Lean版本中修复。使用Apple的编译器重新链接缓存工具即可：

rm -rf .lake/packages/mathlib/.lake/build/bin SDKROOT="$(xcrun --show-sdk-path)" LIBRARY_PATH="$(lean --print-prefix)/lib" LEAN_CC="$(xcrun -f clang)" lake exe cache get

检查所有证明：

lake build

检查感兴趣的定理所依赖的公理（以下示例中，是演示中调用的网格交集实现的正确性定理）。这一点很重要，因为AI代理可能在证明中引入了不需要的公理。此仓库中的所有定理仅依赖于可信的公理[propext, Classical.choice, Quot.sound]：

printf 'import CSG.MeshIntersectWithPreconditionCheck\n#print axioms CSG.meshIntersectWithPreconditionCheck_ok_spec\n#print axioms CSG.meshIntersectWithPreconditionCheck_ok_of_wellFormed\n#print axioms CSG.meshIntersectWithPreconditionCheck_error_sound\n#print axioms CSG.meshIntersectWithPreconditionCheck_error_of_not_wellFormed\n' | lake env lean --stdin

还要确保定理实际上适用于编译后的函数，即实现没有被通过以下关键字之一覆盖。此搜索应返回无匹配结果：

rg -n 'implemented_by|extern|csimp|skipKernelTC|unsafe|partial|opaque' CSG/

构建Web应用程序使用的WebAssembly包（需要emscripten、zstd和node/npm；wasm-opt是可选的）：

./build_web_demo.sh

性能

该算法拒绝了原始的斯坦福兔子，因为网格不是水密的，所以我封闭了底部的孔。该实现在M4 Pro上单线程计算两个7万三角形网格的精确交集需要24秒。

这个实现远慢于最先进的网格交集算法。在本项目中，我们优先考虑最小化人工审核正确性的工作量，而非性能。

• 大多数其他实现使用硬件加速的浮点计算。（即使是像CGAL这样的精确实现，在浮点精度足够的情况下也会使用浮点数进行决策。）我们没有这样做。这不是Lean的根本限制，但使用硬件加速的浮点数需要额外的人工审核者必须信任的公理。
• 我们在运行时根据良好形态定义检查所有输入，这占了总运行时间的很大一部分。

为什么我们通常无法得到流形输出网格

在以下示例中，带孔立方体的精确旋转导致了一个表面非流形的实体。（请参见输出中实体两个组件接触的前方点。）将两个网格的移动网格大小设置为1/3，旋转位数设置为1，即可在网络演示中安排这种情况。如果您重置旋转并移动带孔立方体，还可以安排输出实体表面沿一条边非流形的情况。

如果我们强加流形条件，那么没有任何算法能够满足我们的规范。

特殊情况

规范很简短，但算法必须用专门的代码处理特殊的几何情况，以满足规范。

这里两个四面体的右侧面共面重叠，且法向方向相同。规范隐含地迫使算法在共面面的交集中发射一个面。不遵循形式化规范的程序可能会忽略这种情况，并在表面上产生一个孔或一个双层面。

在这个例子中，四面体精确接触，它们之间没有体积——这是法向方向相反的面的共面重叠。我们的规范迫使输出为空。许多生产应用程序在这种情况下会随机产生双膜伪影。在上面的带孔立方体示例中，您会看到一个非平凡的例子，其中包含法向方向相反的共面重叠。

算法还必须处理许多其他特殊情况。得益于形式化验证，我们无需为任何情况编写任何单元测试来确保正确性。

• 一个网格的顶点位于另一个网格上。算法必须确保考虑这些顶点，以便在切割的两侧创建面。
• 一个或两个输入网格不满足4个良好形态条件之一，并且必须正确报告。
• 我们上面讨论的共面重叠本身也有子特殊情况，例如重叠面的边共线。
• ...

还有一些实现必须正确处理的特例，这些特例从输入中不可见，而是来自算法内部几何构造的结果。如果不阅读实现，我们永远不会想到去测试这些。我们的规范确保所有这些都得到正确处理，而无需我们考虑。

• 在实现中为了确定内部/外部而发射的射线，恰好击中三角形的边或顶点，甚至共面地穿过一个面。
• 一个面恰好位于包围体层次结构加速结构中包围盒的边界上，这要求我们在实现中设置正确的不等式。
• 上述几点不仅适用于交集运算，也适用于良好形态检查。在代码的那部分出错可能会导致网格被错误地分类为非良好形态。
• 算法的子例程可能会创建T型连接，它必须再次修复以产生一个形态良好的输出网格。
• ...

相关工作

• Di Vito和Hocking（NASA形式化方法2021）在PVS中验证了一个多边形合并算法，将两个重叠的简单多边形合并成一个没有孔洞的单一外边界。
• 我早期的verified-polygon-intersection项目在Lean 4中验证了2D多多边形交集，像这里一样依赖于AI编写的实现和证明。
• 当然存在未经验证的精确3D网格布尔运算，例如CGAL的Nef多面体。在实践中精确且健壮，但其正确性依赖于测试和非形式化推理，而非机器检查的证明。

根据评论内容，总结主要观点及论据如下：

1. 形式化验证的局限性与信任问题 - 评论1指出，形式化验证仅针对核心内核（kernel），而UI和胶水代码（glue code）未验证，曾因浮点数转换溢出导致网格漏洞（"I once hit a bug... an overflow in the glue code"）。 - 评论4质疑LLM生成内核的可信度，认为证明内核必须足够小且可人工验证，否则系统不可靠（"How does one trust an LLM generated kernel is proving the right things?"）。 - 评论7进一步追问：如何确保LLM或人类实现的代码与证明描述精确对应？（"How do we know that the implementation maps precisely to the description within the proof?"）

2. 性能与实用性争议 - 评论5强调，实际应用中需使用硬件加速浮点数，而形式化验证算法通常性能不足（"most of these algorithms are not sufficiently performant to be practically useful"）。 - 评论2对比了Manifold库，询问性能与零损坏方面的表现（"How does it compare against... in performance and zero corruption?"）。

3. 技术实现与扩展性 - 评论3赞赏CSG工作流在3D环境构建中的直观性，但指出商业引擎支持糟糕（"The current story with CSG around commercial game engines is pretty awful"）。 - 评论9关注数值稳定性问题，认为这是网格CSG操作的主要敌人（"the one true enemy of mesh-based CSG operations"）。 - 评论10建议扩展至并集、差集等操作，并询问是否考虑模糊测试（"Why not extend to union, difference, and xor?"）。

4. 学习门槛与集成潜力 - 评论8坦言理解证明比代码更难，希望获得学习资源（"I'd have an easier time understanding 1000s of lines of slop than 93 lines of proofs"）。 - 评论6询问项目能否集成到FreeCAD等开源工具中（"Do you see it possible that this project can be integrated into... FreeCAD?"）。

5. 浮点数兼容性 - 评论11提出关键问题：若扩展到浮点数，能否处理共面问题？（"Would you still be able to deal with coplanar faces if you were to expand this to floats?"）

总结：评论者普遍认可形式化验证的创新性，但对其实际应用中的性能、浮点数兼容性、代码与证明的一致性验证存在疑虑。同时，CSG工作流的实用价值被肯定，但商业引擎支持不足和数值稳定性仍是痛点。