结果族 184：Correspondence coloring with a fixed forbidden subgraph · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
宴会上想挑一群互不相识的人。任意图里总能挑出约 n/(d+1) 个（d 是平均熟人数）；但如果全场不存在 4 个两两都认识的人，能挑的其实多得多——多出一个对数因子。论文证明了 1981 年 Ajtai–Erdős–Komlós–Szemerédi 猜想：无团图的独立集至少有 c_r·n·log d/d 个，并去掉了此前最佳界中残留的 log log d 损失。
关键词卡片
看个具体例子
数字版定理（n=10^6 个顶点、平均度 d=100、无 K₄）：
@@M@@\alpha(G)\ \ge\ c_4\cdot\frac{10^6\cdot\ln 100}{100}\ \approx\ 46000\,c_4@@
而平凡保证只有 n/(d+1) ≈ 9901 个——禁团带来的额外收益恰是 ln 100 ≈ 4.6 倍。此前最好结果（Shearer 1995）还带着 log log d 的分母损失，本文彻底去掉它，n·log d/d 这一阶即使对无三角形图也已最优。
为什么值得关心
独立集大小直接关系到染色、装箱与网络问题；它还是同族对应染色论文的方法源头（乘子构造与熵-分裂技术），并且是结果族中已获机器验证的基石。
已 Lean 形式化
第一级台阶
导读的”宴会挑互不相识的人”翻译过来：对象是一张图，顶点是宾客，相邻表示相识；要挑的是一个两两之间没有边的小组。已知全场平均每人认识 d 位宾客时，总能挑出约 n/d 个人的小组；比喻里禁掉的”四个人两两认识”就是禁止图里出现固定大小的团——这份稀疏性应当让小组能挑得更大。
第二级台阶
| 用本科语言精确化：独立集是两两不相邻的顶点集合，最大者的大小记 α(G)；平均度 d = 2 | E | /n 度量稀疏程度；图称 K_r-free，若不含 r 个两两相邻的顶点。一般图有平凡下界 α(G) ≥ n/(d+1)，且不交团的并表明它无法改进；排除固定团后，AKS（1980）与 Shearer 在无三角形图上证明了多出一个对数因子的界。 |
第三级台阶
定理在这样的语境下陈述：对每个固定整数 r ≥ 4，存在常数 c_r > 0，使每个平均度 d ≥ 2 的 n 点 K_r-free 图满足 α(G) ≥ c_r·n·log d/d，常数对 n 与 d 一致。假设 r ≥ 4 挡住的是三角形密集的极端情形——无三角形（r = 3）早有更强结果，r ≥ 4 时三角形允许存在，须用边质量控制三角形质量；d ≥ 2 只是排除对数无意义的退化。结论去掉了 Shearer（1995）界中残留的 log log d 分母，解决 Ajtai–Erdős–Komlós–Szemerédi 1981 年猜想（Erdős 问题 802）；且 n·log d/d 这一阶即使在无三角形图上也已最优，定理在阶的意义上是终结性的。此主结果已在 Lean 中形式化。
论文证明：对每个固定 @@M@@r\ge 4@@，任何 @@M@@n@@ 个顶点、平均度 @@M@@d\ge 2@@ 的 @@M@@K_r@@-free 图都含有大小至少 @@M@@c_r\,n\log d/d@@ 的独立集 (independent set)，从而解决了 Ajtai–Erdős–Komlós–Szemerédi 1981 年猜想（Erdős 问题 802），并去掉此前最佳界中残留的 @@M@@\log\log d@@ 损失。
独立集是图中两两不相邻的顶点集合；一般图有平凡界 @@M@@\alpha(G)\ge n/(d+1)@@，且不交团并表明它已最优，而排除固定团 (clique) 会迫使独立集变大。Ajtai–Komlós–Szemerédi 1980 年证明了无三角形情形的对数改进，Shearer 随后对无三角形图得到渐近系数 @@M@@1@@。1981 年 Ajtai、Erdős、Komlós、Szemerédi 猜想：对每个固定被禁团 @@M@@K_r@@，同阶的 @@M@@\Omega_r(n\log d/d)@@ 成立；他们自己只证得较弱的 @@M@@\Omega_r(n\log\log d/d)@@，Shearer 1995 年改进为 @@M@@\Omega_r(n\log d/(d\log\log d))@@。本文消去了最后的 @@M@@\log\log d@@ 分母；且 @@M@@n\log d/d@@ 这一阶即使对无三角形图也已最优（相差常数倍），故定理在阶的意义上是终结性的。
定理：对每个整数 @@M@@r\ge 4@@ 存在常数 @@M@@c_r>0@@，使每个 @@M@@n@@ 顶点、平均度 @@M@@d\ge 2@@ 的有限简单 @@M@@K_r@@-free 图满足
@@M@@D\alpha(G)\ \ge\ c_r\,\frac{n\log d}{d},@@
常数对 @@M@@n@@ 与 @@M@@d@@ 一致，可取 @@M@@c_r=1/(16D_r)@@。证明的核心——加权三角形定理——是关于交叉质量 (cross-mass) 条件的独立命题，不依赖任何团假设，可单独使用。
证明分三个阶段。第一阶段选”好权重”：研究泛函 @@M@@F_G(w)=\sum_v w_v(1-\log w_v)-M_G(w)@@，即熵减边质量（Davies 势函数的特例），其最大化子 (maximizer) 满足驻点方程 @@M@@\log(1/w_v)=w(N(v))@@ 与一个变分恒等式。再把 AEKS 的稀疏子图递归改造成均值一随机乘子 (mean-one random multipliers)：在 @@M@@K_r@@-free 图上反复摘除重的开邻域（每块自动 @@M@@K_{r-1}@@-free），随机保留一块并除以其选择概率，使期望边质量降至 @@M@@\varepsilon s^2@@。在变分不等式中放大集合 @@M@@S@@ 的权重、清零集合 @@M@@D@@ 的权重会产生负交叉项，由此得到关键的交叉质量估计 @@M@@e_w(S,D)\le 16r^2\,g_x(w(S))@@（当 @@M@@w(S),w(D)\le e^x@@），且它在删边与不重复保留原边的顶点分裂下存活。
第二阶段证中心不等式 @@M@@T_G(w)\le B_r M_G(w)@@：最大化子处的三角形质量受边质量控制。先删去公共邻域权重过小的边，丢失的三角形记入边质量账；再在每个顶点 @@M@@u@@ 的邻域内运行带停留的加权随机游走。熵平滑引理表明 @@M@@\lceil x\rceil@@ 步内游走行分布相对权重的平均熵 (entropy) 仅 @@M@@O_C(\log x)@@，故存在增量极小的步，经相对熵 (relative entropy) 到总变差距离 (total variation distance) 的换算推出：在有序三角形分布下，三角形另两顶点出发的行分布平均距离 @@M@@O(\sqrt{\log x/x})@@。联合采样这些分布为 @@M@@u@@ 的关联边分组，用逆向转移概率的截断控制组内权重，按组分裂 (vertex splitting) 顶点后，最大邻域权重从 @@M@@e^x@@ 降至 @@M@@e^{\sqrt{x}}@@，损失跨迭代可求和；邻域权重最终有界时，三角形质量直接被边质量控制。
第三阶段选独立集：最大度 @@M@@\le\Delta@@ 时以常数测试权重 @@M@@p=\log\Delta/\Delta@@ 得极值 @@M@@F_G^*\ge@@ 常数倍 @@M@@n(\log\Delta)^2/\Delta@@；按权重比例随机选点、删其闭邻域，平均代价恰把邻居之间的边按三角形记账，故存在代价 @@M@@\le D_r\log\Delta@@ 的顶点，归纳给出 @@M@@\alpha(G)\ge n\log\Delta/(4D_r\Delta)@@，且 @@M@@\Delta@@ 在归纳中保持不变。最后删去原图中度 @@M@@>2d@@ 的顶点（总数不足一半），以 @@M@@\Delta=2d@@ 代入即得定理。
本篇主结果已在 Lean 中形式化验证，是结果族 184 的基石；姊妹篇（对应染色）显式沿用其乘子与熵-分裂方法，并在染色场景下自证全部所需引理，两文由此互相印证。按 OpenAI 官方声明，未经形式化的结果可能存在问题，族内尚未形式化的染色篇仍待社区核验。定理为存在性结果，不涉及算法效率与最优首项常数。
问 1：证明中最关键的一步是什么？
（答：中心不等式 T_G(w) ≤ B_r·M_G(w)——在泛函 F_G(w)=Σ w_v(1−log w_v) − M_G(w) 的最大化子处，加权三角形质量被加权边质量控制。证明须在每个顶点邻域内跑带停留的随机游走，用熵平滑控制行分布的平均熵，把有序三角形分布下两条边的行分布拉近，再按联合采样分组、以逆向转移概率截断控制组重，经顶点分裂把最大邻域权重从 e^x 压到 e^√x 且损失可求和。这是全文技术核心。）
问 2：交叉质量条件为什么设计成与团无关？
（答：加权三角形定理被刻意陈述为只依赖交叉质量假设的独立命题，不含任何团条件。好处有二：它在删边与”每条原边至多保留一次”的顶点分裂下存活，使迭代可以在不再是最大化子的权重上继续；也使它能被姊妹染色篇单独搬用。）
问 3：与 Shearer 1995 及近年局部占用理论相比，真正新意是什么？
（答：Shearer 与 DKPS、Dhawan 等的界都残留 log log 损失；DJM2025 虽达首项系数 1 但只覆盖三可染禁图——完全三部图说明那不涵盖全部 K₄-free 图。本文对一切固定 r ≥ 4 消去 log log d，且阶已最优，是 AEKS 猜想的完整解决。）
问 4：Lean 形式化验证了什么、没验证什么？
（答：据任务元数据与导读，主定理已在 Lean 中形式化——这在同批结果中少见，大幅压低了证明出错的概率。但形式化通常锚定主定理陈述与其证明骨架；姊妹染色篇的调整引理、以及”存在性结果、不涉算法效率与最优常数”的边界，仍在形式化覆盖之外。）
问 5：这类 AI 生成证明原本最可能在哪里出错？
（答：熵估计只控制”指定三角形分布下的平均”，而分裂论证恰好只用这些平均——引言专门强调这一对齐；若某步不慎对分布提出逐点要求，论证即失效。这类”平均值与逐点”的错位、以及可求和损失 e^x → e^√x 的迭代账本，正是机器生成长证明的高危点；本篇有幸由形式化兜底。）
问 6：谁会用到它？
（答：姊妹对应染色篇显式沿用本文的乘子构造与熵-分裂方法；Ramsey 理论中 r(s,t) 的对数指数估计与之同族互补——本文对每个输入图用其自身平均度给出控制；导读还提到它服务于染色、装箱与网络问题。）
总评
（终结一个 1981 年猜想、去掉最后的 log log 损失、阶达最优且主结果经机器验证，这是同批结果中可信度与分量俱佳的一篇；剩余风险仅在形式化未必覆盖的辅助命题与姊妹篇的移植环节。）