The Courtade–Kumar conjecture proved with help from Gemini models

Vahab Mirrokni@mirrokni

I'm happy to share that we have completed a proof of the Most Informative Boolean Function conjecture (a.k.a. Courtade–Kumar conjecture) in full generality, resolving a longstanding central open problem at the intersection of information theory and Boolean function analysis (t.co/IqmudUd4wM). We have also successfully verified analytic parts of the proof in Lean.

This result emerged from an extensive human–AI collaboration with input from multiple AI models developed through a close partnership between our group at Google with Amin, Chandra, and Zijie at CHUK; See section 4 for details on our human-AI collaboration.

The Courtade–Kumar conjecture was among the problems we set out to tackle in our AI-acceleration paper (arXiv:2602.03837). In this effort, we made substantial use of the Stellar Colosseum harness (arXiv:2609.15983) and a range of external and internal Gemini models.

Background and Significance of CK Conjecture:

- Posed by Thomas Courtade and P. R. Kumar ("Which Boolean Functions Maximize Mutual Information on Noisy Inputs?"), the conjecture posits that for a uniform input X in {-1, 1}^n passed through BSC(p) to produce Y, the mutual information I(f(X); Y) for any Boolean function f is maximized by coordinate projections f(x) = x_i, attaining the sharp upper bound 1 - h(p).

- The conjecture belongs to a broader family of extremal problems that have attracted sustained attention. It has helped motivate parallel lines of work in information theory, theoretical computer science, Boolean function analysis, and discrete isoperimetry.

- Kindler, O’Donnell, and Witmer document the considerable interest it has generated, and Yu and Tan’s 2022 monograph describes it as “one of the most important open problems in information theory” [28, Section 9.1.2].

- At a structural level, the conjecture is connected to foundational isoperimetric and functional inequalities, including Talagrand’s isoperimetric inequality and Bobkov’s inequality, as well as related conjectures on their optimal forms. In some regimes, it also recovers Harper's classical edge-isoperimetric inequality on the discrete cube.

Last week, we learned that Ky and Tran had independently obtained a very different proof of the conjecture. We coordinated with them to release the two works separately citing the other. The two approaches offer substantially different approaches (t.co/Bg7m89orzj). Congratulations to Ky and Tran  as well on this great achievement.

Stellar Colosseum is available externally as the long proof pattern of /teamwork in AntiGravity (t.co/rZ1JGOKrs0). We plan to move the math x human collaboration features to AntiGravity and I am excited to provide this as a math collaboration platfom externally.

Thanks for my wonderful coauthors Zijie Chen, Amin Gohari, @AdelJavanmard, Honghao Lin, Chandra Nair David Woodruff

Link to paper: t.co/IqmudUd4wM