Computer-assisted proof settles Courtade–Kumar: dictators are most informative

A Proof of the Most Informative Boolean Function Conjecture

Zijie Chen, Amin Gohari, Adel Javanmard, Honghao Lin, Vahab Mirrokni, Chandra Nair, David P. Woodruff

cs.DS, cs.IT

2026-09-22

A CUHK–Google computer-assisted proof shows that after a BSC, no Boolean function of the input carries more mutual information with the noisy output than a dictator.

What problem this solves

Courtade and Kumar asked a clean question in 2013. Let X be uniform on the Boolean cube {-1,1}^n, and let Y be a coordinate-wise noisy copy of X through a binary symmetric channel with crossover p. How much mutual information with Y can a single bit g(X) carry?

A dictator, which inspects one coordinate, achieves exactly 1−H₂(p). They conjectured that no Boolean function does better, in any dimension. That is the Courtade–Kumar conjecture, also called the most informative Boolean function conjecture.

They checked it by brute force up to n≤7. Over the next decade, Pichler, Piantanida, and Matz proved a weaker two-function form I(f(X); g(Y)); Samorodnitsky proved the claim when the channel is noisy enough that |1−2p| sits below a universal constant; Yu combined local optimality with computer-assisted estimates to widen the balanced-function range. A proof with no balance assumption, no noise restriction, and no dimension cap stayed open.

Method

The skeleton is the 2025 differential-equation method of Chen, Gohari, and Nair at CUHK, itself a continuum limit of the auxiliary-receiver method from network information theory. Follow the noise semigroup: the conditional entropy of g(X) given the channel output grows at a rate equal to an edge energy. Split the cube along one coordinate and the energy becomes the average of the two halves plus a two-point cost. A bound in every dimension therefore reduces to a two-point Bellman inequality: given two [0,1]-valued random variables with prescribed means and prescribed average entropies, the infimal edge cost must cover a concavity gap of a candidate function A.

The balanced candidate ϕ was already proposed in that earlier paper; its Bellman inequality was left as a conjecture. This work proves the inequality for ϕ, then introduces a bias correction ψ that folds in the output-entropy deficit 1−H₂(mean), and takes B = max{ϕ, ψ}. ψ alone fails the Bellman inequality, so the pointwise maximum is required.

ζ is the infimum of the edge cost under four moment constraints. The objective is linear in the law, so an optimizer is supported on at most five atoms, a search space of roughly fourteen dimensions. The proof never searches that space. It builds explicit lower bounds: a four-moment bound L₄, supporting planes, and a log-sum inequality. Analytic estimates cut off singular boundaries. What remains is a compact box, exhausted by outward-rounded interval arithmetic (Arb, MPFR, mpmath.iv). A certificate is a bisection of a rational root box; each leaf is either infeasible or satisfies a stated sufficient inequality on the whole box. Sampled points do not count.

On the Google side, Gemini inside the Stellar Colosseum multi-agent harness found counterexamples near the boundary of a generalized conjecture in the previous paper's appendix, which forced stronger lower bounds. The writeup is blunt: the overwhelming majority of novel ideas were generated by AI; CUHK supplied the max-ϕ candidate and one principal lower bound; Part 2, the passage from the balanced to the unbalanced case, ran with no human input.

Results

Main theorem: for every n≥1, every p∈[0,1], and every Boolean g,

I(g(X); Y) ≤ 1−H₂(p),

with equality for dictators and their complements.

There is no experimental table. What can be checked is the scope: no balance assumption, no restriction on noise, no restriction on dimension. Independently, Vu Khac Ky and Tuan Tran obtained a proof by a different entropy-production and spectral route; the two groups coordinated a simultaneous arXiv posting.

The computational side is a stack of certificates covering the small-boundary theorem, the seam and endpoints, stationary Case E, a radial stationary estimate, same-side boxes, opposite-side boxes, and the central square [1/10, 9/10]² at all positive feasible entropies. The document plus supplement runs to 251 pages, rewritten from first principles so cited lemmas can be checked in place.

Why it matters

For information theory and Boolean analysis, this is an endpoint of a line that started in 2013. Dictator optimality under coordinate noise is now a theorem. The statement sits next to hypercontractivity, isoperimetry, and sensitivity inequalities; a stronger Hellinger-type conjecture remains open.

For people who build AI systems, the paper is closer to a lab notebook. A decade-old finite-dimensional optimization was split open by a multi-agent loop plus interval arithmetic. Google had already flagged the problem in a survey of Gemini-accelerated research. What is reproducible is the certificate archive and the Arb logs, not the chat trace.

Nobody should expect an algorithm to copy. There is no model to train and no new coding scheme. A repeatedly partial inequality is now closed.

Limitations

A computer-assisted proof stakes correctness on interval enclosures and on the programs that emit certificates. Coverage (the bisection tree) and arithmetic (outward rounding) are checked separately; supplement S.24 distinguishes original runs, structural audits, and independent replays. That is still not a one-page human-scannable argument. A 251-page "self-contained" manuscript is itself an audit burden.

The authors record that Conjecture 5 in the previous paper's appendix is false: the AI found boundary counterexamples. The main conjecture survived, but the episode shows how brittle a candidate-function generalization can be.

The stronger Hellinger-type inequality that implies CK is untouched. The Ky–Tran proof appeared at the same time; neither side has cross-checked the other.

"The overwhelming majority of novel ideas were generated by AI" is the authors' own sentence. Readers can check the theorem and the certificate hashes. They cannot check idea provenance.

Terms

Source

What people are saying

Related papers

All paper explainers