AREX Feed Article
Google 团队宣布完整证明 Courtade–Kumar 猜想：解析部分经 Lean 验证，Ky 与 Tran 独立证明协调发布
北京时间 9 月 22 日上午 11 时 30 分（UTC 当天 03:30），Vahab Mirrokni 在 宣布：他的 Google 团队与香港中文大学合作者完成了信息论与布尔函数分析交叉领域长期公开问题 Courtade–Kumar 猜想（又称 Most Informative Boolean Function 猜想）一般情形的完整证明，论文链接随帖给出，证明的解析部分据称已在 Lean 定理证明器中通过验证。Mirrokni 的 X 账户简介自述其为 Google Fellow、副总裁（VP）。
随帖给出的题为《A Proof of the Most Informative Boolean Function Conjecture》，9 月 21 日提交 arXiv；同日提交的还有 《Dictators are most informative》。按 Mirrokni 的说法，这是两条彼此独立、路径大不相同的证明，双方协调在同一天分别发布并互相引用——这个安排也写进了主论文的致谢。
Ky 与 Tran 的论文《Dictators are most informative》首页（，2026 年 9 月 21 日提交）。
噪声信道里的一比特：悬置十三年的「哪个函数最有信息量」
设 X 均匀分布在 {−1,1}ⁿ 上，每个坐标以交叉概率 p 独立翻转，通过一条二进制对称信道（binary symmetric channel，BSC）得到带噪版本 Y；任选布尔函数 f，公开一比特总结 f(X)，要最大化的是 f(X) 与 Y 的互信息。Thomas Courtade 与 P. R. Kumar 在 2013 年论文《Which Boolean Functions Maximize Mutual Information on Noisy Inputs?》中猜想：最优的是坐标投影 f(x)=x_i——这类函数被称为 dictator（「独裁者」）函数——对应上界 1−H₂(p)，其中 H₂ 为二进制熵，主论文摘要即以此为陈述形式。Courtade 与 Kumar 还把这个问题与 information bottleneck（信息瓶颈）问题联系在一起：对一个相关观测做压缩描述时，应为「一比特侧面信息的取值」保留多少信息。
十三年里，猜想没有被整体解决，只被逐块推进。据 的综述（以 ρ 记噪声水平，ρ 越大噪声越小）：Samorodnitsky 证明了 ρ 不超过某个绝对常数 ρ₀ 时结论成立；Yu 把平衡情形（均值为零）推进到显式范围 ρ ≤ 0.914，并对任意均值给出进一步界；Ordentlich、Shayevitz 与 Weinstein 用傅里叶分析改进过一般上界；Anantharam、Gohari、Kamath 与 Nair 用 hypercontractivity 研究了把两个向量都约化为布尔输出的更弱版本；Pichler、Piantanida 与 Matz 证明了双输出情形的不等式；Kindler、O'Donnell 与 Witmer 考察过固定均值与连续形式的版本，并记录了它引起的关注。受关注程度的量级，有 Yu 与 Tan 2022 年专著的措辞为证——他们称之为「信息论中最重要的开放问题之一」。Mirrokni 在帖子里补充了结构层面的关联：猜想与 Talagrand 等周不等式、Bobkov 不等式及其最优形式相关，某些参数范围内还能推出经典的 Harper 边等周不等式。
主论文：从局部不等式到两情形的长证明
主论文挂在 arXiv 的 cs.DS（数据结构与算法）分类下，七位作者为 Zijie Chen、Amin Gohari、Adel Javanmard、Honghao Lin、Vahab Mirrokni、Chandra Nair 与 David P. Woodruff。按的作者信息，Chen、Gohari、Nair 三人属香港中文大学信息工程系；Javanmard、Lin、Mirrokni、Woodruff 四人的页面邮箱均为 google.com 域名，单位栏还出现 University of Southern California 与 Carnegie Mellon University。
把这项工作定性为 computer-assisted proof（计算机辅助证明）：对任意布尔函数 g 证明 I(g(X);Y) ≤ 1−H₂(p)，等号由 dictator 函数取得。技术路线写得具体：先建立一条 local inequality（局部不等式），得到与维度无关的熵产生（entropy production）上界；沿 Boolean noise semigroup（布尔噪声半群）做微分，把熵产生表达成 edge costs（边代价）的平均；核心估计是一条带两个均值约束与两个熵约束的 unrestricted Bellman inequality（无限制 Bellman 不等式），允许对边变量做任意耦合。摘要同时交代了方法的谱系：这条微分方程路线是网络信息论中 auxiliary-receiver 方法——用一列连续退化的接收机——的极限形式。
从目录看，正文按 Balanced Case 与 Unbalanced Case 两大块展开，其中出现「Same-side estimates and finite certification」（同侧估计与有限认证）一类小节。论文声明全文按「完全自足」设计，从第一性原理重推所有被引结果，因此篇幅很长；计算机辅助部分的支撑材料以在线补充形式提供。至于 Lean，这部分信息出自 Mirrokni 的帖子：他写道，团队已成功在 Lean 中验证证明的解析部分。
Gemini 与 Stellar Colosseum：这条证明背后的多智能体流水线
Mirrokni 把结果归因于「深度的人机协作」：使用了内部与外部的多款 Gemini 模型，并大量使用 Stellar Colosseum harness。这个 harness 有正式论文：《Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science》，9 月 14 日提交，作者为 Honghao Lin、David P. Woodruff、Yuan Deng、Jieming Mao、Song Zuo 与 Mirrokni。他还提到，Courtade–Kumar 猜想正是团队此前论文 （《Accelerating Scientific Research with Gemini: Case Studies and Common Techniques》）着手解决的问题之一。
harness 的对外形态，在 Google Antigravity 里有描述：Teamwork 是 Antigravity 内的多智能体编排框架，智能体按 pattern（模式）组队，在数小时到数天里自主提案、互评、修正，目前以 /teamwork-preview 的形式对所有付费计划开放。其中面向数学与理论计算机科学的 Long Proof pattern 机制如下：并行生成多条候选证明策略，每条配一个专职 falsifier（证伪者）负责挑错；synthesis tree（综合树）把候选与批评合成更强的解；依赖图让独立子问题并行推进；失败草稿与验证发现沉淀进跨轮次复用的 pitfall registry（陷阱登记表）。博客称 Long Proof 最初是独立的研究 harness，后来移植进 Teamwork，并「显著强化与推广」了 2602.03837 的工作流；它列出的七个已解决开放问题中，Knuth's Cycles 猜想的 40 页证明经 Lean 验证，另有 TCSBench 71% 的成绩（博客称之为其内部测试中的最高分）——这些都出自 Google 一侧的表述。
博客发布时列出的成果清单里没有 Courtade–Kumar 猜想这桩工作；两者的关联来自 Mirrokni 9 月 22 日的帖子。他在帖子末尾给出两个对外动作：Stellar Colosseum 已作为 /teamwork 的 long proof 模式对外开放；下一步计划把数学协作功能迁入 Antigravity，作为一个面向外部的数学协作平台。
同一天的第二条路径：Ky 与 Tran 的「Dictators are most informative」
第二篇论文来自 Vu Khac Ky 与 Tuan Tran，属 cs.IT（信息论）分类，只有一句：在所有布尔函数 f:{−1,1}ⁿ→{−1,1} 中，dictator 函数为经独立二进制噪声观测的均匀随机输入保留最多信息。脚注显示，Tran 的研究受国家自然科学基金优秀青年科学基金项目（海外）资助，项目号 GG0010007003。
两条证明的差别，主论文引言写得更具体：写作期间经私下交流得知对方工作后，他们描述两者路径大不相同——Ky 与 Tran 发展出一套新的熵产生与谱方法（spectral）框架，而主论文走微分方程路径；论文并致谢两人「在协调两篇稿件同时提交 arXiv 时展现的同仁风范」。Mirrokni 帖子里的时间线与此吻合：上周得知对方结果，随后双方协调各自发布、互相引用，他并向 Ky 与 Tran 道贺。
能核对的与尚待核对的
截至 9 月 22 日发稿前核查，Mirrokni 这条帖子有 223 个赞、15,135 次浏览、24 次转发——题材分量不轻，声量却不大。但帖子的关键内容不依赖传播度：两篇论文都已公开，作者名单与单位、两条不同的技术路线、写进主论文致谢的协调声明，以及 Ky 与 Tran 首页上的猜想陈述与此前结果综述，都能在文本层面直接核对。
不能同样直接核对的，是「完整证明」这个结论本身。按帖子原话，Lean 验证只覆盖解析部分；计算机辅助环节的证据不在两篇论文文本之内，而是以在线补充记录的形式提供，摘要称之为 computational verification records。解析部分可以沿 Lean 证明逐行检查；其余部分目前系于团队自己发布的验证记录——那是两篇公开文本之外、需要另行获取才能检查的部分。