一个 GitHub 项目最近把 AI 编程里最别扭的问题摆到了台面上：代码可以让模型写，但你到底信谁？

项目做的是多多边形求交。给定两个区域，输出一个新的多多边形，使它的内部点集合正好等于两个输入内部点集合的交集。作者称，据其了解，这是首个形式化验证的多边形求交实现。

更扎眼的是模型对照。作者说，Claude Opus 4.8 在隔离环境里，几小时内无提示重证了主要定理，还处理了 Opus 4.7 没处理好的重叠线段特殊情况。

但这事不能讲成“Claude 证明了自己可靠”。可靠性不在 Claude 身上。它来自 Lean checker，来自人类审过的约 87 行规格文件，来自一条被故意收窄的审查路径。

项目验证的不是 demo，而是一个数学承诺

多多边形求交听起来像图形编辑器里的普通功能。两个带洞区域重叠，系统输出新的边界。用户只看结果图，工程师要处理的是顶点贴边、线段重合、洞和外轮廓交错。

几何算法最怕边界情况。测试能覆盖样例，覆盖不了无限点集。这个项目把核心性质写进 Lean：输出多多边形的内部点集合，必须等于两个输入内部点集合的交集。

这不是“跑通几张图”。这是把结果是否正确，落到可检查的数学规格上。

问题这次项目的说法需要怎么读
验证对象多多边形求交：构造两个区域内部点集合交集对应的新多多边形不是简单画图，也不只是样例测试
正确性来源Lean checker 检查证明；人类审查约 87 行规格文件信任检查器和规格，不信模型自证
相关工作作者提到 NASA 2021 的 polygon merge相关但不是同一问题；后者不是这里的多多边形求交
作者判断据其了解，这是首个形式化验证的多边形求交实现可以当重要线索，不能当无条件行业定论
现实缺口性能优化、证明简化、SVG 导入导出仍是后续事项目前不是工业级成品宣言

这里最关键的设计，是人类没有逐行审 AI 生成的全部证明和实现。大量文件可以不审。只要 Lean checker 能过，复杂证明就不再靠“我觉得模型写得像那么回事”。

这对开发团队很具体。写业务 CRUD 的团队不必立刻搬去 Lean；但做几何、编译器、协议、金融合约、航空航天这类高代价软件的人，应该开始重新分配审查精力：少花时间读模型吐出的长代码，多花时间写清楚规格、约束和不可违反的性质。

Opus 4.8 的变化，是证明策略变强了

作者给出的代际对照，比“代码写得更快”更有价值。因为形式化证明难的不是把句子写进文件，而是找到能被 checker 接受的路线。

模型阶段作者观察到的能力人类仍要补什么
Opus 4.5 / 4.6能处理非平凡 Lean 证明需要人类给严密证明草图，并拆成小步
Opus 4.7能迈大步，能从定理抽取验证算法仍要提示 Eulerian circuits，并指导特殊情况
Opus 4.8几小时内重证主要定理，处理重叠线段作者称在隔离环境中无提示完成关键工作

这个变化说明，模型不只是更会补代码。它更像开始学会在证明空间里找路：提出中间引理，发现路线不对，换策略，处理特殊情况。

我更在意这一点。因为 AI 编程过去的主要幻觉，不是它完全不会写，而是它经常写出一种“表面顺滑”的东西。函数名对，注释对，测试样例也对，真正的边界却藏在暗处。

形式化验证把这种顺滑感撕掉了。Lean 不看语气，不看自信，不看模型是不是最新版本。过就是过，不过就是不过。

“工欲善其事，必先利其器。”这里的器不是 Claude，而是规格语言、证明环境和检查器。LLM 负责挥毫，Lean 负责量尺。没有尺，再漂亮的代码也只是手艺活。

这对工具链开发者和技术负责人有直接影响。短期动作不是采购一个更贵的模型，然后宣布代码审查可以裁掉。更现实的动作是挑一小块高风险模块试点：先写规格，再让模型生成实现和证明，最后看 checker、性能和维护成本能不能一起过关。

如果做不到这一步，形式化验证就只是论文味很重的演示。能做到，AI 编程才开始从“看起来能跑”进入“能被约束地交付”。

真正的账还没结：规格、性能和工程成本

这件事少见地做对了一点：它没有要求我们相信模型。它要求我们相信一套可复现的检查流程。

但形式化验证有一个老问题：它只保证规格写到的东西。规格没有写性能，代码可以慢；规格没有写 SVG 导入导出，工具可以不好用；规格没有覆盖真实产品里的数据格式、容错、交互和维护需求，验证通过也不等于用户满意。

作者也承认，在形式化约束下生成的代码可能更慢，也可能忽略规格外的实际工程需求。这句话很重要。很多 AI 工具宣传喜欢把“正确”说成一个大词，但工程里的正确经常分层：数学正确、接口正确、性能可用、维护可承受，不是一回事。

所以接下来最该观察的不是模型演示多漂亮，而是三件事：

  • Lean checker 能否被普通开发者稳定复现，而不是只在作者环境里成立。
  • 87 行规格是否真的覆盖用户关心的核心行为，尤其是退化几何和边界输入。
  • 经过验证的实现能否在性能、导入导出和维护成本上接近真实项目需求。

对工程团队来说，当前最合理的姿势是观望但不忽视。不要把它当现成库直接塞进生产系统；也不要把它当玩具。可以把它当作一个信号：未来会写代码的人很多，能把需求压成可验证规格的人会更稀缺。

这也是 AI 编程的分水岭。过去大家争的是模型能不能写更多代码。现在更该争的是：哪些代码可以交给模型生成，哪些性质必须交给机器检查，哪些规格必须由人类负责。

权力结构也变了。以前人审代码，是人在给机器兜底；现在人审规格，是人在定义机器不得越过的边界。边界一清楚，AI 才不再靠话术赢信任。

回到开头的问题：Claude 写对几何算法，不是最值得兴奋的部分。

真正有意思的是，它把 AI 编程的信任问题从“你信不信这个模型”改成了“规格写没写对，checker 过没过，人类审查面有没有压到足够小”。这比模型自夸可靠，要诚实得多。