Browse › Theoretical computer science › 119 The Courtade–Kumar and Hellinger conjectures
Sharp binary-information contraction on the discrete cube
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove sharp contraction of the information carried by a binary channel under independent symmetric noise on a uniform discrete cube. At fixed initial information, a noisy coordinate retains the most information. The Boolean specialization resolves the Courtade–Kumar conjecture and gives an output-entropy refinement. We also establish a stronger mean-dependent entropy-production bound. The proof combines an explicit three-point optimizer for the local joining problem, two entropy capacities, and a common-output thinning inequality, followed by dimension induction and integration along the noise semigroup.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope notes for family 119: The Courtade–Kumar and Hellinger conjectures (lean/docs/119.md, 2026). Describes the release's own Lean development for this paper: sharp soft-channel contraction, the bias-refined Boolean bound, the mean-dependent entropy-production inequality and the Courtade–Kumar inequality, with comparator files
CourtadeKumar.leanandSoftChannel204.lean. - D. P. Woodruff et al., general-courtade-kumar-lean (GitHub, release v1.2 dated 2026-10-01). An independent Lean 4 proof of the Courtade–Kumar inequality $I(f(X);Y)\le 1-H(p)$, i.e. the universal bound in Corollary 1.2; it accompanies Chen–Gohari–Javanmard–Lin–Mirrokni–Nair–Woodruff (arXiv:2609.24931) rather than this paper.
- Google DeepMind formal-conjectures, FormalConjectures/Paper/CourtadeKumar.lean (added by PR #6688, merged 2026-10-15). A formal statement of the Courtade–Kumar conjecture tagged "research solved", whose
formal_prooflink points to the Woodruff et al. Lean project; it does not reference the OpenAI papers.
Possibly relevant literature (found by the agent, not checked)
- Y. Polyanskiy and Y. Wu, Strong data-processing inequalities for channels and Bayesian networks (arXiv:1508.06025, 2015/2016). Introduces the $F_I$-curve as the best possible non-linear SDPI for a channel, a statement of the same kind as Theorem 1.1's bound on $I(U;Y)$ in terms of $I(U;X)$ for the uniform-input product BSC.
- V. K. Ky and T. Tran, Stability of the Courtade-Kumar inequality (arXiv:2609.31797, 25 Sep 2026). Proves dimension-independent stability: functions whose information is close to the dictator value are close to signed dictators, which relates to the equality and strict-improvement statements in Corollary 1.2.
Digests and expositions
- AI Proved What?, The best bit? The Courtade–Kumar and Hellinger conjectures (Episode 119, October 2026). This AI-assisted video and transcript explain both manuscripts’ claims and proof strategies and distinguish the contraction paper’s Lean scope from the Hellinger paper’s exact-arithmetic certificates. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 119
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026,
author = {{OpenAI}},
title = {{Sharp binary-information contraction on the discrete cube}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/main.pdf}{OAI:Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/119.md. The Lean statements have not been checked by people against the paper's claims.
Family 119: The Courtade–Kumar and Hellinger conjectures
Proves the Courtade–Kumar conjecture: among Boolean functions of independent uniform bits, a single coordinate retains the most mutual information after independent bit-flip noise. A stronger theorem treats randomized binary summaries at fixed initial information. The Hellinger conjecture is also proved for every Boolean output bias and noise correlation.
Other papers in this family:
- Hellinger contraction with arbitrary Boolean output bias · September 24, 2026