2026-10-30
Hupyy 的神经符号系统 LPM 用 Lean 4 写出编码与拆分,cake_lpr 核完 38661140 片 SAT 叶子,信任基下得到 w(2;3,21)=416。至今团队之外还没有一次全量重放。
w(2;3,t) 是最小的 n:1 到 n 的任意红蓝染色,都得含一条红色三项等差数列,或一条蓝色的 t 项等差数列。t=21 时,Kullmann 在 2010 年证明 w(2;3,21)≥416,并猜想等号成立。Ahmed、Kullmann、Snevily 在 2014 年给出 1 到 415 的合法染色,把下界坐实,并写明用相近算力证出等号,看起来要有新的算法想法。读到的原始文献里,精确值停在 t=19 的 w(2;3,19)=349,那次大约 196 个 CPU 年,报告讨论了归结证明,没有可单独核验的上界证书。t=20 的 389 归于 Kouřil 2015 年的一章,这一章没读到全文,证书在不在是未知的。
2026 年 9 月 22 日,Google DeepMind 的 Formal Conjectures 把 W(3,21)=416 标成 research open,10 月 28 日的提交里标签还在。1 到 416 的染色有 2 的 416 次方种,十进制 126 位,只能写成命题公式再逐情形反驳。
公式 F(3,21;416) 有 416 个变元、47,176 个子句:43,056 条禁红色三元组,4,120 条禁蓝色 21 项等差数列。可满足当且仅当存在合法染色,这个等价在 Lean 里证过。
拆分从中心向外。位置 i 与镜像 n+1−i 成对,按离中心远近排序。情形 j 要求更靠内的对与镜像同色,第 j 对左边红、右边蓝。再加一个全部与镜像同色的回文情形,共 209 个。公式在反转下不变,Lean 证明原公式若可满足,这 209 个里至少有一个可满足。两种颜色规则不同,对调颜色不是对称,搜索也没有被收成只看回文。
每个情形再用 cube-and-conquer 切开:前瞻求解先挑部分赋值,再逐个反驳。规划器按随机下探切 item,目标大约每项 4 亿个估计节点。驱动器对子节点做 500 次下探,估计超过 250 万节点就再切;引理超过 400 万也再切,追加深度 5。叶子由改过的 tawSolver 写出 LRAT,从管道流进 cakelpr,不落盘。cakelpr 是 Tan、Heule、Myreen 用 CakeML 验证过的检查器。整段输出恰为一行 s VERIFIED UNSAT 才算过。它拒绝证明时退出码仍是 0,退出码只记录、不采用。
16 个情形是两层覆盖,c001 到 c015 以及 c018,共 235,314 个 item,其余 193 个是扁平覆盖。合成定理把「立方体盖住情形」和「每片叶子不可满足」收成 1 到 416 无合法染色。下界染色由 Lean 的 decide 在核内判定合法。假设成立时,定理给出 IsW 21 416,即 w(2;3,21)=416。同一流水线在 t=20、n=389 上给出 IsW 20 389。
LPM 是论文所称的可扩展神经符号系统。它的智能体写了 Lean 4 开发,并在 AWS 上跑完计算。提交记录把 Claude Fable 5.1、Claude Opus 5.5、Claude Opus 5、Codex 和 Codex GPT-6 列为 commit 共同作者。计入结果的只有 Lean 核接受的步骤和 cakelpr 接受的反驳。打印、摘要比对和绑定在两个检查器之外,列为信任项。正文没有机器检查。
最终语句只依赖公理 propext 和 Quot.sound,没有选择公理,也没有 native evaluation。那是用编译后的程序代替核检查,再把结果当成公理。Szeider 证明 w(2;3,17)=279 和 w(2;3,18)=312 时用过它。这里 38,661,140 片叶子的判决留在假设里。
| 量 | t=21 | t=20 |
| 信任基下的结论 | w(2;3,21)=416 | w(2;3,20)=389 |
| 已绑定情形 | 209 | 195 |
| 完成的叶子 | 38,661,140 | 5,244,544 |
| 进程 CPU 小时 | 390,516.0 | 求解 29,646.9,检查 10,942.9 |
| 证书流,不存储 | 5,069,860,346,325,430 字节 | 594,078,127,187,870 字节 |
390,516.0 小时里,带证明的求解占 279,602.4,叶子检查占 104,298.4。生产阶段 870 台机器、24 种 Graviton4,449,427.374 个 vCPU 小时。单叶进程 CPU 中位数 22.2 秒,95 分位 114.5 秒,最大 433.0 秒。搜索节点中位数 422,589。
另一套程序不看绑定器代码,从原始记录重推 209 个覆盖:立方体与 38,661,140 片已接受叶子一致,无缺失、多余或重复。定理用到的 235,523 个覆盖摘要,重印后逐字节相同。
抽查重解 30,000 片叶子,覆盖全部 209 个情形,30,000 片的公式摘要、判决、节点数和引理数都与记录一致。花费 292.2 个进程 CPU 小时,墙钟 1.7 小时,一台 c8g.metal-48xl。若每条记录独立出错的概率至少万分之一,这份样本有至少 95% 的概率撞上一条。单侧 95% 上界大约 0.00009985。这个界只管随机散布的错。
Alexander Fedin 在 Hupyy,未参与计算、形式化或写作。包内 1,899 个文件与 SHA256SUMS 一致,458 条定理的公理列表与随包清单一致,主定理只依赖 propext 和 Quot.sound。他自编译的 cakelpr 重放了 t=20 的 c080(8 片叶子,246,152 个节点)和 t=21 的 c074(11 片叶子,1,392,315 个节点,83.6 秒)。他写明这是 209 里的一个情形,用的是作者的包。Lean 构建报告为 PARTIAL,发布包不含手稿,三项手稿检查用不上。
布尔毕达哥拉斯三元组那次,切分加求解约 3.5 万 CPU 小时,DRAT 证明近 200 TB 并且留下了。这里证书流约 5070 TB,大约 25 倍,检查完就丢。论文不声称新算法,也不声称更快。t=20 的 389 是对 Kouřil 所归数值的带证书核对,不声称首次算准或首次认证。
猜想从 2010 年挂到 2026 年 10 月,DeepMind 的开放列表上还在。信任基若成立,w(2;3,21)=416 可以从那张表拿掉,w(2;3,20)=389 也有了这篇所读文献里没有的逐叶子检查。
交付的是证据形状。一条 Lean 定理,假设是有限个文件,每份反驳被 cakelpr 读过,证明不存盘,文件用 SHA-256 绑回 Lean 项。要用结果,得用重放包:配套 Zenodo 里有源码、209 个情形的交付集和每叶记录。重查一片叶子就要把证明重新生成。美元花费没有公布。
等号没有在 Lean 核里闭环。编码、拆分、合成和 415 的下界染色是核内证明。叶子的不可满足来自核外记录。早先把一个 85 文字的子叶子证书导进内核,五个模块花了 85,721 秒,峰值 18.39 GiB。这个规模能否整包进内核,论文列为开放问题。
证明不留存。求解加叶子检查共 383,900.8 个进程 CPU 小时,全量重放是再做一次同量级计算。生产团队之外、Hupyy 之外,没有人重查过每一片叶子。t=20 那次所谓非作者重放,执行者仍是团队里的自动化智能体:覆盖 195 个情形中的 184 个,只占叶子的 5.5%,而且只重解每行最小的三片叶子和单元反驳的叶子。3 万片抽查约占 38,661,140 的 0.08%。
负对照说明这份构建会拒绝改过的证书,并不重新证明检查器在这个规模上可靠。汇编按上游发布时的摘要被信任,论文不声称它等于 CakeML 的编译输出。未逐叶用 Lean 打印的叶子,还信任编译后的打印程序,以及 Python 与 Lean 一样用十进制写整数。这两处若犯了同一个错,摘要比对看不见。两层覆盖的重放路径还没有从包里对一个两层情形跑过。w(2;3,22) 是否走得通,没有讨论。作者 Eitan Nahmias 隶属开发 LPM 的 Hupyy,Fedin 也在 Hupyy。