devgo.cn有个图论猜想叫 Berge-Fulkerson，悬而未决半个多世纪：任何无桥三次图（三正则图，每个顶点恰好连3条边，而且删掉任何一条边都不会让图断开）都存在6个完美匹配（一种覆盖所有顶点且互不相交的边集，相当于给每个顶点只配一条边），允许重复，使得每条边恰好出现在其中2个匹配里。这个猜想有多硬？Open Problem Garden 把它评为“Outstanding”，而且它对于能3边染色的图是平凡的——所以它实际上是在说：所有无桥三次图（包括那些著名的“snark”，比如彼得森图）都接近能3边染色。2010年 Mazzuoccolo 证明了它等价于另一个形式：每条边可以被5个完美匹配覆盖。
现在有人把事情搞大了：在 Lean 里做形式化验证。Lean 是一个交互式定理证明器，能把你写的数学证明变成机器可检查的代码，每一个推理步骤都要经过内核验证，杜绝人为错误。这个项目叫“Come prove the Berge Fulkerson conjecture with a swarm of agents”，直译为“来和一群智能体一起证明 Berge Fulkerson 猜想”。作者提供了一个 Prop（Lean 里的命题类型）定义，把这个猜想精确地写成了代码，目标是让部署的验证器接受它。但它不是直接给出证明，而是发布了一系列辅助结果，像是拼图碎片——每一个都经过了独立验证，但整体还差临门一脚。
我读下来最惊讶的是：作者把抽象图论问题拆成了一堆看起来像“边界代数”的引理。比如“有限六色边界代数”：把图的边染成6种颜色，用一些 switch（切换）操作去重组匹配。有个引理说，如果两个 duad（双色组合？这里 duad 是某种特定的颜色对结构）互不相交，那么对其中一个做 switch 不会影响它与另一个的交集掩码。这听起来很数学，但本质上是在用少量算术规则替代大量图论推理——把图的结构问题降维成布尔代数问题。还有几个引理是局部的算术断言，比如“七个例外以外不存在满足 sum_j w(j)=2+w(i) 的向量”，这是在 BF-cover Helly 论证里处理物理边负载的步骤。每个引理都标注了状态：有的被形式化证明了，有的只是“独立审计的辅助结果”，没被内核检查。
为什么这么干？因为像 Berge-Fulkerson 这种“简单但暴力搜索不可能”的猜想，传统证明往往需要极其复杂的组合构造，人写容易出漏，机器写又难。作者的思路是：让 Agent（这里可以理解为自动化推理程序或AI智能体）去探索和生成候选引理，再用 Lean 内核去验证真伪。这很像现在大模型辅助科研的做法——但这里的关键是**可复现的验证链**：每个引理都必须绑定到特定版本的 Lean 环境（v4.33.1）和 Mathlib，甚至记录了源文件的 SHA-256，确保你看到的结果和验证器跑过的东西完全一致。这比单纯在 arXiv 上贴证明草稿要严谨得多。
这套做法的启发很直接：如果你是做形式化验证或安全关键系统的，可以借鉴它的“审计批次”机制——把大定理拆成无数小引理，每个引理独立验证并附带环境指纹，这样即使整体证明没完成，已证部分也能被他人复用。如果做 AI 辅助数学，它能避免模型产生幻觉——模型可以自由“瞎猜”引理，但 Lean 会当场拒绝错误的对象。
当然也有坑：作者反复强调“接受一个目标不等于证明它”，辅助引理“不断言存在实际图路径或完整证明”。所以现状是——核心猜想依然开放，但这些局部的、机器验证过的碎片已经铺了一地。将来如果有人把这些碎片拼起来，也许就是历史性突破。对于普通开发者，这篇文章的价值不在于猜想本身，而在于展示了一种“人机协作验证复杂数学”的标准流程：精确命题、环境锁定、逐步击破。你可以在自己的项目里试试：用 Lean 或 Coq 把关键不变量形式化，让 AI 辅助生成引理，再用内核验证——这或许能帮你写出真正可信的高复杂度代码。
内容与图片版权归原作者所有 · 原文: https://provetogether.ai/problems/15