AI 写代码、Llvm 验证：首个形式化证明正确的 3D CSG 网格求交实现
开发者用 Lean 4 形式化验证 3D CSG 网格求交内核，AI 自动生成 60,000 行证明，人工仅需审阅 93…
一位开发者在 Hacker News 上展示了据称是首个形式化验证的 3D 构造实体几何（CSG）网格求交实现：基于 Lean 4 定理证明器编写，核心内核仅需人工审阅一份 93 行的形式化规范即可认定其正确性，无需逐行阅读 AI 生成的上千行实现代码。该项目同时是一次「不信任 AI 也能用 AI」的实验——AI 自主撰写了超过 60,000 行 Lean 证明，但这些证明同样无需人工逐一检查，由 Lean 检查器在编译期保证实现与规范一致。
实现结构与验证范围
项目核心是一个 3D 网格求交内核，作者声称其形式化规范精确刻画了结果网格的曲面形状，并保证了三角剖分满足一组实际可用的「良构性」条件。整个验证流程的关键设计是：
- 规范极简：人工只需读懂 93 行规范，无需理解 1,000+ 行实现细节。
- 证明极重：AI 产出了 60,000+ 行 Lean 证明，用以证明实现严格符合规范。
- 检查外包：正确性由 Lean 检查器机械判定，对 LLM 实现与证明本身零信任。
这种结构使得实现代码和证明都可以被当作「黑盒」对待，只要 Lean 通过，即可视为已通过验证。
AI 在流程中的角色
作者将整个工作描述为一次「智能体引导」过程：他按 README 中设定的里程碑驱动 AI 智能体逐步推进，由 AI 负责生成实现与证明代码，作者本人并不直接审阅这些代码的细节，只审阅顶层规范和阶段性产物。换言之，AI 既是代码作者，也是证明作者，但所有产物的正确性最终由形式化工具而非人工把关。
演示与可用性
项目附带一个 Web 演示页面，将经过验证的网格求交内核编译为 WebAssembly 在浏览器中直接运行。作者将这一架构定位为应对「AI 生成代码难以审查」问题的一种可行路径：与其审查 AI 的每一行输出，不如让 AI 同时产出形式化证明，再用独立检查器验证。
局限与边界
这一成果目前仍是 Show HN 级别的个人项目展示，Hacker News 上的得票与评论均较少。该工作流能否扩展到更大规模的软件系统、对 AI 智能体的形式化能力提出何种要求、以及与现有 AI 代码助手（如 Copilot 类工具）的整合方式，仍有待进一步验证。但对于关注「AI 写代码如何被信任」这一议题的开发者与研究者而言，它提供了一个可操作的范式样本。