开发者 schildep 在 GitHub 上放出一个用 Lean 4 写成的 3D 网格交集内核，卡点是审查方式：人类只需要读 93 行形式化规范、跑一遍 Lean 检查器，就能确认整个内核的正确性，不用去读超过 1000 行的 AI 实现代码，也不用检查 AI 自己写的 6 万多行证明。作者称这是他所知的第一个经过形式化验证的 3D 布尔运算（CSG）实现——这句话只是他自己检索后的判断，没有第三方确认，读者可以当背景信息看，别当行业公认的“首创”认领。
这件事真正的看点不是“AI 写的代码突然可信了”，而是审查的对象换了。以前审 AI 代码，人得盯着实现细节、跑测试、逐段看 diff；这次审查者只要盯住一份 93 行的规范文件，剩下的全部交给编译器去核对。这套方法能不能走出实验室，取决于规范本身写得够不够严、Lean 工具链够不够可信，以及性能能不能追上来——这三样目前都还是问题。
93行规范守住6万行AI证明
具体怎么审？项目把审查范围压缩到 4 个文件、93 行不含注释的代码：DataStructures.lean、Def.lean、MeshIntersectWithPreconditionCheck.lean、WellFormedCheckMsg.lean。规范只说一件事：给定两个满足“水密、无退化三角形、无自相交”等前置条件的输入网格，内核算出的输出网格必须严格等于两个输入实体的集合交集，输出本身也要满足同一套良构条件。
超过 1000 行的算法实现、超过 6 万行的 Lean 证明，人类都不用看。理由是 Lean 的检查器在编译期就会核对实现是否符合规范，符合就通过，不符合就编译不过——这是确定性检查，不是靠人工抽查或 AI 自我声明。
对照一下普通的“AI vibe coding”：开发者给出非形式化的需求描述、跑单元测试、人工抽查关键代码段，靠测试覆盖率给自己壮胆。这个项目换了一条路：规范用数学语言写死，检查器对所有可能输入验证符合性，不是抽样，是全集。
形式化验证换了审查对象，没换掉规范和工具链的风险
问题是，“零信任 LLM”不等于“零风险系统”。93 行规范本身对不对、全不全，仍然要靠人工判断——如果规范漏写了一条约束，再严密的证明也只是证明了一个错误的东西。Lean 编译器本身、以及最终生成可执行代码的整条工具链，也仍然是需要信任的基础设施，只是信任的对象从“AI 写的实现”换成了“更少的规范 + 更成熟的验证工具”。
- 结论.审查对象从代码转向规范，但对规范本身、检查器和工具链的信任并未消失，只是被压缩、被转移。
审查对象变了，不代表信任成本消失，只是转移了地方
另外一个容易被忽略的边界：形式化正确性只覆盖规范里写明的东西。网格三角剖分是否够优、UI 和胶水代码是否可靠，这份证明统统不管，项目文档也明确说这些还没有被形式化。
24秒处理两只兔子，原型离生产还有距离
演示网页里，两个各约 7 万个三角形的 Stanford Bunny 模型求交集，要跑 24 秒。这个速度放进实时 CAD、游戏引擎或工业仿真软件里基本没法用——主流网格布尔运算库处理这种规模的模型，通常在毫秒到亚秒级完成。
- 风险.项目本身也强调，这个速度差距不是形式化验证方法固有的代价，理论上验证过的代码也能做到和普通代码一样快，只是这次开发优先减少了人工审查负担，没有优先做性能优化。
对负责给 AI 代理生成高可信内核、又不想逐行审代码的工程团队来说，“审规范而不审实现”的思路值得记下来，尤其是在需要对外证明一个模块行为边界的场景里。但对负责评估 CAD 或生产级几何处理软件的技术决策者，这个内核目前更像一次方法论验证，还谈不上替换现有的成熟方案——24 秒的求交速度，以及未覆盖三角剖分质量和运行时复杂度的事实，都是短期内绕不开的现实条件。