The Courtade–Kumar conjecture, also called the most informative Boolean function conjecture, concerns n independent uniform bits X observed through independent binary symmetric channels with crossover probability p; call the output Y. It asserts that every Boolean function f satisfies I(f(X); Y) ≤ 1 − h(p) bits, where h is the binary entropy, so that a single coordinate (a dictator function) is the most informative one-bit summary. Courtade and Kumar posed it in 2013. Two manuscripts dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim proofs of it and of the stronger Hellinger conjecture. Several other groups posted proofs of the Courtade–Kumar conjecture in the same week. This page summarizes OpenAI's published claims, lists the other proofs with their public dates and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- The Hellinger conjecture, formulated by Anantharam, Bogdanov, Chakrabarti, Jayram and Nair in a 2017 manuscript, concerns a Boolean function f on {−1, 1}n with mean m. For every ρ in [−1, 1] it asserts that √(1 − m2) − E√(1 − (Tρf)2) ≤ 1 − √(1 − ρ2), where Tρ is the noise operator. As recalled in OpenAI's Hellinger manuscript and in Ky's paper listed below, it implies the Courtade–Kumar conjecture (Proposition 1 of Anantharam et al.).
- Partial results cited in OpenAI's manuscripts include high-noise bounds of Ordentlich, Shayevitz and Weinstein and of Samorodnitsky, the work of Javanmard and Woodruff (arXiv:2601.09679) and the differential-equation approach of Chen, Gohari and Nair.
The original results
- Claim (soft-channel contraction). For every finite n, every function u from {−1, 1}n to [−1, 1] (a randomized binary summary) and every ρ in [−1, 1], the information retained after noise is at most ψ(|ρ| ψ−1(I(u))). Here ψ(r) = log 2 − H(r), and H(r) is the entropy of a sign with mean r. Soft coordinate functions attain equality (Theorem 1.1). For Boolean f with mean m the manuscript derives I(f(X); Y) ≤ ψ(|ρ| rm) ≤ ψ(|ρ|), with rm = ψ−1(H(m)). The right-hand bound is the Courtade–Kumar inequality with ρ = 1 − 2p (Corollary 1.2). The manuscript also states a mean-dependent entropy-production bound. Source: the manuscript Sharp binary-information contraction on the discrete cube, dated 24 September 2026 (repository commit
1581d4c).
- Claim (Hellinger conjecture with arbitrary output bias). For a Boolean function of mean m and every ρ in [−1, 1], the Hellinger loss above is at most 1 − √(1 − ρ2), with equality for signed coordinates. The proof combines asymmetric dimension induction, a noise-semigroup energy estimate and finite exact arithmetic certificates. Source: the manuscript Hellinger contraction with arbitrary Boolean output bias, dated 24 September 2026.
- Formalization, as described by the repository. The scope note lean/docs/119.md lists only the soft-channel manuscript. Its comparator statements are CourtadeKumar.lean (the inequality and its attainment, for crossover probabilities from 0 to 1/2) and SoftChannel204.lean (soft-channel contraction and entropy production). The note does not list the Hellinger manuscript.
- Relation to concurrent work, as stated in the manuscripts. The soft-channel manuscript cites the proofs by Chen et al., Ky and Tran, Mahdavifar and Beirami, and Kramer and Saglam listed below. It states that the overlap with Chen et al. "extends beyond the Boolean conjecture": their Lemma 9.2 applies to arbitrary binary channels, and retaining the initial information when integrating their production bound gives the manuscript's Theorem 1.1 and Corollary 1.2. The Hellinger manuscript describes the Hellinger inequality as a distinct functional statement, from which the ordinary Courtade–Kumar bound follows.
Other proofs of the conjecture
| Date |
Work |
Approach, as described in the cited sources |
Public status (checked 15 October 2026)
|
| 2026-09-21 |
Vu Khac Ky and Tuan Tran, arXiv:2609.24184 (v1), Dictators are most informative; certificates and scripts in vukhacky/courtade-kumar-conjecture |
An entropy-production and spectral framework with computer-assisted verification. |
Preprint, one version.
|
| 2026-09-21 |
Zijie Chen, Amin Gohari, Adel Javanmard, Honghao Lin, Vahab Mirrokni, Chandra Nair and David P. Woodruff, arXiv:2609.24931 (v1; v2 of 24 September), A proof of the most informative Boolean function conjecture; Lean code in dpwoodru/general-courtade-kumar-lean |
A computer-assisted Bellman inequality within the differential-equation method. |
Preprint. The repository README describes an end-to-end Lean 4 proof (about 45,500 modules, mostly generated certificate data) whose final theorem depends only on Lean's three standard axioms. It reports a comparator run and acceptance by the con-leche external checker. Its formal statement was merged into Google DeepMind's Formal Conjectures repository on 15 October 2026 (follow-up table below).
|
| 2026-09-22 |
Hessam Mahdavifar and Ahmad Beirami, arXiv:2609.26444 (v1; v2 of 28 September), The most informative bit and beyond |
A proof of the conjecture, together with multibit extensions: counterexamples to the k-bit extension for k ≥ 8 and a conjecture that it holds for 2 ≤ k ≤ 7. |
Preprint. Its generative-AI disclosure states that AI systems generated the single-bit proof, including its detailed derivations, with the authors providing direction, feedback and final review. Version 2 states that the authors verified Kramer and Saglam's proof independently in Lean.
|
| 2026-09-23 |
Dimiter Kramer and Mert Saglam, deepinfra/courtade-kumar, On the most informative Boolean function under noise (PDF of 23 September; source files from 21 September) |
Induction on the dimension, applied to a strengthened inequality that keeps the output mean μ: the information is at most ρ2(h(μ) − ν) + ν(1 − h(p)) bits, where ν = 4μ(1 − μ). |
A manuscript in a GitHub repository; OpenAI's soft-channel manuscript cites the commit of 23 September.
|
| commits dated up to 8 September 2026 |
Matthew Ho, sunfishho/courtade-kumar-conjecture |
A Lean 4 formalization with completed numerical certificates. |
The README reports a comparator statement check, an axiom whitelist check and a fresh kernel replay, and states that "the proof is in the process of being digested". The repository does not show when it became public. Version 2 of Chen et al. mentions that Ho and a collaborator shared an outline, an AI-generated document and Lean files with them privately after their posting.
|
Public follow-up work
| Date |
Work |
Relation |
Public claim |
Public status (checked 15 October 2026)
|
| 2026-10-07 |
Vu Khac Ky, arXiv:2610.10618 (v1), The Hellinger conjecture for antipodal Boolean functions |
Parallel (special case) |
Proves the Hellinger inequality for Boolean functions with a sign-reversing symmetry and extends the argument to arbitrary independent binary-input channels. It cites OpenAI's collection (entry 119) as an announcement of the inequality for arbitrary output bias. |
Preprint.
|
| 2026-10-15 |
formal-conjectures pull request #6688 |
Formal statement |
Adds the Courtade–Kumar conjecture to Google DeepMind's Formal Conjectures repository, tagged as solved, with a formal-proof link to Chen et al.'s Lean repository. The description states that the definitions are definitionally equal to that repository's statement, so its final theorem implies the Formal Conjectures statement by unfolding. |
Merged on 15 October 2026.
|
Notes
- Dates are those shown by arXiv, by the GitHub commit history or by the pull request. The lists cover sources found up to the date above; they make no priority or completeness claim.
