A Proof of the Most Informative Boolean Function Conjecture
Abstract
Let X be uniform on {−1,1}n, let Y be obtained by passing its coordinates independently through a binary symmetric channel with crossover probability p, and let g:{−1,1}n→{0,1} be a Boolean function. We give a computer-assisted proof of the Courtade--Kumar conjecture I(g(X);Y)≤1−H2(p), where H2 is binary entropy, with equality attained by dictator functions. The present work builds on the differential-equation method, itself a limiting form of the auxiliary-receiver approach in network information theory using a continuum of degraded receivers. The proof proceeds from a local inequality to a dimension-independent bound on entropy production. Differentiation along the Boolean noise semigroup expresses entropy production as an average of edge costs. The key estimate is therefore an unrestricted Bellman inequality with two mean constraints and two entropy constraints, allowing arbitrary couplings of the edge variables. This paper and its supplement provide the proofs and computational verification records. The document is lengthy because it is designed to be entirely self-contained, deriving all proofs from first principles and reproducing the proofs of cited results. We also give a self-contained expository note explaining the reduction to a low-dimensional inequality and the ideas behind the key lower bounds. The entire proof, including all numerical certificates, has been formally verified in Lean end-to-end, and is available online.
Related
- On the most informative Boolean function under noise
- The Most Informative Bit and Beyond: A Proof of the Courtade--Kumar Conjecture and Multibit Extensions
- A Sharp Fisher-Information Inequality for Boolean Pairs: Proof of the Amari--Kobayashi Conjecture
- Dictators are most informative
- On a conjecture on the Kasami APN function: reductions, structure theorems, a proof for kbmod n∈{1,2,n−2,n−1}, and exhaustive verification for n≤ 13
BibTeX
@misc{chen2026proof,
title = {{A Proof of the Most Informative Boolean Function Conjecture}},
author = {Zijie Chen and Amin Gohari and Adel Javanmard and Honghao Lin and Vahab Mirrokni and Chandra Nair and David P. Woodruff},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.24931},
eprint = {2609.24931},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.24931},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - A Proof of the Most Informative Boolean Function Conjecture
AU - Zijie Chen
AU - Amin Gohari
AU - Adel Javanmard
AU - Honghao Lin
AU - Vahab Mirrokni
AU - Chandra Nair
AU - David P. Woodruff
PY - 2026
DA - 2026/09/24
PB - arXiv
DO - 10.48550/arxiv.2609.24931
UR - https://arxiv.org/abs/2609.24931
AB - Let X be uniform on {−1,1}^n, let Y be obtained by passing its coordinates independently through a binary symmetric channel with crossover probability p, and let g:{−1,1}^n→{0,1} be a Boolean function. We give a computer-assisted proof of the Courtade--Kumar conjecture I(g(X);Y)≤1−H_2(p), where H_2 is binary entropy, with equality attained by dictator functions. The present work builds on the differential-equation method, itself a limiting form of the auxiliary-receiver approach in network information theory using a continuum of degraded receivers. The proof proceeds from a local inequality to a dimension-independent bound on entropy production. Differentiation along the Boolean noise semigroup expresses entropy production as an average of edge costs. The key estimate is therefore an unrestricted Bellman inequality with two mean constraints and two entropy constraints, allowing arbitrary couplings of the edge variables. This paper and its supplement provide the proofs and computational verification records. The document is lengthy because it is designed to be entirely self-contained, deriving all proofs from first principles and reproducing the proofs of cited results. We also give a self-contained expository note explaining the reduction to a low-dimensional inequality and the ideas behind the key lower bounds. The entire proof, including all numerical certificates, has been formally verified in Lean end-to-end, and is available online.
ER -